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 COMPLEX1:def 1; :: 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;
not [*a,b*] in REAL by A1, ARYTM_0:8;
then a2: not [*a,b*] is real by XREAL_0:def 1;
f . 0 = a by A1, FUNCT_4:63;
hence Re [*a,b*] = a by a2, COMPLEX1:def 1; :: thesis: verum

end;

end;

end;

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

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

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

end;

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

then A4: [*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;
not [*a,b*] in REAL by A4, ARYTM_0:8;
then a5: not [*a,b*] is real by XREAL_0:def 1;
f . 1 = b by A4, FUNCT_4:63;
hence Im [*a,b*] = b by a5, COMPLEX1:def 2; :: thesis: verum

end;

end;