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: the Comp of C is associative by Def17;
A5: <^o1,o3^> <> {} by A1, A2, Def4;
A6: b * a = (the Comp of C . o1,o2,o3) . b,a by A1, A2, Def10;
A7: <^o2,o4^> <> {} by A2, A3, Def4;
A8: c * b = (the Comp of C . o2,o3,o4) . c,b by A2, A3, Def10;
thus c * (b * a) = (the Comp of C . o1,o3,o4) . c,((the Comp of C . o1,o2,o3) . b,a) by A3, A5, A6, Def10
.= (the Comp of C . o1,o2,o4) . ((the Comp of C . o2,o3,o4) . c,b),a by A1, A2, A3, A4, Def7
.= (c * b) * a by A1, A7, A8, Def10 ; :: thesis: verum