let X be non empty set ; for f, g being PartFunc of X,COMPLEX holds
( Re (f + g) = (Re f) + (Re g) & Im (f + g) = (Im f) + (Im g) )
let f, g be PartFunc of X,COMPLEX; ( Re (f + g) = (Re f) + (Re g) & Im (f + g) = (Im f) + (Im g) )
A1:
dom (Re (f + g)) = dom (f + g)
by COMSEQ_3:def 3;
A2:
dom (Re g) = dom g
by COMSEQ_3:def 3;
A3:
dom (Re f) = dom f
by COMSEQ_3:def 3;
then
dom ((Re f) + (Re g)) = (dom f) /\ (dom g)
by A2, VALUED_1:def 1;
then A4:
dom (Re (f + g)) = dom ((Re f) + (Re g))
by A1, VALUED_1:def 1;
now for x being object st x in dom (Re (f + g)) holds
(Re (f + g)) . x = ((Re f) + (Re g)) . xlet x be
object ;
( x in dom (Re (f + g)) implies (Re (f + g)) . x = ((Re f) + (Re g)) . x )assume A5:
x in dom (Re (f + g))
;
(Re (f + g)) . x = ((Re f) + (Re g)) . xthen
(Re (f + g)) . x = Re ((f + g) . x)
by COMSEQ_3:def 3;
then
(Re (f + g)) . x = Re ((f . x) + (g . x))
by A1, A5, VALUED_1:def 1;
then A6:
(Re (f + g)) . x = (Re (f . x)) + (Re (g . x))
by COMPLEX1:8;
A7:
x in (dom f) /\ (dom g)
by A1, A5, VALUED_1:def 1;
then
x in dom (Re g)
by A2, XBOOLE_0:def 4;
then A8:
(Re g) . x = Re (g . x)
by COMSEQ_3:def 3;
x in dom (Re f)
by A3, A7, XBOOLE_0:def 4;
then
(Re f) . x = Re (f . x)
by COMSEQ_3:def 3;
hence
(Re (f + g)) . x = ((Re f) + (Re g)) . x
by A4, A5, A6, A8, VALUED_1:def 1;
verum end;
hence
Re (f + g) = (Re f) + (Re g)
by A4, FUNCT_1:2; Im (f + g) = (Im f) + (Im g)
A9:
dom (Im (f + g)) = dom (f + g)
by COMSEQ_3:def 4;
A10:
dom (Im g) = dom g
by COMSEQ_3:def 4;
A11:
dom (Im f) = dom f
by COMSEQ_3:def 4;
then
dom ((Im f) + (Im g)) = (dom f) /\ (dom g)
by A10, VALUED_1:def 1;
then A12:
dom (Im (f + g)) = dom ((Im f) + (Im g))
by A9, VALUED_1:def 1;
now for x being object st x in dom (Im (f + g)) holds
(Im (f + g)) . x = ((Im f) + (Im g)) . xlet x be
object ;
( x in dom (Im (f + g)) implies (Im (f + g)) . x = ((Im f) + (Im g)) . x )assume A13:
x in dom (Im (f + g))
;
(Im (f + g)) . x = ((Im f) + (Im g)) . xthen
(Im (f + g)) . x = Im ((f + g) . x)
by COMSEQ_3:def 4;
then
(Im (f + g)) . x = Im ((f . x) + (g . x))
by A9, A13, VALUED_1:def 1;
then A14:
(Im (f + g)) . x = (Im (f . x)) + (Im (g . x))
by COMPLEX1:8;
A15:
x in (dom f) /\ (dom g)
by A9, A13, VALUED_1:def 1;
then
x in dom (Im g)
by A10, XBOOLE_0:def 4;
then A16:
(Im g) . x = Im (g . x)
by COMSEQ_3:def 4;
x in dom (Im f)
by A11, A15, XBOOLE_0:def 4;
then
(Im f) . x = Im (f . x)
by COMSEQ_3:def 4;
hence
(Im (f + g)) . x = ((Im f) + (Im g)) . x
by A12, A13, A14, A16, VALUED_1:def 1;
verum end;
hence
Im (f + g) = (Im f) + (Im g)
by A12, FUNCT_1:2; verum