let V be RealLinearSpace; :: thesis: RLSStruct(# the carrier of V,the U2 of V,the addF of V,the Mult of V #) is RealLinearSpace
A1: for v', w' being VECTOR of
for v, w being VECTOR of st v = v' & w = w' holds
( v + w = v' + w' & ( for r being Real holds r * v = r * v' ) ) ;
( RLSStruct(# the carrier of V,the U2 of V,the addF of V,the Mult of V #) is Abelian & RLSStruct(# the carrier of V,the U2 of V,the addF of V,the Mult of V #) is add-associative & RLSStruct(# the carrier of V,the U2 of V,the addF of V,the Mult of V #) is right_zeroed & RLSStruct(# the carrier of V,the U2 of V,the addF of V,the Mult of V #) is right_complementable & RLSStruct(# the carrier of V,the U2 of V,the addF of V,the Mult of V #) is RealLinearSpace-like )

proof

hereby :: according to RLVECT_1:def 5 :: thesis: ( RLSStruct(# the carrier of V,the U2 of V,the addF of V,the Mult of V #) is add-associative & RLSStruct(# the carrier of V,the U2 of V,the addF of V,the Mult of V #) is right_zeroed & RLSStruct(# the carrier of V,the U2 of V,the addF of V,the Mult of V #) is right_complementable & RLSStruct(# the carrier of V,the U2 of V,the addF of V,the Mult of V #) is RealLinearSpace-like )

let v, w be VECTOR of ; :: thesis: v + w = w + v
reconsider v' = v, w' = w as VECTOR of ;
thus v + w = w' + v' by A1
.= w + v ; :: thesis: verum

end;

hereby :: according to RLVECT_1:def 6 :: thesis: ( RLSStruct(# the carrier of V,the U2 of V,the addF of V,the Mult of V #) is right_zeroed & RLSStruct(# the carrier of V,the U2 of V,the addF of V,the Mult of V #) is right_complementable & RLSStruct(# the carrier of V,the U2 of V,the addF of V,the Mult of V #) is RealLinearSpace-like )

let u, v, w be VECTOR of ; :: thesis: (u + v) + w = u + (v + w)
reconsider u' = u, v' = v, w' = w as VECTOR of ;
thus (u + v) + w = (u' + v') + w'
.= u' + (v' + w') by RLVECT_1:def 6
.= u + (v + w) ; :: thesis: verum

end;

hereby :: according to RLVECT_1:def 7 :: thesis: ( RLSStruct(# the carrier of V,the U2 of V,the addF of V,the Mult of V #) is right_complementable & RLSStruct(# the carrier of V,the U2 of V,the addF of V,the Mult of V #) is RealLinearSpace-like )

let v be VECTOR of ; :: thesis: v + (0. RLSStruct(# the carrier of V,the U2 of V,the addF of V,the Mult of V #)) = v
reconsider v' = v as VECTOR of ;
thus v + (0. RLSStruct(# the carrier of V,the U2 of V,the addF of V,the Mult of V #)) = v' + (0. V)
.= v by RLVECT_1:10 ; :: thesis: verum

end;

thus RLSStruct(# the carrier of V,the U2 of V,the addF of V,the Mult of V #) is right_complementable :: thesis: RLSStruct(# the carrier of V,the U2 of V,the addF of V,the Mult of V #) is RealLinearSpace-like

proof

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

end;

hereby :: according to RLVECT_1:def 9 :: thesis: ( ( for b₁, b₂ being set
for b₃ being Element of the carrier of RLSStruct(# the carrier of V,the U2 of V,the addF of V,the Mult of V #) holds (b₁ + b₂) * b₃ = (b₁ * b₃) + (b₂ * b₃) ) & ( for b₁, b₂ being set
for b₃ being Element of the carrier of RLSStruct(# the carrier of V,the U2 of V,the addF of V,the Mult of V #) holds (b₁ * b₂) * b₃ = b₁ * (b₂ * b₃) ) & ( for b₁ being Element of the carrier of RLSStruct(# the carrier of V,the U2 of V,the addF of V,the Mult of V #) holds 1 * b₁ = b₁ ) )

let a be real number ; :: thesis: for v, w being VECTOR of holds a * (v + w) = (a * v) + (a * w)
let v, w be VECTOR of ; :: thesis: a * (v + w) = (a * v) + (a * w)
reconsider v' = v, w' = w as VECTOR of ;
thus a * (v + w) = a * (v' + w')
.= (a * v') + (a * w') by RLVECT_1:def 9
.= (a * v) + (a * w) ; :: thesis: verum

end;

hereby :: thesis: ( ( for b₁, b₂ being set
for b₃ being Element of the carrier of RLSStruct(# the carrier of V,the U2 of V,the addF of V,the Mult of V #) holds (b₁ * b₂) * b₃ = b₁ * (b₂ * b₃) ) & ( for b₁ being Element of the carrier of RLSStruct(# the carrier of V,the U2 of V,the addF of V,the Mult of V #) holds 1 * b₁ = b₁ ) )

let a, b be real number ; :: thesis: for v being VECTOR of holds (a + b) * v = (a * v) + (b * v)
let v be VECTOR of ; :: thesis: (a + b) * v = (a * v) + (b * v)
reconsider v' = v as VECTOR of ;
thus (a + b) * v = (a + b) * v'
.= (a * v') + (b * v') by RLVECT_1:def 9
.= (a * v) + (b * v) ; :: thesis: verum

end;

hereby :: thesis: for b₁ being Element of the carrier of RLSStruct(# the carrier of V,the U2 of V,the addF of V,the Mult of V #) holds 1 * b₁ = b₁

let a, b be real number ; :: thesis: for v being VECTOR of holds (a * b) * v = a * (b * v)
let v be VECTOR of ; :: thesis: (a * b) * v = a * (b * v)
reconsider v' = v as VECTOR of ;
thus (a * b) * v = (a * b) * v'
.= a * (b * v') by RLVECT_1:def 9
.= a * (b * v) ; :: thesis: verum

end;

let v be VECTOR of ; :: thesis: 1 * v = v
reconsider v' = v as VECTOR of ;
thus 1 * v = 1 * v'
.= v by RLVECT_1:def 9 ; :: thesis: verum

end;

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