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 ;
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 ;
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 ;
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
.= gg * ff by ;
:: thesis: verum