hereby ( ( 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
;
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;
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;
verum
end;
assume A4:
for o being Object of A holds the ObjectMap of F . (o,o) = [(F . o),(F . o)]
; F is reflexive
let x be object ; TARSKI:def 3,FUNCTOR0:def 8 ( 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)
; 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; verum