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 RealLinearSpace-like )
thus for u, v being VECTOR of (RLSp_PFunct A) holds u + v = v + u by Th10; :: according to RLVECT_1:def 5 :: thesis: ( RLSp_PFunct A is add-associative & RLSp_PFunct A is right_zeroed & RLSp_PFunct A is RealLinearSpace-like )
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 6 :: thesis: ( RLSp_PFunct A is right_zeroed & RLSp_PFunct A is RealLinearSpace-like )
thus for u being VECTOR of (RLSp_PFunct A) holds u + (0. (RLSp_PFunct A)) = u :: according to RLVECT_1:def 7 :: thesis: RLSp_PFunct A is RealLinearSpace-like

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 9 :: thesis: ( ( for b₁, b₂ being set
for b₃ being Element of the carrier of (RLSp_PFunct A) holds (b₁ + b₂) * b₃ = (b₁ * b₃) + (b₂ * b₃) ) & ( for b₁, b₂ being set
for b₃ being Element of the carrier of (RLSp_PFunct A) holds (b₁ * b₂) * b₃ = b₁ * (b₂ * b₃) ) & ( for b₁ being Element of the carrier of (RLSp_PFunct A) holds 1 * b₁ = b₁ ) )

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) :: thesis: ( ( for b₁, b₂ being set
for b₃ being Element of the carrier of (RLSp_PFunct A) holds (b₁ * b₂) * b₃ = b₁ * (b₂ * b₃) ) & ( for b₁ being Element of the carrier of (RLSp_PFunct A) holds 1 * b₁ = b₁ ) )

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) :: thesis: for b₁ being Element of the carrier of (RLSp_PFunct A) holds 1 * b₁ = b₁

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;

thus for b₁ being Element of the carrier of (RLSp_PFunct A) holds 1 * b₁ = b₁ by Th17; :: thesis: verum