let a, b be Element of REAL ; :: thesis: ( Re [*a,b*] = a & Im [*a,b*] = b )
reconsider a' = a, b' = 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 COMPLEX1:def 2; :: thesis: verum

end;

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

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

end;

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

then A4: [*a,b*] = 0 ,1 --> a',b' by ARYTM_0:def 7;
then reconsider f = [*a,b*] as Function of 2,REAL by CARD_1:88;
A5: not [*a,b*] in REAL by A4, ARYTM_0:10;
f . 1 = b by A4, FUNCT_4:66;
hence Im [*a,b*] = b by A5, COMPLEX1:def 3; :: thesis: verum

end;

end;