let C be category; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( <^o1,o2^> <> {} & <^o2,o3^> <> {} & <^o3,o1^> <> {} & A is iso & B is iso implies ( B * A is iso & (B * A) " = (A " ) * (B " ) ) )
assume A1: ( <^o1,o2^> <> {} & <^o2,o3^> <> {} & <^o3,o1^> <> {} ) ; :: thesis: ( not A is iso or not B is iso or ( B * A is iso & (B * A) " = (A " ) * (B " ) ) )
then A2: ( <^o2,o1^> <> {} & <^o3,o2^> <> {} & <^o1,o3^> <> {} ) by ALTCAT_1:def 4;
assume ( A is iso & B is iso ) ; :: thesis: ( B * A is iso & (B * A) " = (A " ) * (B " ) )
then A3: ( A is retraction & A is coretraction & B is retraction & B is coretraction ) by A1, A2, Th6;
consider A1 being Morphism of o2,o1 such that
A4: A1 = A " ;
consider B1 being Morphism of o3,o2 such that
A5: B1 = B " ;
A6: (A1 * B1) * (B * A) = A1 * (B1 * (B * A)) by A2, ALTCAT_1:25
.= A1 * ((B1 * B) * A) by A1, A2, ALTCAT_1:25
.= A1 * ((idm o2) * A) by A1, A2, A3, A5, Th2
.= A1 * A by A1, ALTCAT_1:24
.= idm o1 by A1, A2, A3, A4, Th2 ;
then A7: A1 * B1 is_left_inverse_of B * A by Def1;
then A8: B * A is coretraction by Def3;
A9: (B * A) * (A1 * B1) = B * (A * (A1 * B1)) by A1, ALTCAT_1:25
.= B * ((A * A1) * B1) by A1, A2, ALTCAT_1:25
.= B * ((idm o2) * B1) by A1, A2, A3, A4, Th2
.= B * B1 by A2, ALTCAT_1:24
.= idm o3 by A1, A2, A3, A5, Th2 ;
then A10: A1 * B1 is_right_inverse_of B * A by Def1;
then B * A is retraction by Def2;
then A1 * B1 = (B * A) " by A1, A2, A7, A8, A10, Def4;
hence ( B * A is iso & (B * A) " = (A " ) * (B " ) ) by A4, A5, A6, A9, Def5; :: thesis: verum