let a, b be Element of REAL ; :: thesis: ( Re [*a,b*] = a & Im [*a,b*] = b )
reconsider a9 = a, b9 = b as Element of REAL ;
thus Re [*a,b*] = a :: thesis: Im [*a,b*] = b

proof

per cases ( b = 0 or b <> 0 ) ;

suppose b = 0 ; :: thesis: Re [*a,b*] = a

then [*a,b*] = a by ARYTM_0:def 5;
hence Re [*a,b*] = a by Def1; :: thesis: verum

end;

suppose b <> 0 ; :: thesis: Re [*a,b*] = a

then A1: [*a,b*] = (0,1) --> (a9,b9) by ARYTM_0:def 5;
then reconsider f = [*a,b*] as Function of 2,REAL by CARD_1:50;
A2: ( not [*a,b*] in REAL & f . 0 = a ) by A1, ARYTM_0:8, FUNCT_4:63;
then not [*a,b*] is real by XREAL_0:def 1;
hence Re [*a,b*] = a by Def1, A2; :: thesis: verum

end;

end;

end;

per cases ( b = 0 or b <> 0 ) ;

suppose A2: b = 0 ; :: thesis: Im [*a,b*] = b

then [*a,b*] = a by ARYTM_0:def 5;
hence Im [*a,b*] = b by A2; :: thesis: verum

end;

suppose b <> 0 ; :: thesis: Im [*a,b*] = b

then A3: [*a,b*] = (0,1) --> (a9,b9) by ARYTM_0:def 5;
then reconsider f = [*a,b*] as Function of 2,REAL by CARD_1:50;
A4: ( not [*a,b*] in REAL & f . 1 = b ) by A3, ARYTM_0:8, FUNCT_4:63;
then not [*a,b*] is real by XREAL_0:def 1;
hence Im [*a,b*] = b by Def2, A4; :: thesis: verum

end;

end;