let C be non empty transitive associative AltCatStr ; :: thesis: for o1, o2, o3, o4 being Object of C st <^o1,o2^> <> {} & <^o2,o3^> <> {} & <^o3,o4^> <> {} holds

for a being Morphism of o1,o2

for b being Morphism of o2,o3

for c being Morphism of o3,o4 holds c * (b * a) = (c * b) * a

let o1, o2, o3, o4 be Object of C; :: thesis: ( <^o1,o2^> <> {} & <^o2,o3^> <> {} & <^o3,o4^> <> {} implies for a being Morphism of o1,o2

for b being Morphism of o2,o3

for c being Morphism of o3,o4 holds c * (b * a) = (c * b) * a )

assume that

A1: <^o1,o2^> <> {} and

A2: <^o2,o3^> <> {} and

A3: <^o3,o4^> <> {} ; :: thesis: for a being Morphism of o1,o2

for b being Morphism of o2,o3

for c being Morphism of o3,o4 holds c * (b * a) = (c * b) * a

let a be Morphism of o1,o2; :: thesis: for b being Morphism of o2,o3

for c being Morphism of o3,o4 holds c * (b * a) = (c * b) * a

let b be Morphism of o2,o3; :: thesis: for c being Morphism of o3,o4 holds c * (b * a) = (c * b) * a

let c be Morphism of o3,o4; :: thesis: c * (b * a) = (c * b) * a

A4: ( <^o2,o4^> <> {} & c * b = ( the Comp of C . (o2,o3,o4)) . (c,b) ) by A2, A3, Def2, Def8;

A5: the Comp of C is associative by Def15;

( <^o1,o3^> <> {} & b * a = ( the Comp of C . (o1,o2,o3)) . (b,a) ) by A1, A2, Def2, Def8;

hence c * (b * a) = ( the Comp of C . (o1,o3,o4)) . (c,(( the Comp of C . (o1,o2,o3)) . (b,a))) by A3, Def8

.= ( the Comp of C . (o1,o2,o4)) . ((( the Comp of C . (o2,o3,o4)) . (c,b)),a) by A1, A2, A3, A5

.= (c * b) * a by A1, A4, Def8 ;

:: thesis: verum

for a being Morphism of o1,o2

for b being Morphism of o2,o3

for c being Morphism of o3,o4 holds c * (b * a) = (c * b) * a

let o1, o2, o3, o4 be Object of C; :: thesis: ( <^o1,o2^> <> {} & <^o2,o3^> <> {} & <^o3,o4^> <> {} implies for a being Morphism of o1,o2

for b being Morphism of o2,o3

for c being Morphism of o3,o4 holds c * (b * a) = (c * b) * a )

assume that

A1: <^o1,o2^> <> {} and

A2: <^o2,o3^> <> {} and

A3: <^o3,o4^> <> {} ; :: thesis: for a being Morphism of o1,o2

for b being Morphism of o2,o3

for c being Morphism of o3,o4 holds c * (b * a) = (c * b) * a

let a be Morphism of o1,o2; :: thesis: for b being Morphism of o2,o3

for c being Morphism of o3,o4 holds c * (b * a) = (c * b) * a

let b be Morphism of o2,o3; :: thesis: for c being Morphism of o3,o4 holds c * (b * a) = (c * b) * a

let c be Morphism of o3,o4; :: thesis: c * (b * a) = (c * b) * a

A4: ( <^o2,o4^> <> {} & c * b = ( the Comp of C . (o2,o3,o4)) . (c,b) ) by A2, A3, Def2, Def8;

A5: the Comp of C is associative by Def15;

( <^o1,o3^> <> {} & b * a = ( the Comp of C . (o1,o2,o3)) . (b,a) ) by A1, A2, Def2, Def8;

hence c * (b * a) = ( the Comp of C . (o1,o3,o4)) . (c,(( the Comp of C . (o1,o2,o3)) . (b,a))) by A3, Def8

.= ( the Comp of C . (o1,o2,o4)) . ((( the Comp of C . (o2,o3,o4)) . (c,b)),a) by A1, A2, A3, A5

.= (c * b) * a by A1, A4, Def8 ;

:: thesis: verum