set IT = CLSp_PFunct A;
thus CLSp_PFunct A is strict ; :: thesis: ( CLSp_PFunct A is Abelian & CLSp_PFunct A is add-associative & CLSp_PFunct A is right_zeroed & CLSp_PFunct A is vector-distributive & CLSp_PFunct A is scalar-distributive & CLSp_PFunct A is scalar-associative & CLSp_PFunct A is scalar-unital )
thus for u, v being VECTOR of (CLSp_PFunct A) holds u + v = v + u by BINOP_1:def 2; :: according to RLVECT_1:def 2 :: thesis: ( CLSp_PFunct A is add-associative & CLSp_PFunct A is right_zeroed & CLSp_PFunct A is vector-distributive & CLSp_PFunct A is scalar-distributive & CLSp_PFunct A is scalar-associative & CLSp_PFunct A is scalar-unital )
thus for u, v, w being VECTOR of (CLSp_PFunct A) holds (u + v) + w = u + (v + w) by BINOP_1:def 3; :: according to RLVECT_1:def 3 :: thesis: ( CLSp_PFunct A is right_zeroed & CLSp_PFunct A is vector-distributive & CLSp_PFunct A is scalar-distributive & CLSp_PFunct A is scalar-associative & CLSp_PFunct A is scalar-unital )
thus for u being VECTOR of (CLSp_PFunct A) holds u + (0. (CLSp_PFunct A)) = u :: according to RLVECT_1:def 4 :: thesis: ( CLSp_PFunct A is vector-distributive & CLSp_PFunct A is scalar-distributive & CLSp_PFunct A is scalar-associative & CLSp_PFunct A is scalar-unital )

proof

let u be VECTOR of (CLSp_PFunct A); :: thesis: u + (0. (CLSp_PFunct A)) = u
reconsider u9 = u as Element of PFuncs (A,COMPLEX) ;
A1: CPFuncZero A is_a_unity_wrt addcpfunc A by Th9;
thus u + (0. (CLSp_PFunct A)) = u by A1, BINOP_1:3; :: thesis: verum

end;

thus for a being Complex
for u, v being VECTOR of (CLSp_PFunct A) holds a * (u + v) = (a * u) + (a * v) :: according to CLVECT_1:def 2 :: thesis: ( CLSp_PFunct A is scalar-distributive & CLSp_PFunct A is scalar-associative & CLSp_PFunct A is scalar-unital )

proof

let a be Complex; :: thesis: for u, v being VECTOR of (CLSp_PFunct A) holds a * (u + v) = (a * u) + (a * v)
reconsider a1 = a as Element of COMPLEX by XCMPLX_0:def 2;
for u, v being VECTOR of (CLSp_PFunct A) holds a * (u + v) = (a * u) + (a * v)

proof

let u, v be VECTOR of (CLSp_PFunct A); :: thesis: a * (u + v) = (a * u) + (a * v)
reconsider u9 = u as Element of PFuncs (A,COMPLEX) ;
reconsider v9 = v as Element of PFuncs (A,COMPLEX) ;
a1 * (u + v) = (multcomplexcpfunc A) . (a1,((addcpfunc A) . (u9,v9)))
.= (addcpfunc A) . (((multcomplexcpfunc A) . (a1,u9)),((multcomplexcpfunc A) . (a1,v9))) by Lm1
.= (a1 * u) + (a1 * v) ;
hence a * (u + v) = (a * u) + (a * v) ; :: thesis: verum

end;

hence for u, v being VECTOR of (CLSp_PFunct A) holds a * (u + v) = (a * u) + (a * v) ; :: thesis: verum

end;

thus for a, b being Complex
for v being VECTOR of (CLSp_PFunct A) holds (a + b) * v = (a * v) + (b * v) :: according to CLVECT_1:def 3 :: thesis: ( CLSp_PFunct A is scalar-associative & CLSp_PFunct A is scalar-unital )

proof

let a, b be Complex; :: thesis: for v being VECTOR of (CLSp_PFunct A) holds (a + b) * v = (a * v) + (b * v)
let v be VECTOR of (CLSp_PFunct A); :: thesis: (a + b) * v = (a * v) + (b * v)
reconsider a1 = a, b1 = b as Element of COMPLEX by XCMPLX_0:def 2;
reconsider v9 = v as Element of PFuncs (A,COMPLEX) ;
(a1 + b1) * v = (multcomplexcpfunc A) . ((a1 + b1),v9)
.= (addcpfunc A) . (((multcomplexcpfunc A) . (a1,v9)),((multcomplexcpfunc A) . (b1,v9))) by Th13
.= (a1 * v) + (b1 * v) ;
hence (a + b) * v = (a * v) + (b * v) ; :: thesis: verum

end;

thus for a, b being Complex
for v being VECTOR of (CLSp_PFunct A) holds (a * b) * v = a * (b * v) :: according to CLVECT_1:def 4 :: thesis: CLSp_PFunct A is scalar-unital

proof

let a, b be Complex; :: thesis: for v being VECTOR of (CLSp_PFunct A) holds (a * b) * v = a * (b * v)
let v be VECTOR of (CLSp_PFunct A); :: thesis: (a * b) * v = a * (b * v)
reconsider a1 = a, b1 = b as Element of COMPLEX by XCMPLX_0:def 2;
reconsider v9 = v as Element of PFuncs (A,COMPLEX) ;
(a1 * b1) * v = (multcomplexcpfunc A) . ((a1 * b1),v9)
.= (multcomplexcpfunc A) . (a1,((multcomplexcpfunc A) . (b1,v9))) by Th12
.= a1 * (b1 * v) ;
hence (a * b) * v = a * (b * v) ; :: thesis: verum

end;

let v be VECTOR of (CLSp_PFunct A); :: according to CLVECT_1:def 5 :: thesis: 1r * v = v
reconsider v9 = v as Element of PFuncs (A,COMPLEX) ;
1r * v = (multcomplexcpfunc A) . (1r,v9)
.= v by Th11 ;
hence 1r * v = v ; :: thesis: verum