let a, b be Element of multEX_0; :: thesis: ( a <> 0. multEX_0 implies ex x being Element of multEX_0 st a * x = b )
assume A1: a <> 0. multEX_0 ; :: thesis: ex x being Element of multEX_0 st a * x = b
reconsider p = a, q = b as Real ;
consider r being Real such that
A2: p * r = q by A1, Th32;
reconsider x = r as Element of multEX_0 ;
a * x = b by A2, BINOP_2:def 11;
hence ex x being Element of multEX_0 st a * x = b ; :: thesis: verum