let a, b be Element of F_Real ; :: thesis: ( a <> 0. F_Real implies ex x being Element of F_Real st a * x = b )
assume A1: a <> 0. F_Real ; :: thesis: ex x being Element of F_Real st a * x = b
reconsider p = a, q = b as Real by VECTSP_1:def 15;
consider r being Real such that
A2: p * r = q by A1, Lm1, ALGSTR_1:32;
reconsider x = r as Element of F_Real by VECTSP_1:def 15;
a * x = b by A2;
hence ex x being Element of F_Real st a * x = b ; :: thesis: verum