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^> <> {} and
A5: <^o2,o1^> <> {} and
A6: <^o2,o3^> <> {} and
A7: <^o3,o4^> <> {} and
A8: <^o4,o3^> <> {} ; :: thesis: c * (a ") = (d ") * b
A9: <^o2,o4^> <> {} by ;
<^o1,o3^> <> {} by ;
then A10: <^o1,o4^> <> {} by ;
b = b * (idm o2) by
.= (b * a) * (a ") by ;
hence (d ") * b = (d ") * (d * (c * (a "))) by
.= ((d ") * d) * (c * (a ")) by
.= c * (a ") by ;
:: thesis: verum