consider B1 being Morphism of o2,o1 such that
A4: B1 is_right_inverse_of A by A3;
take B1 ; :: thesis: ( B1 is_left_inverse_of A & B1 is_right_inverse_of A )
consider B2 being Morphism of o2,o1 such that
A5: B2 is_left_inverse_of A by A3;
B1 = (idm o1) * B1 by A2, ALTCAT_1:20
.= (B2 * A) * B1 by A5
.= B2 * (A * B1) by A1, A2, ALTCAT_1:21
.= B2 * (idm o2) by A4
.= B2 by A2, ALTCAT_1:def 17 ;
hence ( B1 is_left_inverse_of A & B1 is_right_inverse_of A ) by A4, A5; :: thesis: verum