let C be category; :: thesis: for o1, o2, o3, o4 being object of C
for a being Morphism of o1,o2
for b being Morphism of o2,o3
for c being Morphism of o1,o4
for d being Morphism of o4,o3 st b * a = d * c & a * (a " ) = idm o2 & (d " ) * d = idm o4 & <^o1,o2^> <> {} & <^o2,o1^> <> {} & <^o2,o3^> <> {} & <^o3,o4^> <> {} & <^o4,o3^> <> {} holds
c * (a " ) = (d " ) * b
let o1, o2, o3, o4 be object of C; :: thesis: for a being Morphism of o1,o2
for b being Morphism of o2,o3
for c being Morphism of o1,o4
for d being Morphism of o4,o3 st b * a = d * c & a * (a " ) = idm o2 & (d " ) * d = idm o4 & <^o1,o2^> <> {} & <^o2,o1^> <> {} & <^o2,o3^> <> {} & <^o3,o4^> <> {} & <^o4,o3^> <> {} holds
c * (a " ) = (d " ) * b
let a be Morphism of o1,o2; :: thesis: for b being Morphism of o2,o3
for c being Morphism of o1,o4
for d being Morphism of o4,o3 st b * a = d * c & a * (a " ) = idm o2 & (d " ) * d = idm o4 & <^o1,o2^> <> {} & <^o2,o1^> <> {} & <^o2,o3^> <> {} & <^o3,o4^> <> {} & <^o4,o3^> <> {} holds
c * (a " ) = (d " ) * b
let b be Morphism of o2,o3; :: thesis: for c being Morphism of o1,o4
for d being Morphism of o4,o3 st b * a = d * c & a * (a " ) = idm o2 & (d " ) * d = idm o4 & <^o1,o2^> <> {} & <^o2,o1^> <> {} & <^o2,o3^> <> {} & <^o3,o4^> <> {} & <^o4,o3^> <> {} holds
c * (a " ) = (d " ) * b
let c be Morphism of o1,o4; :: thesis: for d being Morphism of o4,o3 st b * a = d * c & a * (a " ) = idm o2 & (d " ) * d = idm o4 & <^o1,o2^> <> {} & <^o2,o1^> <> {} & <^o2,o3^> <> {} & <^o3,o4^> <> {} & <^o4,o3^> <> {} holds
c * (a " ) = (d " ) * b
let d be Morphism of o4,o3; :: thesis: ( b * a = d * c & a * (a " ) = idm o2 & (d " ) * d = idm o4 & <^o1,o2^> <> {} & <^o2,o1^> <> {} & <^o2,o3^> <> {} & <^o3,o4^> <> {} & <^o4,o3^> <> {} implies c * (a " ) = (d " ) * b )
assume that
A1: b * a = d * c and
A2: a * (a " ) = idm o2 and
A3: (d " ) * d = idm o4 and
A4: ( <^o1,o2^> <> {} & <^o2,o1^> <> {} & <^o2,o3^> <> {} & <^o3,o4^> <> {} & <^o4,o3^> <> {} ) ; :: thesis: c * (a " ) = (d " ) * b
<^o1,o3^> <> {} by A4, ALTCAT_1:def 4;
then A5: ( <^o1,o4^> <> {} & <^o2,o4^> <> {} ) by A4, ALTCAT_1:def 4;
b = b * (idm o2) by A4, ALTCAT_1:def 19
.= (b * a) * (a " ) by A2, A4, ALTCAT_1:25 ;
hence (d " ) * b = (d " ) * (d * (c * (a " ))) by A1, A4, A5, ALTCAT_1:25
.= ((d " ) * d) * (c * (a " )) by A4, A5, ALTCAT_1:25
.= c * (a " ) by A3, A5, ALTCAT_1:24 ;
:: thesis: verum