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 ) thus for a being Real
for u, v being VECTOR of (RLSp_PFunct A) holds a * (u + v) = (a * u) + (a * v) by Lm1; :: 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 )
thus for a, b being Real
for v being VECTOR of (RLSp_PFunct A) holds (a + b) * v = (a * v) + (b * v) by Th19; :: according to RLVECT_1:def 6 :: thesis: ( RLSp_PFunct A is scalar-associative & RLSp_PFunct A is scalar-unital )
thus for a, b being Real
for v being VECTOR of (RLSp_PFunct A) holds (a * b) * v = a * (b * v) by Th18; :: according to RLVECT_1:def 7 :: thesis: RLSp_PFunct A is scalar-unital
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