let C be non empty transitive AltCatStr ; :: thesis: 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; :: thesis: 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; :: thesis: ( <^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^> <> {} ) ; :: thesis: 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; :: thesis: ( 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 ) ; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: for gg being Morphism of p2,p3 st f = ff & g = gg holds
g * f = gg * ff
let gg be Morphism of p2,p3; :: thesis: ( f = ff & g = gg implies g * f = gg * ff )
assume A3: ( f = ff & g = gg ) ; :: thesis: g * f = gg * ff
<^p1,p3^> <> {} by A1, ALTCAT_1:def 4;
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:106;
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, Def2;
( <^o1,o2^> <> {} & <^o2,o3^> <> {} ) by A1, A2, Th32, XBOOLE_1:3;
hence g * f = (the Comp of C . o1,o2,o3) . g,f by ALTCAT_1:def 10
.= (the Comp of D . p1,p2,p3) . gg,ff by A3, A4, A6, GRFUNC_1:8
.= gg * ff by A1, ALTCAT_1:def 10 ;
:: thesis: verum