let X, Y be non empty set ; :: thesis: for f being Function of X,Y holds [:f,f:] " (id Y) is Equivalence_Relation of X
let f be Function of X,Y; :: thesis: [:f,f:] " (id Y) is Equivalence_Relation of X
set ff = [:f,f:] " (id Y);
A1: dom f = X by FUNCT_2:def 1;
reconsider R9 = [:f,f:] " (id Y) as Relation of X ;
A2: dom [:f,f:] = [:(dom f),(dom f):] by FUNCT_3:def 8;
R9 is_reflexive_in X

proof

let x be object ; :: according to RELAT_2:def 1 :: thesis: ( not x in X or [x,x] in R9 )
assume A3: x in X ; :: thesis: [x,x] in R9
then reconsider x9 = x as Element of X ;
A4: [(f . x9),(f . x9)] in id Y by RELAT_1:def 10;
( [x,x] in dom [:f,f:] & [(f . x),(f . x)] = [:f,f:] . (x,x) ) by A2, A1, A3, FUNCT_3:def 8, ZFMISC_1:def 2;
hence [x,x] in R9 by A4, FUNCT_1:def 7; :: thesis: verum

end;

then A5: ( dom R9 = X & field R9 = X ) by ORDERS_1:13;
A6: R9 is_symmetric_in X

proof

let x, y be object ; :: according to RELAT_2:def 3 :: thesis: ( not x in X or not y in X or not [x,y] in R9 or [y,x] in R9 )
assume that
A7: ( x in X & y in X ) and
A8: [x,y] in R9 ; :: thesis: [y,x] in R9
reconsider x9 = x, y9 = y as Element of X by A7;
A9: ( [y,x] in dom [:f,f:] & [(f . y),(f . x)] = [:f,f:] . (y,x) ) by A2, A1, A7, FUNCT_3:def 8, ZFMISC_1:def 2;
A10: ( [:f,f:] . [x,y] in id Y & [(f . x),(f . y)] = [:f,f:] . (x,y) ) by A1, A7, A8, FUNCT_1:def 7, FUNCT_3:def 8;
then f . x9 = f . y9 by RELAT_1:def 10;
hence [y,x] in R9 by A10, A9, FUNCT_1:def 7; :: thesis: verum

end;

R9 is_transitive_in X

proof

let x, y, z be object ; :: according to RELAT_2:def 8 :: thesis: ( not x in X or not y in X or not z in X or not [x,y] in R9 or not [y,z] in R9 or [x,z] in R9 )
assume that
A11: x in X and
A12: y in X and
A13: z in X and
A14: [x,y] in R9 and
A15: [y,z] in R9 ; :: thesis: [x,z] in R9
A16: ( [x,z] in dom [:f,f:] & [(f . x),(f . z)] = [:f,f:] . (x,z) ) by A2, A1, A11, A13, FUNCT_3:def 8, ZFMISC_1:def 2;
reconsider y9 = y, z9 = z as Element of X by A12, A13;
( [:f,f:] . [y,z] in id Y & [(f . y),(f . z)] = [:f,f:] . (y,z) ) by A1, A12, A13, A15, FUNCT_1:def 7, FUNCT_3:def 8;
then A17: f . y9 = f . z9 by RELAT_1:def 10;
( [:f,f:] . [x,y] in id Y & [(f . x),(f . y)] = [:f,f:] . (x,y) ) by A1, A11, A12, A14, FUNCT_1:def 7, FUNCT_3:def 8;
hence [x,z] in R9 by A17, A16, FUNCT_1:def 7; :: thesis: verum

end;

hence [:f,f:] " (id Y) is Equivalence_Relation of X by A5, A6, PARTFUN1:def 2, RELAT_2:def 11, RELAT_2:def 16; :: thesis: verum