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) by VALUED_1:def 5;
A2: Im r = 0 by COMPLEX1:def 2;
A3: dom (Re f) = dom f by COMSEQ_3:def 3;
A4: Re r = r by COMPLEX1:def 1;
A5: dom (r (#) f) = dom f by VALUED_1:def 5;
A6: dom (Re (r (#) f)) = dom (r (#) f) by COMSEQ_3:def 3;

now

let x be set ; :: thesis: ( x in dom (r (#) (Re f)) implies (r (#) (Re f)) . x = (Re (r (#) f)) . x )
A7: Re (r * (f . x)) = ((Re r) * (Re (f . x))) - ((Im r) * (Im (f . x))) by COMPLEX1:9;
assume A8: x in dom (r (#) (Re f)) ; :: thesis: (r (#) (Re f)) . x = (Re (r (#) f)) . x
then A9: (Re f) . x = Re (f . x) by A1, COMSEQ_3:def 3;
(Re (r (#) f)) . x = Re ((r (#) f) . x) by A1, A5, A6, A3, A8, COMSEQ_3:def 3;
then (Re (r (#) f)) . x = r * (Re (f . x)) by A1, A5, A3, A4, A2, A8, A7, VALUED_1:def 5;
hence (r (#) (Re f)) . x = (Re (r (#) f)) . x by A8, A9, VALUED_1:def 5; :: thesis: verum

end;

hence r (#) (Re f) = Re (r (#) f) by A1, A5, A6, A3, FUNCT_1:2; :: thesis: r (#) (Im f) = Im (r (#) f)
A10: dom (r (#) (Im f)) = dom (Im f) by VALUED_1:def 5;
A11: dom (Im f) = dom f by COMSEQ_3:def 4;
A12: dom (Im (r (#) f)) = dom (r (#) f) by COMSEQ_3:def 4;

now

let x be set ; :: thesis: ( x in dom (r (#) (Im f)) implies (r (#) (Im f)) . x = (Im (r (#) f)) . x )
A13: Im (r * (f . x)) = ((Im r) * (Re (f . x))) + ((Re r) * (Im (f . x))) by COMPLEX1:9;
assume A14: x in dom (r (#) (Im f)) ; :: thesis: (r (#) (Im f)) . x = (Im (r (#) f)) . x
then A15: (Im f) . x = Im (f . x) by A10, COMSEQ_3:def 4;
(Im (r (#) f)) . x = Im ((r (#) f) . x) by A10, A5, A12, A11, A14, COMSEQ_3:def 4;
then (Im (r (#) f)) . x = r * (Im (f . x)) by A10, A5, A11, A4, A2, A14, A13, VALUED_1:def 5;
hence (r (#) (Im f)) . x = (Im (r (#) f)) . x by A14, A15, VALUED_1:def 5; :: thesis: verum

end;

hence r (#) (Im f) = Im (r (#) f) by A10, A5, A12, A11, FUNCT_1:2; :: thesis: verum