[isabelle] partial functions



Hi,

how can i prove

"the (f a) = b ⟶  ((f |` (- {a}))(a ↦ b)) = f"

Thank you!
 		 	   		  


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.