let X be non empty set ; :: thesis: for f being PartFunc of X,COMPLEX
for r being Real holds
( r (#) (Re f) = Re (r (#) f) & r (#) (Im f) = Im (r (#) f) )
let f be PartFunc of X,COMPLEX ; :: thesis: for r being Real holds
( r (#) (Re f) = Re (r (#) f) & r (#) (Im f) = Im (r (#) f) )
let r be Real; :: thesis: ( r (#) (Re f) = Re (r (#) f) & r (#) (Im f) = Im (r (#) f) )
A1: ( dom (r (#) (Re f)) = dom (Re f) & dom (r (#) (Im f)) = dom (Im f) & dom (r (#) f) = dom f ) by VALUED_1:def 5;
A2: ( dom (Re (r (#) f)) = dom (r (#) f) & dom (Re f) = dom f ) by Def1;
A3: ( dom (Im (r (#) f)) = dom (r (#) f) & dom (Im f) = dom f ) by Def2;
A4: ( Re r = r & Im r = 0 ) by COMPLEX1:def 2, COMPLEX1:def 3;

now

let x be set ; :: thesis: ( x in dom (r (#) (Re f)) implies (r (#) (Re f)) . x = (Re (r (#) f)) . x )
assume A5: x in dom (r (#) (Re f)) ; :: thesis: (r (#) (Re f)) . x = (Re (r (#) f)) . x
then A6: ( (Re f) . x = Re (f . x) & (Re (r (#) f)) . x = Re ((r (#) f) . x) ) by A1, A2, Def1;
Re (r * (f . x)) = ((Re r) * (Re (f . x))) - ((Im r) * (Im (f . x))) by COMPLEX1:24;
then (Re (r (#) f)) . x = r * (Re (f . x)) by A1, A4, A5, A6, A2, VALUED_1:def 5;
hence (r (#) (Re f)) . x = (Re (r (#) f)) . x by A5, A6, VALUED_1:def 5; :: thesis: verum

end;

hence r (#) (Re f) = Re (r (#) f) by A1, A2, FUNCT_1:9; :: thesis: r (#) (Im f) = Im (r (#) f)

now

let x be set ; :: thesis: ( x in dom (r (#) (Im f)) implies (r (#) (Im f)) . x = (Im (r (#) f)) . x )
assume A7: x in dom (r (#) (Im f)) ; :: thesis: (r (#) (Im f)) . x = (Im (r (#) f)) . x
then A8: ( (Im f) . x = Im (f . x) & (Im (r (#) f)) . x = Im ((r (#) f) . x) ) by A1, A3, Def2;
Im (r * (f . x)) = ((Im r) * (Re (f . x))) + ((Re r) * (Im (f . x))) by COMPLEX1:24;
then (Im (r (#) f)) . x = r * (Im (f . x)) by A1, A4, A7, A8, A3, VALUED_1:def 5;
hence (r (#) (Im f)) . x = (Im (r (#) f)) . x by A7, A8, VALUED_1:def 5; :: thesis: verum

end;

hence r (#) (Im f) = Im (r (#) f) by A1, A3, FUNCT_1:9; :: thesis: verum