let A be complex-membered set ; :: thesis: 1 ** A = A
let a be Complex; :: 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 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 a in A ; :: thesis: a in 1 ** A
then 1 * a in { (1 * c) where c is Complex : c in A } ;
hence a in 1 ** A by Th194; :: thesis: verum