let a, b be Element of F_Real; :: thesis: ( a <> 0. F_Real implies ex x being Element of F_Real st x * a = b )

assume a <> 0. F_Real ; :: thesis: ex x being Element of F_Real st x * a = b

then ex x being Element of F_Real st a * x = b by Lm2;

hence ex x being Element of F_Real st x * a = b ; :: thesis: verum

assume a <> 0. F_Real ; :: thesis: ex x being Element of F_Real st x * a = b

then ex x being Element of F_Real st a * x = b by Lm2;

hence ex x being Element of F_Real st x * a = b ; :: thesis: verum