let C be category; 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; 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; 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; 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; 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; ( 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^> <> {}
; c * (a ") = (d ") * b
A9:
<^o2,o4^> <> {}
by A6, A7, ALTCAT_1:def 2;
<^o1,o3^> <> {}
by A4, A6, ALTCAT_1:def 2;
then A10:
<^o1,o4^> <> {}
by A7, ALTCAT_1:def 2;
b =
b * (idm o2)
by A6, ALTCAT_1:def 17
.=
(b * a) * (a ")
by A2, A4, A5, A6, ALTCAT_1:21
;
hence (d ") * b =
(d ") * (d * (c * (a ")))
by A1, A5, A8, A10, ALTCAT_1:21
.=
((d ") * d) * (c * (a "))
by A7, A8, A9, ALTCAT_1:21
.=
c * (a ")
by A3, A9, ALTCAT_1:20
;
verum