let X, Y be non empty set ; :: thesis: for f being Function of X,Y holds [:f,f:] " (id Y) is Equivalence_Relation of
let f be Function of X,Y; :: thesis: [:f,f:] " (id Y) is Equivalence_Relation of
set ff = [:f,f:] " (id Y);
A1: dom f = X by FUNCT_2:def 1;
reconsider R' = [:f,f:] " (id Y) as Relation of ;
A2: dom [:f,f:] = [:(dom f),(dom f):] by FUNCT_3:def 9;
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: [(f . x'),(f . x')] 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 9, ZFMISC_1:def 2;
hence [x,x] in R' by A4, FUNCT_1:def 13; :: thesis: verum

end;

then A5: ( dom R' = X & field R' = X ) by ORDERS_1:98;
A6: 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 that
A7: ( x in X & y in X ) and
A8: [x,y] in R' ; :: thesis: [y,x] in R'
reconsider x' = x, y' = 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 9, 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 13, FUNCT_3:def 9;
then f . x' = f . y' by RELAT_1:def 10;
hence [y,x] in R' by A10, A9, FUNCT_1:def 13; :: thesis: verum

end;

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
A11: x in X and
A12: y in X and
A13: z in X and
A14: [x,y] in R' and
A15: [y,z] in R' ; :: thesis: [x,z] in R'
A16: ( [x,z] in dom [:f,f:] & [(f . x),(f . z)] = [:f,f:] . x,z ) by A2, A1, A11, A13, FUNCT_3:def 9, ZFMISC_1:def 2;
reconsider y' = y, z' = 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 13, FUNCT_3:def 9;
then A17: f . y' = f . z' 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 13, FUNCT_3:def 9;
hence [x,z] in R' by A17, A16, FUNCT_1:def 13; :: thesis: verum

end;

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