let l be RLSStruct ; :: thesis: ( RLSStruct(# the carrier of l, the ZeroF of l, the addF of l, the Mult of l #) is RealLinearSpace implies l is RealLinearSpace )

assume A1: RLSStruct(# the carrier of l, the ZeroF of l, the addF of l, the Mult of l #) is RealLinearSpace ; :: thesis: l is RealLinearSpace

reconsider l = l as non empty RLSStruct by A1;

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

for v being VECTOR of l holds (a * b) * v = a * (b * v)

for v being VECTOR of l holds (a + b) * v = (a * v) + (b * v)

for v, w being VECTOR of l holds a * (v + w) = (a * v) + (a * w)

assume A1: RLSStruct(# the carrier of l, the ZeroF of l, the addF of l, the Mult of l #) is RealLinearSpace ; :: thesis: l is RealLinearSpace

reconsider l = l as non empty RLSStruct by A1;

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

A3:
l is right_zeroed
let v, w be VECTOR of l; :: according to RLVECT_1:def 2 :: 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;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

proof

A4:
l is right_complementable
let v be VECTOR of l; :: according to RLVECT_1:def 4 :: thesis: v + (0. l) = v

reconsider v1 = v as VECTOR of l0 ;

thus v + (0. l) = v1 + (0. l0)

.= v ; :: thesis: verum

end;reconsider v1 = v as VECTOR of l0 ;

thus v + (0. l) = v1 + (0. l0)

.= v ; :: thesis: verum

proof

A6:
for v being VECTOR of l holds 1 * v = v
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

A5: 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 A5; :: thesis: verum

end;reconsider v1 = v as VECTOR of l0 ;

consider w1 being VECTOR of l0 such that

A5: 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 A5; :: thesis: verum

proof

A7:
for a, b being Real
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 8 ; :: thesis: verum

end;reconsider v1 = v as VECTOR of l0 ;

thus 1 * v = 1 * v1

.= v by RLVECT_1:def 8 ; :: thesis: verum

for v being VECTOR of l holds (a * b) * v = a * (b * v)

proof

A8:
for a, b being Real
let a, b be Real; :: 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 7

.= a * (b * v) ; :: thesis: verum

end;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 7

.= a * (b * v) ; :: thesis: verum

for v being VECTOR of l holds (a + b) * v = (a * v) + (b * v)

proof

A9:
for a being Real
let a, b be Real; :: 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 6

.= (a * v) + (b * v) ; :: thesis: verum

end;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 6

.= (a * v) + (b * v) ; :: thesis: verum

for v, w being VECTOR of l holds a * (v + w) = (a * v) + (a * w)

proof

l is add-associative
let a be Real; :: 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 5

.= (a * v) + (a * w) ; :: thesis: verum

end;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 5

.= (a * v) + (a * w) ; :: thesis: verum

proof

hence
l is RealLinearSpace
by A2, A3, A4, A9, A8, A7, A6, RLVECT_1:def 5, RLVECT_1:def 6, RLVECT_1:def 7, RLVECT_1:def 8; :: thesis: verum
let u, v, w be VECTOR of l; :: according to RLVECT_1:def 3 :: 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 3

.= u + (v + w) ; :: thesis: verum

end;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 3

.= u + (v + w) ; :: thesis: verum