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 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 ;
:: thesis: verum