consider B1 being Morphism of o2,o1 such that
A4: B1 is_right_inverse_of A by A3, Def2;
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, Def3;
B1 = (idm o1) * B1 by A2, ALTCAT_1:24
.= (B2 * A) * B1 by A5, Def1
.= B2 * (A * B1) by A1, A2, ALTCAT_1:25
.= B2 * (idm o2) by A4, Def1
.= B2 by A2, ALTCAT_1:def 19 ;
hence ( B1 is_left_inverse_of A & B1 is_right_inverse_of A ) by A4, A5; :: thesis: verum