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

proof

let x be Element of Linear_Space_of_ComplexSequences; :: according to RLVECT_1:def 3 :: thesis: for b₁, b₂ being Element of the carrier of Linear_Space_of_ComplexSequences holds (x + b₁) + b₂ = x + (b₁ + b₂)
thus for b₁, b₂ being Element of the carrier of Linear_Space_of_ComplexSequences holds (x + b₁) + b₂ = x + (b₁ + b₂) by Th6; :: thesis: verum

end;

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

proof

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

end;

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

proof

let x be Element of Linear_Space_of_ComplexSequences; :: according to ALGSTR_0:def 16 :: thesis: x is right_complementable
consider y being Element of Linear_Space_of_ComplexSequences such that
A1: x + y = 0. Linear_Space_of_ComplexSequences by Th8;
take y ; :: according to ALGSTR_0:def 11 :: thesis: x + y = 0. Linear_Space_of_ComplexSequences
thus x + y = 0. Linear_Space_of_ComplexSequences by A1; :: thesis: verum

end;

thus ( ( for z being Complex
for v, w being VECTOR of Linear_Space_of_ComplexSequences holds z * (v + w) = (z * v) + (z * w) ) & ( for z1, z2 being Complex
for v being VECTOR of Linear_Space_of_ComplexSequences holds (z1 + z2) * v = (z1 * v) + (z2 * v) ) & ( for z1, z2 being Complex
for v being VECTOR of Linear_Space_of_ComplexSequences holds (z1 * z2) * v = z1 * (z2 * v) ) & ( for v being VECTOR of Linear_Space_of_ComplexSequences holds 1r * v = v ) ) by Th9, Th10, Th11, Th12; :: according to CLVECT_1:def 2,CLVECT_1:def 3,CLVECT_1:def 4,CLVECT_1:def 5 :: thesis: verum