let C1, C2 be non empty AltGraph ; 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; ( <^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^> <> {}
; 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; 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; 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; ( <^o,o9^> <> {} implies (Morph-Map ((C1 --> m),o,o9)) . f = m )
assume A2:
<^o,o9^> <> {}
; (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 ;
TARSKI:def 3 ( 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 }
;
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 }
;
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 ;
TARSKI:def 3 ( 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 }
;
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 }
;
verum
end;
defpred S1[ set , set ] means verum;
deffunc H1( 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],H1(o1,o19)] where o1, o19 is Element of C1 : S1[o1,o19] }
by A3, A5;
A8:
S1[o,o9]
;
Morph-Map ((C1 --> m),o,o9) =
the MorphMap of (C1 --> m) . (o,o9)
.=
H1(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
;
verum