let A be non empty set ; :: thesis: CPFuncZero A is_a_unity_wrt addcpfunc A
thus CPFuncZero A is_a_left_unity_wrt addcpfunc A :: according to BINOP_1:def 7 :: thesis: CPFuncZero A is_a_right_unity_wrt addcpfunc A

proof

let f be Element of PFuncs (A,COMPLEX); :: according to BINOP_1:def 16 :: thesis: (addcpfunc A) . ((CPFuncZero A),f) = f
set h = (addcpfunc A) . ((CPFuncZero A),f);
dom ((addcpfunc A) . ((CPFuncZero A),f)) = (dom (CPFuncZero A)) /\ (dom f) by Th4;
then dom ((addcpfunc A) . ((CPFuncZero A),f)) = A /\ (dom f) by FUNCOP_1:13;
then A1: dom ((addcpfunc A) . ((CPFuncZero A),f)) = dom f by XBOOLE_1:28;

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

let x be Element of A; :: thesis: ( x in dom f implies ((addcpfunc A) . ((CPFuncZero A),f)) . x = f . x )
A2: (CPFuncZero A) . x = 0c by FUNCOP_1:7;
assume x in dom f ; :: thesis: ((addcpfunc A) . ((CPFuncZero A),f)) . x = f . x
hence ((addcpfunc A) . ((CPFuncZero A),f)) . x = 0c + (f . x) by A1, A2, Th4
.= f . x ;
:: thesis: verum

end;

hence (addcpfunc A) . ((CPFuncZero A),f) = f by A1, PARTFUN1:5; :: thesis: verum

end;

let f be Element of PFuncs (A,COMPLEX); :: according to BINOP_1:def 17 :: thesis: (addcpfunc A) . (f,(CPFuncZero A)) = f
set h = (addcpfunc A) . (f,(CPFuncZero A));
dom ((addcpfunc A) . (f,(CPFuncZero A))) = (dom (CPFuncZero A)) /\ (dom f) by Th4;
then dom ((addcpfunc A) . (f,(CPFuncZero A))) = A /\ (dom f) by FUNCOP_1:13;
then A3: dom ((addcpfunc A) . (f,(CPFuncZero A))) = dom f by XBOOLE_1:28;

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

let x be Element of A; :: thesis: ( x in dom f implies ((addcpfunc A) . (f,(CPFuncZero A))) . x = f . x )
A4: (CPFuncZero A) . x = 0c by FUNCOP_1:7;
assume x in dom f ; :: thesis: ((addcpfunc A) . (f,(CPFuncZero A))) . x = f . x
hence ((addcpfunc A) . (f,(CPFuncZero A))) . x = 0c + (f . x) by A3, A4, Th4
.= f . x ;
:: thesis: verum

end;

hence (addcpfunc A) . (f,(CPFuncZero A)) = f by A3, PARTFUN1:5; :: thesis: verum