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,f:] = [:(dom f),(dom f):] by FUNCT_3:def 9;
A2: dom f = X by FUNCT_2:def 1;
reconsider R' = [:f,f:] " (id Y) as Relation of X ;
( R' is total & R' is symmetric & R' is transitive )

proof

R' is_reflexive_in X

proof

let x be set ; :: according to RELAT_2:def 1 :: thesis: ( not x in X or [x,x] in R' )
assume A3: x in X ; :: thesis: [x,x] in R'
then reconsider x' = x as Element of X ;
A4: [x,x] in dom [:f,f:] by A1, A2, A3, ZFMISC_1:def 2;
A5: [(f . x'),(f . x')] in id Y by RELAT_1:def 10;
[(f . x),(f . x)] = [:f,f:] . x,x by A2, A3, FUNCT_3:def 9;
hence [x,x] in R' by A4, A5, FUNCT_1:def 13; :: thesis: verum

end;

then A6: ( dom R' = X & field R' = X ) by ORDERS_1:98;
hence R' is total by PARTFUN1:def 4; :: thesis: ( R' is symmetric & R' is transitive )
R' is_symmetric_in X

proof

let x, y be set ; :: according to RELAT_2:def 3 :: thesis: ( not x in X or not y in X or not [x,y] in R' or [y,x] in R' )
assume A7: ( x in X & y in X & [x,y] in R' ) ; :: thesis: [y,x] in R'
then reconsider x' = x, y' = y as Element of X ;
A8: ( [x,y] in dom [:f,f:] & [:f,f:] . [x,y] in id Y ) by A7, FUNCT_1:def 13;
A9: [(f . x),(f . y)] = [:f,f:] . x,y by A2, A7, FUNCT_3:def 9;
then A10: f . x' = f . y' by A8, RELAT_1:def 10;
A11: [y,x] in dom [:f,f:] by A1, A2, A7, ZFMISC_1:def 2;
[(f . y),(f . x)] = [:f,f:] . y,x by A2, A7, FUNCT_3:def 9;
hence [y,x] in R' by A8, A9, A10, A11, FUNCT_1:def 13; :: thesis: verum

end;

hence R' is symmetric by A6, RELAT_2:def 11; :: thesis: R' is transitive
R' is_transitive_in X

proof

let x, y, z be set ; :: 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 R' or not [y,z] in R' or [x,z] in R' )
assume that
A12: ( x in X & y in X & z in X ) and
A13: ( [x,y] in R' & [y,z] in R' ) ; :: thesis: [x,z] in R'
reconsider y' = y, z' = z as Element of X by A12;
A14: ( [x,y] in dom [:f,f:] & [:f,f:] . [x,y] in id Y ) by A13, FUNCT_1:def 13;
A15: ( [y,z] in dom [:f,f:] & [:f,f:] . [y,z] in id Y ) by A13, FUNCT_1:def 13;
A16: [(f . x),(f . y)] = [:f,f:] . x,y by A2, A12, FUNCT_3:def 9;
[(f . y),(f . z)] = [:f,f:] . y,z by A2, A12, FUNCT_3:def 9;
then A17: f . y' = f . z' by A15, RELAT_1:def 10;
A18: [x,z] in dom [:f,f:] by A1, A2, A12, ZFMISC_1:def 2;
[(f . x),(f . z)] = [:f,f:] . x,z by A2, A12, FUNCT_3:def 9;
hence [x,z] in R' by A14, A16, A17, A18, FUNCT_1:def 13; :: thesis: verum

end;

hence R' is transitive by A6, RELAT_2:def 16; :: thesis: verum

end;

hence [:f,f:] " (id Y) is Equivalence_Relation of X ; :: thesis: verum