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

now :: thesis: for x being object st x in dom (r (#) (Re f)) holds
(r (#) (Re f)) . x = (Re (r (#) f)) . x

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

end;

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

now :: thesis: for x being object st x in dom (r (#) (Im f)) holds
(r (#) (Im f)) . x = (Im (r (#) f)) . x

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

end;

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