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 Def3;
hence [*(Re z),(Im z)*] = Re z by ARYTM_0:def 7
.= z by A2, Def2 ;
:: thesis: verum

end;

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

then consider f being Function of 2,REAL such that
A4: z = f and
A5: Im z = f . 1 by Def3;
consider f being Function of 2,REAL such that
A6: z = f and
A7: Re z = f . 0 by A3, Def2;
consider a, b being Element of REAL such that
A8: z = 0 ,1 --> a,b by A4, Th5;
A9: Re z = a by A6, A7, A8, FUNCT_4:66;
A10: Im z = b by A4, A5, A8, 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 A11: 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 A8, CARD_1:88, FUNCT_2:11;
f . 1 <> 0 by A11;
then b <> 0 by A8, FUNCT_4:66;
hence [*(Re z),(Im z)*] = z by A8, A9, A10, ARYTM_0:def 7; :: thesis: verum

end;

end;