let l be RLSStruct ; :: thesis: ( RLSStruct(# the carrier of l,the U2 of l,the addF of l,the Mult of l #) is RealLinearSpace implies l is RealLinearSpace )
assume A1: RLSStruct(# the carrier of l,the U2 of l,the addF of l,the Mult of l #) is RealLinearSpace ; :: thesis: l is RealLinearSpace
not the carrier of l is empty by A1;
then reconsider l = l as non empty RLSStruct ;
reconsider l0 = RLSStruct(# the carrier of l,(0. l),the addF of l,the Mult of l #) as RealLinearSpace by A1;
A2: l is Abelian

proof

let v, w be VECTOR of l; :: according to RLVECT_1:def 5 :: thesis: v + w = w + v
reconsider v1 = v as VECTOR of l0 ;
reconsider w1 = w as VECTOR of l0 ;
thus v + w = v1 + w1
.= w1 + v1
.= w + v ; :: thesis: verum

end;

A3: l is add-associative

proof

let u, v, w be VECTOR of l; :: according to RLVECT_1:def 6 :: thesis: (u + v) + w = u + (v + w)
reconsider u1 = u, v1 = v, w1 = w as VECTOR of l0 ;
thus (u + v) + w = (u1 + v1) + w1
.= u1 + (v1 + w1) by RLVECT_1:def 6
.= u + (v + w) ; :: thesis: verum

end;

A4: l is right_zeroed

proof

let v be VECTOR of l; :: according to RLVECT_1:def 7 :: thesis: v + (0. l) = v
reconsider v1 = v as VECTOR of l0 ;
thus v + (0. l) = v1 + (0. l0)
.= v by RLVECT_1:def 7 ; :: thesis: verum

end;

A5: l is right_complementable

proof

let v be VECTOR of l; :: according to ALGSTR_0:def 16 :: thesis: v is right_complementable
reconsider v1 = v as VECTOR of l0 ;
consider w1 being VECTOR of l0 such that
A6: v1 + w1 = 0. l0 by ALGSTR_0:def 11;
reconsider w = w1 as VECTOR of l ;
take w ; :: according to ALGSTR_0:def 11 :: thesis: v + w = 0. l
thus v + w = 0. l by A6; :: thesis: verum

end;

l is RealLinearSpace-like

proof

thus for a being real number
for v, w being VECTOR of l holds a * (v + w) = (a * v) + (a * w) :: according to RLVECT_1:def 9 :: thesis: ( ( for b₁, b₂ being set
for b₃ being Element of the carrier of l holds (b₁ + b₂) * b₃ = (b₁ * b₃) + (b₂ * b₃) ) & ( for b₁, b₂ being set
for b₃ being Element of the carrier of l holds (b₁ * b₂) * b₃ = b₁ * (b₂ * b₃) ) & ( for b₁ being Element of the carrier of l holds 1 * b₁ = b₁ ) )

proof

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

end;

thus for a, b being real number
for v being VECTOR of l holds (a + b) * v = (a * v) + (b * v) :: thesis: ( ( for b₁, b₂ being set
for b₃ being Element of the carrier of l holds (b₁ * b₂) * b₃ = b₁ * (b₂ * b₃) ) & ( for b₁ being Element of the carrier of l holds 1 * b₁ = b₁ ) )

proof

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

end;

thus for a, b being real number
for v being VECTOR of l holds (a * b) * v = a * (b * v) :: thesis: for b₁ being Element of the carrier of l holds 1 * b₁ = b₁

proof

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

end;

thus for v being VECTOR of l holds 1 * v = v :: thesis: verum

proof

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

end;

end;

hence l is RealLinearSpace by A2, A3, A4, A5; :: thesis: verum