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

proof

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

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

let x be Element of A; :: thesis: ( x in dom f implies ((multcpfunc A) . ((CPFuncUnit A),f)) . x = f . x )
assume x in dom f ; :: thesis: ((multcpfunc A) . ((CPFuncUnit A),f)) . x = f . x
then ((multcpfunc A) . ((CPFuncUnit A),f)) . x = ((CPFuncUnit A) . x) * (f . x) by A1, Th5;
then ((multcpfunc A) . ((CPFuncUnit A),f)) . x = 1r * (f . x) by FUNCOP_1:7
.= f . x by COMPLEX1:def 4 ;
hence ((multcpfunc A) . ((CPFuncUnit A),f)) . x = f . x ; :: thesis: verum

end;

hence (multcpfunc A) . ((CPFuncUnit 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: (multcpfunc A) . (f,(CPFuncUnit A)) = f
set h = (multcpfunc A) . (f,(CPFuncUnit A));
dom ((multcpfunc A) . (f,(CPFuncUnit A))) = (dom (CPFuncUnit A)) /\ (dom f) by Th5;
then dom ((multcpfunc A) . (f,(CPFuncUnit A))) = A /\ (dom f) by FUNCOP_1:13;
then A2: dom ((multcpfunc A) . (f,(CPFuncUnit A))) = dom f by XBOOLE_1:28;

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

let x be Element of A; :: thesis: ( x in dom f implies ((multcpfunc A) . (f,(CPFuncUnit A))) . x = f . x )
assume x in dom f ; :: thesis: ((multcpfunc A) . (f,(CPFuncUnit A))) . x = f . x
then ((multcpfunc A) . (f,(CPFuncUnit A))) . x = ((CPFuncUnit A) . x) * (f . x) by A2, Th5;
then ((multcpfunc A) . (f,(CPFuncUnit A))) . x = 1r * (f . x) by FUNCOP_1:7
.= f . x by COMPLEX1:def 4 ;
hence ((multcpfunc A) . (f,(CPFuncUnit A))) . x = f . x ; :: thesis: verum

end;

hence (multcpfunc A) . (f,(CPFuncUnit A)) = f by A2, PARTFUN1:5; :: thesis: verum