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