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;

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;

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

hence
r (#) (Re f) = Re (r (#) f)
by A1, A6, A7, A4, FUNCT_1:2; :: thesis: r (#) (Im f) = Im (r (#) f)(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;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

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

hence
r (#) (Im f) = Im (r (#) f)
by A11, A6, A13, A12, FUNCT_1:2; :: thesis: verum(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;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