let z be Complex; :: 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 2;
hence [*(Re z),(Im z)*] = Re z by ARYTM_0:def 5
.= z by A2, COMPLEX1:def 1 ;
:: thesis: verum

end;

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

then a3: not z is real by XREAL_0:def 1;
then A4: ex f being Function of 2,REAL st
( z = f & Im z = f . 1 ) by COMPLEX1:def 2;
A5: ex f being Function of 2,REAL st
( z = f & Re z = f . 0 ) by a3, COMPLEX1:def 1;
consider a, b being Element of REAL such that
A6: z = (0,1) --> (a,b) by A4, COMPLEX1:2;
A7: Re z = a by A5, A6, FUNCT_4:63;
A8: Im z = b by A4, A6, FUNCT_4:63;
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 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:50, FUNCT_2:8;
f . 1 <> 0 by A9;
then b <> 0 by A6, FUNCT_4:63;
hence [*(Re z),(Im z)*] = z by A6, A7, A8, ARYTM_0:def 5; :: thesis: verum

end;

end;