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

per cases ( z is real or not z is real ) ;

suppose A2: z is real ; :: thesis: [*(Re z),(Im z)*] = z

then Im z = 0 ;
hence [*(Re z),(Im z)*] = Re z by ARYTM_0:def 5
.= z by A2, Def1 ;
:: thesis: verum

end;

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

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

end;

end;