let A be set ; :: thesis: for B being non empty set
for f being Function of A,B holds [:f,f:] .: (id A) c= id B
let B be non empty set ; :: thesis: for f being Function of A,B holds [:f,f:] .: (id A) c= id B
let f be Function of A,B; :: thesis: [:f,f:] .: (id A) c= id B
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in [:f,f:] .: (id A) or x in id B )
assume x in [:f,f:] .: (id A) ; :: thesis: x in id B
then consider yy being set such that
A1: yy in [:A,A:] and
A2: yy in id A and
A3: [:f,f:] . yy = x by FUNCT_2:115;
consider y, y' being set such that
A4: ( y in A & y' in A ) and
A5: yy = [y,y'] by A1, ZFMISC_1:103;
A6: y = y' by A2, A5, RELAT_1:def 10;
reconsider y = y as Element of A by A4;
A7: f . y in B by A4, FUNCT_2:7;
A8: y in dom f by A4, FUNCT_2:def 1;
x = [:f,f:] . y,y' by A3, A5
.= [(f . y),(f . y)] by A6, A8, FUNCT_3:def 9 ;
hence x in id B by A7, RELAT_1:def 10; :: thesis: verum