let C be non empty transitive AltCatStr ; for D being non empty transitive SubCatStr of C
for p1, p2, p3 being Object of D st <^p1,p2^> <> {} & <^p2,p3^> <> {} holds
for o1, o2, o3 being Object of C st o1 = p1 & o2 = p2 & o3 = p3 holds
for f being Morphism of o1,o2
for g being Morphism of o2,o3
for ff being Morphism of p1,p2
for gg being Morphism of p2,p3 st f = ff & g = gg holds
g * f = gg * ff
let D be non empty transitive SubCatStr of C; for p1, p2, p3 being Object of D st <^p1,p2^> <> {} & <^p2,p3^> <> {} holds
for o1, o2, o3 being Object of C st o1 = p1 & o2 = p2 & o3 = p3 holds
for f being Morphism of o1,o2
for g being Morphism of o2,o3
for ff being Morphism of p1,p2
for gg being Morphism of p2,p3 st f = ff & g = gg holds
g * f = gg * ff
let p1, p2, p3 be Object of D; ( <^p1,p2^> <> {} & <^p2,p3^> <> {} implies for o1, o2, o3 being Object of C st o1 = p1 & o2 = p2 & o3 = p3 holds
for f being Morphism of o1,o2
for g being Morphism of o2,o3
for ff being Morphism of p1,p2
for gg being Morphism of p2,p3 st f = ff & g = gg holds
g * f = gg * ff )
assume A1:
( <^p1,p2^> <> {} & <^p2,p3^> <> {} )
; for o1, o2, o3 being Object of C st o1 = p1 & o2 = p2 & o3 = p3 holds
for f being Morphism of o1,o2
for g being Morphism of o2,o3
for ff being Morphism of p1,p2
for gg being Morphism of p2,p3 st f = ff & g = gg holds
g * f = gg * ff
let o1, o2, o3 be Object of C; ( o1 = p1 & o2 = p2 & o3 = p3 implies for f being Morphism of o1,o2
for g being Morphism of o2,o3
for ff being Morphism of p1,p2
for gg being Morphism of p2,p3 st f = ff & g = gg holds
g * f = gg * ff )
assume A2:
( o1 = p1 & o2 = p2 & o3 = p3 )
; for f being Morphism of o1,o2
for g being Morphism of o2,o3
for ff being Morphism of p1,p2
for gg being Morphism of p2,p3 st f = ff & g = gg holds
g * f = gg * ff
let f be Morphism of o1,o2; for g being Morphism of o2,o3
for ff being Morphism of p1,p2
for gg being Morphism of p2,p3 st f = ff & g = gg holds
g * f = gg * ff
let g be Morphism of o2,o3; for ff being Morphism of p1,p2
for gg being Morphism of p2,p3 st f = ff & g = gg holds
g * f = gg * ff
let ff be Morphism of p1,p2; for gg being Morphism of p2,p3 st f = ff & g = gg holds
g * f = gg * ff
let gg be Morphism of p2,p3; ( f = ff & g = gg implies g * f = gg * ff )
assume A3:
( f = ff & g = gg )
; g * f = gg * ff
<^p1,p3^> <> {}
by A1, ALTCAT_1:def 2;
then
dom ( the Comp of D . (p1,p2,p3)) = [:<^p2,p3^>,<^p1,p2^>:]
by FUNCT_2:def 1;
then A4:
[gg,ff] in dom ( the Comp of D . (p1,p2,p3))
by A1, ZFMISC_1:87;
A5:
the Comp of D cc= the Comp of C
by Def11;
( the Comp of D . (p1,p2,p3) = the Comp of D . [p1,p2,p3] & the Comp of C . (o1,o2,o3) = the Comp of C . [o1,o2,o3] )
by MULTOP_1:def 1;
then A6:
the Comp of D . (p1,p2,p3) c= the Comp of C . (o1,o2,o3)
by A2, A5;
( <^o1,o2^> <> {} & <^o2,o3^> <> {} )
by A1, A2, Th31, XBOOLE_1:3;
hence g * f =
( the Comp of C . (o1,o2,o3)) . (g,f)
by ALTCAT_1:def 8
.=
( the Comp of D . (p1,p2,p3)) . (gg,ff)
by A3, A4, A6, GRFUNC_1:2
.=
gg * ff
by A1, ALTCAT_1:def 8
;
verum