let y be Element of X; :: thesis: ( y = x " iff ( x * y = 1. X & y * x = 1. X ) )
consider x1 being Element of X such that
A2: x * x1 = 1. X by A1, ALGSTR_0:def 28;
A3: 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 A4: y * x = z * x ; :: thesis: y = z
thus y = y * (1. X) by VECTSP_1:def 6
.= (z * x) * x1 by A2, A4, GROUP_1:def 3
.= z * (1. X) by A2, GROUP_1:def 3
.= z by VECTSP_1:def 6 ; :: 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 A5: y = x " ; :: thesis: ( x * y = 1. X & y * x = 1. X )
y = y * (1. X) by VECTSP_1:def 6
.= (y * x) * x1 by A2, GROUP_1:def 3
.= (1. X) * x1 by A1, A3, A5, ALGSTR_0:def 30
.= x1 by VECTSP_1:def 6 ;
hence x * y = 1. X by A2; :: thesis: y * x = 1. X
thus y * x = 1. X by A1, A3, A5, ALGSTR_0:def 30; :: thesis: verum

end;

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