let a, b be Complex; for A being non empty set
for f being Element of PFuncs (A,COMPLEX) holds (addcpfunc A) . (((multcomplexcpfunc A) . (a,f)),((multcomplexcpfunc A) . (b,f))) = (multcomplexcpfunc A) . ((a + b),f)
let A be non empty set ; for f being Element of PFuncs (A,COMPLEX) holds (addcpfunc A) . (((multcomplexcpfunc A) . (a,f)),((multcomplexcpfunc A) . (b,f))) = (multcomplexcpfunc A) . ((a + b),f)
let f be Element of PFuncs (A,COMPLEX); (addcpfunc A) . (((multcomplexcpfunc A) . (a,f)),((multcomplexcpfunc A) . (b,f))) = (multcomplexcpfunc A) . ((a + b),f)
reconsider a = a, b = b as Element of COMPLEX by XCMPLX_0:def 2;
reconsider c = a + b as Element of COMPLEX by XCMPLX_0:def 2;
reconsider g = (multcomplexcpfunc A) . (a,f) as Element of PFuncs (A,COMPLEX) ;
reconsider h = (multcomplexcpfunc A) . (b,f) as Element of PFuncs (A,COMPLEX) ;
reconsider k = (multcomplexcpfunc A) . (c,f) as Element of PFuncs (A,COMPLEX) ;
set j = (addcpfunc A) . (g,h);
dom g = dom f
by Th7;
then
(dom h) /\ (dom g) = (dom f) /\ (dom f)
by Th7;
then A1:
dom ((addcpfunc A) . (g,h)) = dom f
by Th4;
A2:
now for x being Element of A st x in dom ((addcpfunc A) . (g,h)) holds
((addcpfunc A) . (g,h)) . x = k . xlet x be
Element of
A;
( x in dom ((addcpfunc A) . (g,h)) implies ((addcpfunc A) . (g,h)) . x = k . x )assume A3:
x in dom ((addcpfunc A) . (g,h))
;
((addcpfunc A) . (g,h)) . x = k . xthen
x in dom (b (#) f)
by A1, VALUED_1:def 5;
then
(b (#) f) . x = b * (f . x)
by VALUED_1:def 5;
then A4:
h . x = b * (f . x)
by Def4;
x in dom (a (#) f)
by A1, A3, VALUED_1:def 5;
then
(a (#) f) . x = a * (f . x)
by VALUED_1:def 5;
then
g . x = a * (f . x)
by Def4;
then
(g . x) + (h . x) = (a + b) * (f . x)
by A4;
hence ((addcpfunc A) . (g,h)) . x =
(a + b) * (f . x)
by A3, Th4
.=
k . x
by A1, A3, Th7
;
verum end;
dom k = dom f
by Th7;
hence
(addcpfunc A) . (((multcomplexcpfunc A) . (a,f)),((multcomplexcpfunc A) . (b,f))) = (multcomplexcpfunc A) . ((a + b),f)
by A1, A2, PARTFUN1:5; verum