let IT be Element of F; :: thesis: ( IT = x " iff IT * x = 1. F )

A2: x is left_invertible by A1, ALGSTR_0:def 39;

then consider x1 being Element of F such that

A3: x1 * x = 1. F ;

x is right_mult-cancelable

A2: x is left_invertible by A1, ALGSTR_0:def 39;

then consider x1 being Element of F such that

A3: x1 * x = 1. F ;

x is right_mult-cancelable

proof

hence
( IT = x " iff IT * x = 1. F )
by A2, ALGSTR_0:def 30; :: thesis: verum
let y, z be Element of F; :: 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. F)

.= (z * x) * x1 by A3, A4, GROUP_1:def 3

.= z * (1. F) by A3, GROUP_1:def 3

.= z ; :: thesis: verum

end;assume A4: y * x = z * x ; :: thesis: y = z

thus y = y * (1. F)

.= (z * x) * x1 by A3, A4, GROUP_1:def 3

.= z * (1. F) by A3, GROUP_1:def 3

.= z ; :: thesis: verum