let X be non empty set ; 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; for r being Real holds
( r (#) (Re f) = Re (r (#) f) & r (#) (Im f) = Im (r (#) f) )
let r be Real; ( 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 for x being object st x in dom (r (#) (Re f)) holds
(r (#) (Re f)) . x = (Re (r (#) f)) . xlet x be
object ;
( 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))
;
(r (#) (Re f)) . x = (Re (r (#) f)) . xthen 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;
verum end;
hence
r (#) (Re f) = Re (r (#) f)
by A1, A6, A7, A4, FUNCT_1:2; 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 for x being object st x in dom (r (#) (Im f)) holds
(r (#) (Im f)) . x = (Im (r (#) f)) . xlet x be
object ;
( 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))
;
(r (#) (Im f)) . x = (Im (r (#) f)) . xthen 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;
verum end;
hence
r (#) (Im f) = Im (r (#) f)
by A11, A6, A13, A12, FUNCT_1:2; verum