let V be RealLinearSpace; :: thesis: RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) is RealLinearSpace
A1: for v9, w9 being VECTOR of V
for v, w being VECTOR of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) st v = v9 & w = w9 holds
( v + w = v9 + w9 & ( for r being Real holds r * v = r * v9 ) ) ;
( RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) is Abelian & RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) is add-associative & RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) is right_zeroed & RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) is right_complementable & RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) is vector-distributive & RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) is scalar-distributive & RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) is scalar-associative & RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) is scalar-unital )

proof

hereby :: according to RLVECT_1:def 2 :: thesis: ( RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) is add-associative & RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) is right_zeroed & RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) is right_complementable & RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) is vector-distributive & RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) is scalar-distributive & RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) is scalar-associative & RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) is scalar-unital )

let v, w be VECTOR of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #); :: thesis: v + w = w + v
reconsider v9 = v, w9 = w as VECTOR of V ;
thus v + w = w9 + v9 by A1
.= w + v ; :: thesis: verum

end;

hereby :: according to RLVECT_1:def 3 :: thesis: ( RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) is right_zeroed & RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) is right_complementable & RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) is vector-distributive & RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) is scalar-distributive & RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) is scalar-associative & RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) is scalar-unital )

let u, v, w be VECTOR of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #); :: thesis: (u + v) + w = u + (v + w)
reconsider u9 = u, v9 = v, w9 = w as VECTOR of V ;
thus (u + v) + w = (u9 + v9) + w9
.= u9 + (v9 + w9) by RLVECT_1:def 3
.= u + (v + w) ; :: thesis: verum

end;

hereby :: according to RLVECT_1:def 4 :: thesis: ( RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) is right_complementable & RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) is vector-distributive & RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) is scalar-distributive & RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) is scalar-associative & RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) is scalar-unital )

let v be VECTOR of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #); :: thesis: v + (0. RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #)) = v
reconsider v9 = v as VECTOR of V ;
thus v + (0. RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #)) = v9 + (0. V)
.= v ; :: thesis: verum

end;

thus RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) is right_complementable :: thesis: ( RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) is vector-distributive & RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) is scalar-distributive & RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) is scalar-associative & RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) is scalar-unital )

proof

let v be VECTOR of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #); :: according to ALGSTR_0:def 16 :: thesis: v is right_complementable
reconsider v9 = v as VECTOR of V ;
consider w9 being VECTOR of V such that
A2: v9 + w9 = 0. V by ALGSTR_0:def 11;
reconsider w = w9 as VECTOR of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) ;
take w ; :: according to ALGSTR_0:def 11 :: thesis: v + w = 0. RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #)
thus v + w = 0. RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) by A2; :: thesis: verum

end;

hereby :: according to RLVECT_1:def 5 :: thesis: ( RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) is scalar-distributive & RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) is scalar-associative & RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) is scalar-unital )

let a be Real; :: thesis: for v, w being VECTOR of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) holds a * (v + w) = (a * v) + (a * w)
let v, w be VECTOR of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #); :: thesis: a * (v + w) = (a * v) + (a * w)
reconsider v9 = v, w9 = w as VECTOR of V ;
thus a * (v + w) = a * (v9 + w9)
.= (a * v9) + (a * w9) by RLVECT_1:def 5
.= (a * v) + (a * w) ; :: thesis: verum

end;

hereby :: according to RLVECT_1:def 6 :: thesis: ( RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) is scalar-associative & RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) is scalar-unital )

let a, b be Real; :: thesis: for v being VECTOR of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) holds (a + b) * v = (a * v) + (b * v)
let v be VECTOR of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #); :: thesis: (a + b) * v = (a * v) + (b * v)
reconsider v9 = v as VECTOR of V ;
thus (a + b) * v = (a + b) * v9
.= (a * v9) + (b * v9) by RLVECT_1:def 6
.= (a * v) + (b * v) ; :: thesis: verum

end;

hereby :: according to RLVECT_1:def 7 :: thesis: RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) is scalar-unital

let a, b be Real; :: thesis: for v being VECTOR of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) holds (a * b) * v = a * (b * v)
let v be VECTOR of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #); :: thesis: (a * b) * v = a * (b * v)
reconsider v9 = v as VECTOR of V ;
thus (a * b) * v = (a * b) * v9
.= a * (b * v9) by RLVECT_1:def 7
.= a * (b * v) ; :: thesis: verum

end;

let v be VECTOR of RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #); :: according to RLVECT_1:def 8 :: thesis: 1 * v = v
reconsider v9 = v as VECTOR of V ;
thus 1 * v = 1 * v9
.= v by RLVECT_1:def 8 ; :: thesis: verum

end;

hence RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) is RealLinearSpace ; :: thesis: verum