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

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

consider x1 being Element of X such that

A2: x * x1 = 1. X by A1;

A3: x is right_mult-cancelable

proof

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 " )
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;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

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