let l0 be RealNormSpace; :: thesis: NORMSTR(# the carrier of l0, the ZeroF of l0, the addF of l0, the Mult of l0, the normF of l0 #) is strict RealNormSpace
set l = NORMSTR(# the carrier of l0, the ZeroF of l0, the addF of l0, the Mult of l0, the normF of l0 #);
reconsider l = NORMSTR(# the carrier of l0, the ZeroF of l0, the addF of l0, the Mult of l0, the normF of l0 #) as non empty NORMSTR ;
A1: l is Abelian

proof

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

end;

A2: l is right_zeroed

proof

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;

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

end;

A5: for v being VECTOR of l holds 1 * v = v

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

end;

A6: for a, b being Real
for v being VECTOR of l holds (a * b) * v = a * (b * v)

proof

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;

A7: for a, b being Real
for v being VECTOR of l holds (a + b) * v = (a * v) + (b * v)

proof

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;

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

proof

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;

A9: l is add-associative

proof

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;

now :: thesis: for x, y being Point of l
for a being Real holds
( ( ||.x.|| = 0 implies x = 0. l ) & ( x = 0. l implies ||.x.|| = 0 ) & ||.(a * x).|| = |.a.| * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| )

let x, y be Point of l; :: thesis: for a being Real holds
( ( ||.x.|| = 0 implies x = 0. l ) & ( x = 0. l implies ||.x.|| = 0 ) & ||.(a * x).|| = |.a.| * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| )
let a be Real; :: thesis: ( ( ||.x.|| = 0 implies x = 0. l ) & ( x = 0. l implies ||.x.|| = 0 ) & ||.(a * x).|| = |.a.| * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| )
reconsider u = x, w = y as VECTOR of l0 ;
( ||.u.|| = 0 iff u = 0. l0 ) by NORMSP_0:def 5, NORMSP_0:def 6;
hence ( ||.x.|| = 0 iff x = 0. l ) ; :: thesis: ( ||.(a * x).|| = |.a.| * ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| )
thus ||.(a * x).|| = ||.(a * u).||
.= |.a.| * ||.u.|| by NORMSP_1:def 1
.= |.a.| * ||.x.|| ; :: thesis: ||.(x + y).|| <= ||.x.|| + ||.y.||
||.(u + w).|| <= ||.u.|| + ||.w.|| by NORMSP_1:def 1;
hence ||.(x + y).|| <= ||.x.|| + ||.y.|| ; :: thesis: verum

end;

then ( l is discerning & l is reflexive & l is RealNormSpace-like ) ;
hence NORMSTR(# the carrier of l0, the ZeroF of l0, the addF of l0, the Mult of l0, the normF of l0 #) is strict RealNormSpace by A1, A2, A3, A5, A6, A7, A8, A9, RLVECT_1:def 5, RLVECT_1:def 6, RLVECT_1:def 7, RLVECT_1:def 8; :: thesis: verum