hereby :: thesis: ( ( for o being Object of A holds the ObjectMap of F . (o,o) = [(F . o),(F . o)] ) implies F is reflexive )

assume F is reflexive ; :: thesis: for o being Object of A holds the ObjectMap of F . (o,o) = [(F . o),(F . o)]
then A1: the ObjectMap of F .: (id the carrier of A) c= id the carrier of B ;
let o be Object of A; :: thesis: the ObjectMap of F . (o,o) = [(F . o),(F . o)]
[o,o] in id the carrier of A by RELAT_1:def 10;
then A2: the ObjectMap of F . (o,o) in the ObjectMap of F .: (id the carrier of A) by FUNCT_2:35;
consider p, p9 being object such that
A3: the ObjectMap of F . (o,o) = [p,p9] by RELAT_1:def 1;
thus the ObjectMap of F . (o,o) = [(F . o),(F . o)] by A1, A2, A3, RELAT_1:def 10; :: thesis: verum

end;

assume A4: for o being Object of A holds the ObjectMap of F . (o,o) = [(F . o),(F . o)] ; :: thesis: F is reflexive
let x be object ; :: according to TARSKI:def 3,FUNCTOR0:def 8 :: thesis: ( not x in the ObjectMap of F .: (id the carrier of A) or x in id the carrier of B )
assume x in the ObjectMap of F .: (id the carrier of A) ; :: thesis: x in id the carrier of B
then consider y being object such that
A5: y in [: the carrier of A, the carrier of A:] and
A6: y in id the carrier of A and
A7: x = the ObjectMap of F . y by FUNCT_2:64;
consider o, o9 being Element of A such that
A8: y = [o,o9] by A5, DOMAIN_1:1;
reconsider o = o as Object of A ;
o = o9 by A6, A8, RELAT_1:def 10;
then x = [(F . o),(F . o)] by A4, A7, A8;
hence x in id the carrier of B by RELAT_1:def 10; :: thesis: verum