2 imports PIPDefs

     2 imports PIPDefs

     3 begin

     3 begin

     4 

     4 

     5 lemma f_image_eq:

     5 lemma f_image_eq:

     6   assumes h: "\<And> a. a \<in> A \<Longrightarrow> f a = g a"

     6   assumes h: "\<And> a. a \<in> A \<Longrightarrow> f a = g a"