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 consider x being Element of F_Real such that
A1: a * x = b by Lm2;
thus ex x being Element of F_Real st x * a = b by A1; :: thesis: verum