let C be category; for o1, o2, o3 being Object of C
for A being Morphism of o1,o2
for B being Morphism of o2,o3 st <^o1,o2^> <> {} & <^o2,o3^> <> {} & <^o3,o1^> <> {} & A is iso & B is iso holds
( B * A is iso & (B * A) " = (A ") * (B ") )
let o1, o2, o3 be Object of C; for A being Morphism of o1,o2
for B being Morphism of o2,o3 st <^o1,o2^> <> {} & <^o2,o3^> <> {} & <^o3,o1^> <> {} & A is iso & B is iso holds
( B * A is iso & (B * A) " = (A ") * (B ") )
let A be Morphism of o1,o2; for B being Morphism of o2,o3 st <^o1,o2^> <> {} & <^o2,o3^> <> {} & <^o3,o1^> <> {} & A is iso & B is iso holds
( B * A is iso & (B * A) " = (A ") * (B ") )
let B be Morphism of o2,o3; ( <^o1,o2^> <> {} & <^o2,o3^> <> {} & <^o3,o1^> <> {} & A is iso & B is iso implies ( B * A is iso & (B * A) " = (A ") * (B ") ) )
assume that
A1:
<^o1,o2^> <> {}
and
A2:
<^o2,o3^> <> {}
and
A3:
<^o3,o1^> <> {}
; ( not A is iso or not B is iso or ( B * A is iso & (B * A) " = (A ") * (B ") ) )
assume that
A4:
A is iso
and
A5:
B is iso
; ( B * A is iso & (B * A) " = (A ") * (B ") )
consider A1 being Morphism of o2,o1 such that
A6:
A1 = A "
;
A7:
<^o2,o1^> <> {}
by A2, A3, ALTCAT_1:def 2;
then A8:
( A is retraction & A is coretraction )
by A1, A4, Th6;
consider B1 being Morphism of o3,o2 such that
A9:
B1 = B "
;
A10:
<^o3,o2^> <> {}
by A1, A3, ALTCAT_1:def 2;
then A11:
( B is retraction & B is coretraction )
by A2, A5, Th6;
A12: (B * A) * (A1 * B1) =
B * (A * (A1 * B1))
by A1, A2, A3, ALTCAT_1:21
.=
B * ((A * A1) * B1)
by A1, A7, A10, ALTCAT_1:21
.=
B * ((idm o2) * B1)
by A1, A7, A8, A6, Th2
.=
B * B1
by A10, ALTCAT_1:20
.=
idm o3
by A2, A10, A11, A9, Th2
;
then A13:
A1 * B1 is_right_inverse_of B * A
;
then A14:
B * A is retraction
;
A15:
<^o1,o3^> <> {}
by A1, A2, ALTCAT_1:def 2;
then A16: (A1 * B1) * (B * A) =
A1 * (B1 * (B * A))
by A7, A10, ALTCAT_1:21
.=
A1 * ((B1 * B) * A)
by A1, A2, A10, ALTCAT_1:21
.=
A1 * ((idm o2) * A)
by A2, A10, A11, A9, Th2
.=
A1 * A
by A1, ALTCAT_1:20
.=
idm o1
by A1, A7, A8, A6, Th2
;
then A17:
A1 * B1 is_left_inverse_of B * A
;
then
B * A is coretraction
;
then
A1 * B1 = (B * A) "
by A3, A15, A17, A13, A14, Def4;
hence
( B * A is iso & (B * A) " = (A ") * (B ") )
by A6, A9, A16, A12; verum