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

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