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

proof

let u be VECTOR of (RLSp_PFunct A); :: thesis: u + (0. (RLSp_PFunct A)) = u
reconsider u9 = u as Element of PFuncs (A,REAL) ;
thus u + (0. (RLSp_PFunct A)) = (addpfunc A) . ((RealPFuncZero A),u9) by Th10
.= u by Th15 ; :: thesis: verum

end;

thus for a being real number
for u, v being VECTOR of (RLSp_PFunct A) holds a * (u + v) = (a * u) + (a * v) :: according to RLVECT_1:def 5 :: thesis: ( RLSp_PFunct A is scalar-distributive & RLSp_PFunct A is scalar-associative & RLSp_PFunct A is scalar-unital )

proof

let a be real number ; :: thesis: for u, v being VECTOR of (RLSp_PFunct A) holds a * (u + v) = (a * u) + (a * v)
reconsider a = a as Real by XREAL_0:def 1;
for u, v being VECTOR of (RLSp_PFunct A) holds a * (u + v) = (a * u) + (a * v) by Lm1;
hence for u, v being VECTOR of (RLSp_PFunct A) holds a * (u + v) = (a * u) + (a * v) ; :: thesis: verum

end;

thus for a, b being real number
for v being VECTOR of (RLSp_PFunct A) holds (a + b) * v = (a * v) + (b * v) :: according to RLVECT_1:def 6 :: thesis: ( RLSp_PFunct A is scalar-associative & RLSp_PFunct A is scalar-unital )

proof

let a, b be real number ; :: thesis: for v being VECTOR of (RLSp_PFunct A) holds (a + b) * v = (a * v) + (b * v)
reconsider a = a, b = b as Real by XREAL_0:def 1;
for v being VECTOR of (RLSp_PFunct A) holds (a + b) * v = (a * v) + (b * v) by Th19;
hence for v being VECTOR of (RLSp_PFunct A) holds (a + b) * v = (a * v) + (b * v) ; :: thesis: verum

end;

thus for a, b being real number
for v being VECTOR of (RLSp_PFunct A) holds (a * b) * v = a * (b * v) :: according to RLVECT_1:def 7 :: thesis: RLSp_PFunct A is scalar-unital

proof

let a, b be real number ; :: thesis: for v being VECTOR of (RLSp_PFunct A) holds (a * b) * v = a * (b * v)
reconsider a = a, b = b as Real by XREAL_0:def 1;
for v being VECTOR of (RLSp_PFunct A) holds (a * b) * v = a * (b * v) by Th18;
hence for v being VECTOR of (RLSp_PFunct A) holds (a * b) * v = a * (b * v) ; :: thesis: verum

end;

let v be VECTOR of (RLSp_PFunct A); :: according to RLVECT_1:def 8 :: thesis: 1 * v = v
thus 1 * v = v by Th17; :: thesis: verum