set o = addcpfunc A;

hereby :: according to BINOP_1:def 2 :: thesis: addcpfunc A is associative

let F1, F2 be Element of PFuncs (A,COMPLEX); :: thesis: (addcpfunc A) . (F1,F2) = (addcpfunc A) . (F2,F1)
thus (addcpfunc A) . (F1,F2) = F2 + F1 by Def5
.= (addcpfunc A) . (F2,F1) by Def5 ; :: thesis: verum

end;

let F1, F2, F3 be Element of PFuncs (A,COMPLEX); :: according to BINOP_1:def 3 :: thesis: (addcpfunc A) . (F1,((addcpfunc A) . (F2,F3))) = (addcpfunc A) . (((addcpfunc A) . (F1,F2)),F3)
thus (addcpfunc A) . (F1,((addcpfunc A) . (F2,F3))) = F1 + ((addcpfunc A) . (F2,F3)) by Def5
.= F1 + (F2 + F3) by Def5
.= (F1 + F2) + F3 by RFUNCT_1:8
.= ((addcpfunc A) . (F1,F2)) + F3 by Def5
.= (addcpfunc A) . (((addcpfunc A) . (F1,F2)),F3) by Def5 ; :: thesis: verum