let A be complex-membered set ; :: thesis: 1 ** A = A
let a be complex number ; :: according to MEMBERED:def 13 :: thesis: ( ( not a in 1 ** A or a in A ) & ( not a in A or a in 1 ** A ) )

hereby :: thesis: ( not a in A or a in 1 ** A )

assume a in 1 ** A ; :: thesis: a in A
then consider c1, c2 being Element of COMPLEX such that
A1: a = c1 * c2 and
A2: c1 in {1} and
A3: c2 in A ;
c1 = 1 by A2, TARSKI:def 1;
hence a in A by A1, A3; :: thesis: verum

end;

assume A4: a in A ; :: thesis: a in 1 ** A
a in COMPLEX by XCMPLX_0:def 2;
then 1 * a in { (1 * c) where c is Element of COMPLEX : c in A } by A4;
hence a in 1 ** A by Th200; :: thesis: verum