let A be Subset of REAL; :: thesis: for x being Real st x <> 0 holds
(x ") ** (x ** A) = A
let x be Real; :: thesis: ( x <> 0 implies (x ") ** (x ** A) = A )
assume A1: x <> 0 ; :: thesis: (x ") ** (x ** A) = A
thus (x ") ** (x ** A) c= A :: according to XBOOLE_0:def 10 :: thesis: A c= (x ") ** (x ** A)

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in (x ") ** (x ** A) or y in A )
assume A2: y in (x ") ** (x ** A) ; :: thesis: y in A
consider z being Real such that
A3: z in x ** A and
A4: y = (x ") * z by A2, INTEGRA2:39;
consider t being Real such that
A5: t in A and
A6: z = x * t by A3, INTEGRA2:39;
y = ((x ") * x) * t by A4, A6
.= 1 * t by A1, XCMPLX_0:def 7
.= t ;
hence y in A by A5; :: thesis: verum

end;

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in A or y in (x ") ** (x ** A) )
assume A7: y in A ; :: thesis: y in (x ") ** (x ** A)
then reconsider y = y as Real ;
set t = y / (x ");
A8: y / (x ") in x ** A by A7, MEMBER_1:193;
y = (x ") * (y / (x ")) by A1, XCMPLX_1:87, XCMPLX_1:202;
hence y in (x ") ** (x ** A) by A8, MEMBER_1:193; :: thesis: verum