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, o' being object of C1
for f being Morphism of o,o' st <^o,o'^> <> {} holds
(Morph-Map (C1 --> m),o,o') . f = m
let o2 be object of C2; :: thesis: ( <^o2,o2^> <> {} implies for m being Morphism of o2,o2
for o, o' being object of C1
for f being Morphism of o,o' st <^o,o'^> <> {} holds
(Morph-Map (C1 --> m),o,o') . f = m )
assume A1:
<^o2,o2^> <> {}
; :: thesis: for m being Morphism of o2,o2
for o, o' being object of C1
for f being Morphism of o,o' st <^o,o'^> <> {} holds
(Morph-Map (C1 --> m),o,o') . f = m
let m be Morphism of o2,o2; :: thesis: for o, o' being object of C1
for f being Morphism of o,o' st <^o,o'^> <> {} holds
(Morph-Map (C1 --> m),o,o') . f = m
let o, o' be object of C1; :: thesis: for f being Morphism of o,o' st <^o,o'^> <> {} holds
(Morph-Map (C1 --> m),o,o') . f = m
let f be Morphism of o,o'; :: 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 C1 : verum } ;
set Y = { [[o1,o1'],((the Arrows of C1 . o1,o1') --> m)] where o1, o1' is Element of C1 : verum } ;
A3:
{ [[o1,o1'],(<^o1,o1'^> --> m)] where o1, o1' is object of C1 : verum } c= { [[o1,o1'],((the Arrows of C1 . o1,o1') --> m)] where o1, o1' is Element of C1 : 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 C1 : verum } or e in { [[o1,o1'],((the Arrows of C1 . o1,o1') --> m)] where o1, o1' is Element of C1 : verum } )
assume
e in { [[o1,o1'],(<^o1,o1'^> --> m)] where o1, o1' is object of C1 : verum }
;
:: thesis: e in { [[o1,o1'],((the Arrows of C1 . o1,o1') --> m)] where o1, o1' is Element of C1 : verum }
then consider o1,
o1' being
object of
C1 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 C1 : verum }
;
:: thesis: verum
end;
A5:
{ [[o1,o1'],((the Arrows of C1 . o1,o1') --> m)] where o1, o1' is Element of C1 : verum } c= { [[o1,o1'],(<^o1,o1'^> --> m)] where o1, o1' is object of C1 : 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 C1 : verum } or e in { [[o1,o1'],(<^o1,o1'^> --> m)] where o1, o1' is object of C1 : verum } )
assume
e in { [[o1,o1'],((the Arrows of C1 . o1,o1') --> m)] where o1, o1' is Element of C1 : verum }
;
:: thesis: e in { [[o1,o1'],(<^o1,o1'^> --> m)] where o1, o1' is object of C1 : verum }
then consider o1,
o1' being
Element of
C1 such that A6:
e = [[o1,o1'],((the Arrows of C1 . o1,o1') --> m)]
;
reconsider o1 =
o1,
o1' =
o1' as
object of
C1 ;
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 C1 : verum }
;
:: thesis: 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,o1'],(<^o1,o1'^> --> m)] where o1, o1' is object of C1 : verum }
by A1, Def18;
then A7:
the MorphMap of (C1 --> m) = { [[o1,o1'],H1(o1,o1')] where o1, o1' is Element of C1 : S1[o1,o1'] }
by A3, A5, XBOOLE_0:def 10;
A8:
S1[o,o']
;
Morph-Map (C1 --> m),o,o' =
the MorphMap of (C1 --> m) . o,o'
.=
H1(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