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;
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 ) ) by A1, A3, ALGSTR_0:def 30; :: thesis: ( x * y = 1. X & y * x = 1. X implies y = x " )
thus ( x * y = 1. X & y * x = 1. X implies y = x " ) by A1, A3, ALGSTR_0:def 30; :: thesis: verum