let z be complex number ; :: thesis: [*(Re z),(Im z)*] = z
A1: z in COMPLEX by XCMPLX_0:def 2;

per cases ( z in REAL or not z in REAL ) ;

suppose A2: z in REAL ; :: thesis: [*(Re z),(Im z)*] = z

then Im z = 0 by COMPLEX1:def 3;
hence [*(Re z),(Im z)*] = Re z by ARYTM_0:def 7
.= z by A2, COMPLEX1:def 2 ;
:: thesis: verum

end;

suppose A3: not z in REAL ; :: thesis: [*(Re z),(Im z)*] = z

then A4: ex f being Function of 2,REAL st
( z = f & Im z = f . 1 ) by COMPLEX1:def 3;
A5: ex f being Function of 2,REAL st
( z = f & Re z = f . 0 ) by A3, COMPLEX1:def 2;
consider a, b being Element of REAL such that
A6: z = 0 ,1 --> a,b by A4, COMPLEX1:5;
A7: Re z = a by A5, A6, FUNCT_4:66;
A8: Im z = b by A4, A6, FUNCT_4:66;
z in (Funcs 2,REAL ) \ { x where x is Element of Funcs 2,REAL : x . 1 = 0 } by A1, A3, CARD_1:88, NUMBERS:def 2, XBOOLE_0:def 3;
then A9: not z in { x where x is Element of Funcs 2,REAL : x . 1 = 0 } by XBOOLE_0:def 5;
reconsider f = z as Element of Funcs 2,REAL by A6, CARD_1:88, FUNCT_2:11;
f . 1 <> 0 by A9;
then b <> 0 by A6, FUNCT_4:66;
hence [*(Re z),(Im z)*] = z by A6, A7, A8, ARYTM_0:def 7; :: thesis: verum

end;

end;