let x be Real; :: thesis: ( x <> 0 implies for A being Subset of REAL st A = REAL holds
x ** A = A )
assume A1: x <> 0 ; :: thesis: for A being Subset of REAL st A = REAL holds
x ** A = A
let A be Subset of REAL; :: thesis: ( A = REAL implies x ** A = A )
assume A2: A = REAL ; :: thesis: x ** A = A
for y being object st y in A holds
y in x ** A

proof

let y be object ; :: thesis: ( y in A implies y in x ** A )
assume y in A ; :: thesis: y in x ** A
then reconsider y = y as Real ;
reconsider z = y / x as Element of REAL by XREAL_0:def 1;
y = x * z by A1, XCMPLX_1:87;
hence y in x ** A by A2, MEMBER_1:193; :: thesis: verum

end;

then A c= x ** A ;
hence x ** A = A by A2; :: thesis: verum