[isabelle] partial functions



Hi,

thank you, but i dont know how to prove this either :-) 
"f a = Some b ⟶  ((f |` (- {a}))(a ↦ b)) = f"Can you help me?
 		 	   		  


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