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 object ; :: 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 object such that
A1: yy in [:A,A:] and
A2: yy in id A and
A3: [:f,f:] . yy = x by FUNCT_2:64;
consider y, y9 being object such that
A4: y in A and
y9 in A and
A5: yy = [y,y9] by A1, ZFMISC_1:84;
A6: y = y9 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:5;
A8: y in dom f by A4, FUNCT_2:def 1;
x = [:f,f:] . (y,y9) by A3, A5
.= [(f . y),(f . y)] by A6, A8, FUNCT_3:def 8 ;
hence x in id B by A7, RELAT_1:def 10; :: thesis: verum