let y be Element of X; :: thesis: ( y = x " iff ( x * y = 1. X & y * x = 1. X ) )
A2: x is left_invertible by A1;
x is right_invertible by A1;
then consider x1 being Element of X such that
A3: x * x1 = 1. X by ALGSTR_0:def 28;
A4: x is right_mult-cancelable

proof

let y, z be Element of X; :: according to ALGSTR_0:def 21 :: thesis: ( not y * x = z * x or y = z )
assume A5: y * x = z * x ; :: thesis: y = z
thus y = y * (1. X) by VECTSP_1:def 16
.= (z * x) * x1 by A3, A5, GROUP_1:def 4
.= z * (1. X) by A3, GROUP_1:def 4
.= z by VECTSP_1:def 16 ; :: thesis: verum

end;

thus ( y = x " implies ( x * y = 1. X & y * x = 1. X ) ) :: thesis: ( x * y = 1. X & y * x = 1. X implies y = x " )

proof

assume A6: y = x " ; :: thesis: ( x * y = 1. X & y * x = 1. X )
y = y * (1. X) by VECTSP_1:def 16
.= (y * x) * x1 by A3, GROUP_1:def 4
.= (1. X) * x1 by A2, A4, A6, ALGSTR_0:def 30
.= x1 by VECTSP_1:def 16 ;
hence x * y = 1. X by A3; :: thesis: y * x = 1. X
thus y * x = 1. X by A2, A4, A6, ALGSTR_0:def 30; :: thesis: verum

end;

thus ( x * y = 1. X & y * x = 1. X implies y = x " ) by A2, A4, ALGSTR_0:def 30; :: thesis: verum