let X be non empty set ; for f, g being PartFunc of X,COMPLEX holds
( Re (f (#) g) = ((Re f) (#) (Re g)) - ((Im f) (#) (Im g)) & Im (f (#) g) = ((Im f) (#) (Re g)) + ((Re f) (#) (Im g)) )
let f, g be PartFunc of X,COMPLEX; ( Re (f (#) g) = ((Re f) (#) (Re g)) - ((Im f) (#) (Im g)) & Im (f (#) g) = ((Im f) (#) (Re g)) + ((Re f) (#) (Im g)) )
A1:
dom ((Re f) (#) (Re g)) = (dom (Re f)) /\ (dom (Re g))
by VALUED_1:def 4;
A2:
dom ((Im f) (#) (Im g)) = (dom (Im f)) /\ (dom (Im g))
by VALUED_1:def 4;
A3:
dom (Re f) = dom f
by COMSEQ_3:def 3;
A4:
dom (Im g) = dom g
by COMSEQ_3:def 4;
A5:
dom (Re g) = dom g
by COMSEQ_3:def 3;
A6:
dom (Re (f (#) g)) = dom (f (#) g)
by COMSEQ_3:def 3;
then A7:
dom (Re (f (#) g)) = (dom f) /\ (dom g)
by VALUED_1:def 4;
A8:
dom (Im f) = dom f
by COMSEQ_3:def 4;
A9:
dom (((Re f) (#) (Re g)) - ((Im f) (#) (Im g))) = (dom ((Re f) (#) (Re g))) /\ (dom ((Im f) (#) (Im g)))
by VALUED_1:12;
now for x being object st x in dom (Re (f (#) g)) holds
(Re (f (#) g)) . x = (((Re f) (#) (Re g)) - ((Im f) (#) (Im g))) . xlet x be
object ;
( x in dom (Re (f (#) g)) implies (Re (f (#) g)) . x = (((Re f) (#) (Re g)) - ((Im f) (#) (Im g))) . x )assume A10:
x in dom (Re (f (#) g))
;
(Re (f (#) g)) . x = (((Re f) (#) (Re g)) - ((Im f) (#) (Im 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 A6, A10, VALUED_1:def 4;
then A11:
(Re (f (#) g)) . x = ((Re (f . x)) * (Re (g . x))) - ((Im (f . x)) * (Im (g . x)))
by COMPLEX1:9;
x in dom g
by A7, A10, XBOOLE_0:def 4;
then A12:
(
(Re g) . x = Re (g . x) &
(Im g) . x = Im (g . x) )
by A5, A4, COMSEQ_3:def 3, COMSEQ_3:def 4;
x in dom f
by A7, A10, XBOOLE_0:def 4;
then
(
(Re f) . x = Re (f . x) &
(Im f) . x = Im (f . x) )
by A3, A8, COMSEQ_3:def 3, COMSEQ_3:def 4;
then
(Re (f (#) g)) . x = (((Re f) (#) (Re g)) . x) - (((Im f) . x) * ((Im g) . x))
by A7, A1, A3, A5, A10, A11, A12, VALUED_1:def 4;
then
(Re (f (#) g)) . x = (((Re f) (#) (Re g)) . x) - (((Im f) (#) (Im g)) . x)
by A7, A2, A8, A4, A10, VALUED_1:def 4;
hence
(Re (f (#) g)) . x = (((Re f) (#) (Re g)) - ((Im f) (#) (Im g))) . x
by A7, A9, A1, A2, A3, A8, A5, A4, A10, VALUED_1:13;
verum end;
hence
Re (f (#) g) = ((Re f) (#) (Re g)) - ((Im f) (#) (Im g))
by A7, A9, A1, A2, A3, A8, A5, A4, FUNCT_1:2; Im (f (#) g) = ((Im f) (#) (Re g)) + ((Re f) (#) (Im g))
A13:
dom ((Im f) (#) (Re g)) = (dom (Im f)) /\ (dom (Re g))
by VALUED_1:def 4;
A14:
dom ((Re f) (#) (Im g)) = (dom (Re f)) /\ (dom (Im g))
by VALUED_1:def 4;
A15:
dom (Im (f (#) g)) = dom (f (#) g)
by COMSEQ_3:def 4;
then A16:
dom (Im (f (#) g)) = (dom f) /\ (dom g)
by VALUED_1:def 4;
A17:
dom (((Im f) (#) (Re g)) + ((Re f) (#) (Im g))) = (dom ((Im f) (#) (Re g))) /\ (dom ((Re f) (#) (Im g)))
by VALUED_1:def 1;
now for x being object st x in dom (Im (f (#) g)) holds
(Im (f (#) g)) . x = (((Im f) (#) (Re g)) + ((Re f) (#) (Im g))) . xlet x be
object ;
( x in dom (Im (f (#) g)) implies (Im (f (#) g)) . x = (((Im f) (#) (Re g)) + ((Re f) (#) (Im g))) . x )assume A18:
x in dom (Im (f (#) g))
;
(Im (f (#) g)) . x = (((Im f) (#) (Re g)) + ((Re 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 A15, A18, VALUED_1:def 4;
then A19:
(Im (f (#) g)) . x = ((Im (f . x)) * (Re (g . x))) + ((Re (f . x)) * (Im (g . x)))
by COMPLEX1:9;
x in dom g
by A16, A18, XBOOLE_0:def 4;
then A20:
(
(Re g) . x = Re (g . x) &
(Im g) . x = Im (g . x) )
by A5, A4, COMSEQ_3:def 3, COMSEQ_3:def 4;
x in dom f
by A16, A18, XBOOLE_0:def 4;
then
(
(Re f) . x = Re (f . x) &
(Im f) . x = Im (f . x) )
by A3, A8, COMSEQ_3:def 3, COMSEQ_3:def 4;
then
(Im (f (#) g)) . x = (((Im f) (#) (Re g)) . x) + (((Re f) . x) * ((Im g) . x))
by A16, A13, A8, A5, A18, A19, A20, VALUED_1:def 4;
then
(Im (f (#) g)) . x = (((Im f) (#) (Re g)) . x) + (((Re f) (#) (Im g)) . x)
by A16, A14, A3, A4, A18, VALUED_1:def 4;
hence
(Im (f (#) g)) . x = (((Im f) (#) (Re g)) + ((Re f) (#) (Im g))) . x
by A16, A17, A13, A14, A3, A8, A5, A4, A18, VALUED_1:def 1;
verum end;
hence
Im (f (#) g) = ((Im f) (#) (Re g)) + ((Re f) (#) (Im g))
by A16, A17, A13, A14, A3, A8, A5, A4, FUNCT_1:2; verum