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 7;
hence Re [*a,b*] = a by Def2; :: thesis: verum

end;

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

then A1: [*a,b*] = 0 ,1 --> a9,b9 by ARYTM_0:def 7;
then reconsider f = [*a,b*] as Function of 2,REAL by CARD_1:88;
( not [*a,b*] in REAL & f . 0 = a ) by A1, ARYTM_0:10, FUNCT_4:66;
hence Re [*a,b*] = a by Def2; :: 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 7;
hence Im [*a,b*] = b by A2, Def3; :: thesis: verum

end;

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

then A3: [*a,b*] = 0 ,1 --> a9,b9 by ARYTM_0:def 7;
then reconsider f = [*a,b*] as Function of 2,REAL by CARD_1:88;
( not [*a,b*] in REAL & f . 1 = b ) by A3, ARYTM_0:10, FUNCT_4:66;
hence Im [*a,b*] = b by Def3; :: thesis: verum

end;

end;