set S = Linear_Space_of_RealSequences ;
thus Linear_Space_of_RealSequences is Abelian ; :: thesis: ( Linear_Space_of_RealSequences is add-associative & Linear_Space_of_RealSequences is right_zeroed & Linear_Space_of_RealSequences is right_complementable & Linear_Space_of_RealSequences is vector-distributive & Linear_Space_of_RealSequences is scalar-distributive & Linear_Space_of_RealSequences is scalar-associative & Linear_Space_of_RealSequences is scalar-unital )
thus Linear_Space_of_RealSequences is add-associative :: thesis: ( Linear_Space_of_RealSequences is right_zeroed & Linear_Space_of_RealSequences is right_complementable & Linear_Space_of_RealSequences is vector-distributive & Linear_Space_of_RealSequences is scalar-distributive & Linear_Space_of_RealSequences is scalar-associative & Linear_Space_of_RealSequences is scalar-unital )

proof

let u, v, w be Element of Linear_Space_of_RealSequences; :: according to RLVECT_1:def 3 :: thesis: (u + v) + w = u + (v + w)
thus (u + v) + w = u + (v + w) by Th6; :: thesis: verum

end;

thus Linear_Space_of_RealSequences is right_zeroed :: thesis: ( Linear_Space_of_RealSequences is right_complementable & Linear_Space_of_RealSequences is vector-distributive & Linear_Space_of_RealSequences is scalar-distributive & Linear_Space_of_RealSequences is scalar-associative & Linear_Space_of_RealSequences is scalar-unital )

proof

let v be Element of Linear_Space_of_RealSequences; :: according to RLVECT_1:def 4 :: thesis: v + (0. Linear_Space_of_RealSequences) = v
thus v + (0. Linear_Space_of_RealSequences) = v by Th7; :: thesis: verum

end;

thus Linear_Space_of_RealSequences is right_complementable :: thesis: ( Linear_Space_of_RealSequences is vector-distributive & Linear_Space_of_RealSequences is scalar-distributive & Linear_Space_of_RealSequences is scalar-associative & Linear_Space_of_RealSequences is scalar-unital )

proof

let v be Element of Linear_Space_of_RealSequences; :: according to ALGSTR_0:def 16 :: thesis: v is right_complementable
thus ex w being VECTOR of Linear_Space_of_RealSequences st v + w = 0. Linear_Space_of_RealSequences by Th8; :: according to ALGSTR_0:def 11 :: thesis: verum

end;

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

proof

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

end;

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

proof

let a, b be real number ; :: thesis: for v being VECTOR of Linear_Space_of_RealSequences 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 Linear_Space_of_RealSequences holds (a + b) * v = (a * v) + (b * v) by Th10;
hence for v being VECTOR of Linear_Space_of_RealSequences holds (a + b) * v = (a * v) + (b * v) ; :: thesis: verum

end;

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

proof

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

end;

let v be VECTOR of Linear_Space_of_RealSequences; :: according to RLVECT_1:def 8 :: thesis: 1 * v = v
thus 1 * v = v by Th12; :: thesis: verum