let A be non empty set ; :: thesis: for f being Element of PFuncs (A,COMPLEX) holds (addcpfunc A) . (f,((multcomplexcpfunc A) . ((- 1r),f))) = (CPFuncZero A) | (dom f)
let f be Element of PFuncs (A,COMPLEX); :: thesis: (addcpfunc A) . (f,((multcomplexcpfunc A) . ((- 1r),f))) = (CPFuncZero A) | (dom f)
reconsider g = (multcomplexcpfunc A) . (R,f) as Element of PFuncs (A,COMPLEX) ;
set h = (addcpfunc A) . (f,g);
dom (CPFuncZero A) = A by FUNCOP_1:13;
then dom ((CPFuncZero A) | (dom f)) = A /\ (dom f) by RELAT_1:61;
then A1: dom ((CPFuncZero A) | (dom f)) = dom f by XBOOLE_1:28;
A2: dom ((addcpfunc A) . (f,g)) = (dom g) /\ (dom f) by Th4
.= (dom f) /\ (dom f) by Th7 ;

now :: thesis: for x being Element of A st x in dom f holds
((addcpfunc A) . (f,g)) . x = ((CPFuncZero A) | (dom f)) . x

let x be Element of A; :: thesis: ( x in dom f implies ((addcpfunc A) . (f,g)) . x = ((CPFuncZero A) | (dom f)) . x )
assume A3: x in dom f ; :: thesis: ((addcpfunc A) . (f,g)) . x = ((CPFuncZero A) | (dom f)) . x
then A4: x in dom ((- 1r) (#) f) by VALUED_1:def 5;
thus ((addcpfunc A) . (f,g)) . x = (f . x) + (g . x) by A2, A3, Th4
.= (f . x) + (((- 1r) (#) f) . x) by Def4
.= (f . x) + ((- 1r) * (f . x)) by A4, VALUED_1:def 5
.= (CPFuncZero A) . x by FUNCOP_1:7, COMPLEX1:def 4
.= ((CPFuncZero A) | (dom f)) . x by A3, FUNCT_1:49 ; :: thesis: verum

end;

hence (addcpfunc A) . (f,((multcomplexcpfunc A) . ((- 1r),f))) = (CPFuncZero A) | (dom f) by A1, A2, PARTFUN1:5; :: thesis: verum