let C1, C2 be non empty AltGraph ; :: thesis: for o2 being object of st <^o2,o2^> <> {} holds
for m being Morphism of ,
for o, o' being object of
for f being Morphism of , st <^o,o'^> <> {} holds
(Morph-Map (C1 --> m),o,o') . f = m
let o2 be object of ; :: thesis: ( <^o2,o2^> <> {} implies for m being Morphism of ,
for o, o' being object of
for f being Morphism of , st <^o,o'^> <> {} holds
(Morph-Map (C1 --> m),o,o') . f = m )
assume A1: <^o2,o2^> <> {} ; :: thesis: for m being Morphism of ,
for o, o' being object of
for f being Morphism of , st <^o,o'^> <> {} holds
(Morph-Map (C1 --> m),o,o') . f = m
let m be Morphism of ,; :: thesis: for o, o' being object of
for f being Morphism of , st <^o,o'^> <> {} holds
(Morph-Map (C1 --> m),o,o') . f = m
let o, o' be object of ; :: thesis: for f being Morphism of , st <^o,o'^> <> {} holds
(Morph-Map (C1 --> m),o,o') . f = m
let f be Morphism of ,; :: thesis: ( <^o,o'^> <> {} implies (Morph-Map (C1 --> m),o,o') . f = m )
assume A2: <^o,o'^> <> {} ; :: thesis: (Morph-Map (C1 --> m),o,o') . f = m
set X = { [[o1,o1'],(<^o1,o1'^> --> m)] where o1, o1' is object of : verum } ;
set Y = { [[o1,o1'],((the Arrows of C1 . o1,o1') --> m)] where o1, o1' is Element of : verum } ;
A3: { [[o1,o1'],(<^o1,o1'^> --> m)] where o1, o1' is object of : verum } c= { [[o1,o1'],((the Arrows of C1 . o1,o1') --> m)] where o1, o1' is Element of : verum }

proof

let e be set ; :: according to TARSKI:def 3 :: thesis: ( not e in { [[o1,o1'],(<^o1,o1'^> --> m)] where o1, o1' is object of : verum } or e in { [[o1,o1'],((the Arrows of C1 . o1,o1') --> m)] where o1, o1' is Element of : verum } )
assume e in { [[o1,o1'],(<^o1,o1'^> --> m)] where o1, o1' is object of : verum } ; :: thesis: e in { [[o1,o1'],((the Arrows of C1 . o1,o1') --> m)] where o1, o1' is Element of : verum }
then consider o1, o1' being object of such that
A4: e = [[o1,o1'],(<^o1,o1'^> --> m)] ;
e = [[o1,o1'],((the Arrows of C1 . o1,o1') --> m)] by A4, ALTCAT_1:def 2;
hence e in { [[o1,o1'],((the Arrows of C1 . o1,o1') --> m)] where o1, o1' is Element of : verum } ; :: thesis: verum

end;

A5: { [[o1,o1'],((the Arrows of C1 . o1,o1') --> m)] where o1, o1' is Element of : verum } c= { [[o1,o1'],(<^o1,o1'^> --> m)] where o1, o1' is object of : verum }

proof

let e be set ; :: according to TARSKI:def 3 :: thesis: ( not e in { [[o1,o1'],((the Arrows of C1 . o1,o1') --> m)] where o1, o1' is Element of : verum } or e in { [[o1,o1'],(<^o1,o1'^> --> m)] where o1, o1' is object of : verum } )
assume e in { [[o1,o1'],((the Arrows of C1 . o1,o1') --> m)] where o1, o1' is Element of : verum } ; :: thesis: e in { [[o1,o1'],(<^o1,o1'^> --> m)] where o1, o1' is object of : verum }
then consider o1, o1' being Element of such that
A6: e = [[o1,o1'],((the Arrows of C1 . o1,o1') --> m)] ;
reconsider o1 = o1, o1' = o1' as object of ;
e = [[o1,o1'],(<^o1,o1'^> --> m)] by A6, ALTCAT_1:def 2;
hence e in { [[o1,o1'],(<^o1,o1'^> --> m)] where o1, o1' is object of : verum } ; :: thesis: verum

end;

defpred S₁[ set , set ] means verum;
deffunc H₁( Element of , Element of ) -> Element of bool [:(the Arrows of C1 . $1,$2),{m}:] = (the Arrows of C1 . $1,$2) --> m;
the MorphMap of (C1 --> m) = { [[o1,o1'],(<^o1,o1'^> --> m)] where o1, o1' is object of : verum } by A1, Def18;
then A7: the MorphMap of (C1 --> m) = { [[o1,o1'],H₁(o1,o1')] where o1, o1' is Element of : S₁[o1,o1'] } by A3, A5, XBOOLE_0:def 10;
A8: S₁[o,o'] ;
Morph-Map (C1 --> m),o,o' = the MorphMap of (C1 --> m) . o,o'
.= H₁(o,o') from FUNCTOR0:sch 1(A7, A8) ;
hence (Morph-Map (C1 --> m),o,o') . f = (<^o,o'^> --> m) . f by ALTCAT_1:def 2
.= m by A2, FUNCOP_1:13 ;
:: thesis: verum