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

proof

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

end;

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

proof

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

end;

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