consider B1 being Morphism of o2,o1 such that
A1: B1 is_right_inverse_of A by B3, 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
A2: B2 is_left_inverse_of A by B3, Def3;
B1 = (idm o1) * B1 by B2, ALTCAT_1:20
.= (B2 * A) * B1 by A2, Def1
.= B2 * (A * B1) by B1, B2, ALTCAT_1:21
.= B2 * (idm o2) by A1, Def1
.= B2 by B2, ALTCAT_1:def 17 ;
hence ( B1 is_left_inverse_of A & B1 is_right_inverse_of A ) by A1, A2; :: thesis: verum