consider CY being Subset of X such that

A2: ( CY = the carrier of Y & CY is closed ) by A1;

set S = VectQuot (X,Y);

A3: the carrier of (VectQuot (X,Y)) = CosetSet (X,Y) by LMQ06;

then reconsider NF = NormCoset (X,Y) as Function of the carrier of (VectQuot (X,Y)),REAL ;

reconsider T = NORMSTR(# the carrier of (VectQuot (X,Y)),(0. (VectQuot (X,Y))), the addF of (VectQuot (X,Y)), the Mult of (VectQuot (X,Y)),NF #) as non empty NORMSTR ;

A7: T is right_complementable

A13: ||.(0. T).|| = lower_bound (NormVSets (X,Y,(0. X))) by A3, DeNorm, LMQ13;

then A14: ||.(0. T).|| <= ||.(0. X).|| by LMQ23;

then A15: T is reflexive by A13, LMQ23;

then reconsider T = T as strict RealNormSpace by A4, A5, A6, A7, A8, A9, A10, A11, A15, A22;

take T ; :: thesis: ( RLSStruct(# the carrier of T, the ZeroF of T, the addF of T, the Mult of T #) = VectQuot (X,Y) & the normF of T = NormCoset (X,Y) )

thus ( RLSStruct(# the carrier of T, the ZeroF of T, the addF of T, the Mult of T #) = VectQuot (X,Y) & the normF of T = NormCoset (X,Y) ) ; :: thesis: verum

A2: ( CY = the carrier of Y & CY is closed ) by A1;

set S = VectQuot (X,Y);

A3: the carrier of (VectQuot (X,Y)) = CosetSet (X,Y) by LMQ06;

then reconsider NF = NormCoset (X,Y) as Function of the carrier of (VectQuot (X,Y)),REAL ;

reconsider T = NORMSTR(# the carrier of (VectQuot (X,Y)),(0. (VectQuot (X,Y))), the addF of (VectQuot (X,Y)), the Mult of (VectQuot (X,Y)),NF #) as non empty NORMSTR ;

now :: thesis: for v, w being Element of T holds v + w = w + v

then A4:
T is Abelian
;let v, w be Element of T; :: thesis: v + w = w + v

reconsider v1 = v, w1 = w as Element of (VectQuot (X,Y)) ;

thus v + w = v1 + w1

.= w1 + v1

.= w + v ; :: thesis: verum

end;reconsider v1 = v, w1 = w as Element of (VectQuot (X,Y)) ;

thus v + w = v1 + w1

.= w1 + v1

.= w + v ; :: thesis: verum

now :: thesis: for u, v, w being Element of T holds (u + v) + w = u + (v + w)

then A5:
T is add-associative
;let u, v, w be Element of T; :: thesis: (u + v) + w = u + (v + w)

reconsider u1 = u, v1 = v, w1 = w as Element of (VectQuot (X,Y)) ;

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 Element of (VectQuot (X,Y)) ;

thus (u + v) + w = (u1 + v1) + w1

.= u1 + (v1 + w1) by RLVECT_1:def 3

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

now :: thesis: for v being Element of T holds v + (0. T) = v

then A6:
T is right_zeroed
;let v be Element of T; :: thesis: v + (0. T) = v

reconsider v1 = v as Element of (VectQuot (X,Y)) ;

thus v + (0. T) = v1 + (0. (VectQuot (X,Y)))

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

end;reconsider v1 = v as Element of (VectQuot (X,Y)) ;

thus v + (0. T) = v1 + (0. (VectQuot (X,Y)))

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

A7: T is right_complementable

proof

let v be Element of T; :: according to ALGSTR_0:def 16 :: thesis: v is right_complementable

reconsider v1 = v as Element of (VectQuot (X,Y)) ;

reconsider w1 = - v1 as Element of (VectQuot (X,Y)) ;

reconsider w = w1 as Element of T ;

take w ; :: according to ALGSTR_0:def 11 :: thesis: v + w = 0. T

thus v + w = v1 + w1

.= 0. T by RLVECT_1:5 ; :: thesis: verum

end;reconsider v1 = v as Element of (VectQuot (X,Y)) ;

reconsider w1 = - v1 as Element of (VectQuot (X,Y)) ;

reconsider w = w1 as Element of T ;

take w ; :: according to ALGSTR_0:def 11 :: thesis: v + w = 0. T

thus v + w = v1 + w1

.= 0. T by RLVECT_1:5 ; :: thesis: verum

now :: thesis: for a, b being Real

for v being Element of T holds (a + b) * v = (a * v) + (b * v)

then A8:
T is scalar-distributive
;for v being Element of T holds (a + b) * v = (a * v) + (b * v)

let a, b be Real; :: thesis: for v being Element of T holds (a + b) * v = (a * v) + (b * v)

let v be Element of T; :: thesis: (a + b) * v = (a * v) + (b * v)

reconsider v1 = v as Element of (VectQuot (X,Y)) ;

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 Element of T; :: thesis: (a + b) * v = (a * v) + (b * v)

reconsider v1 = v as Element of (VectQuot (X,Y)) ;

thus (a + b) * v = (a + b) * v1

.= (a * v1) + (b * v1) by RLVECT_1:def 6

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

now :: thesis: for a being Real

for v, w being Element of T holds a * (v + w) = (a * v) + (a * w)

then A9:
T is vector-distributive
;for v, w being Element of T holds a * (v + w) = (a * v) + (a * w)

let a be Real; :: thesis: for v, w being Element of T holds a * (v + w) = (a * v) + (a * w)

let v, w be Element of T; :: thesis: a * (v + w) = (a * v) + (a * w)

reconsider v1 = v, w1 = w as Element of (VectQuot (X,Y)) ;

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 Element of T; :: thesis: a * (v + w) = (a * v) + (a * w)

reconsider v1 = v, w1 = w as Element of (VectQuot (X,Y)) ;

thus a * (v + w) = a * (v1 + w1)

.= (a * v1) + (a * w1) by RLVECT_1:def 5

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

now :: thesis: for a, b being Real

for v being Element of T holds (a * b) * v = a * (b * v)

then A10:
T is scalar-associative
;for v being Element of T holds (a * b) * v = a * (b * v)

let a, b be Real; :: thesis: for v being Element of T holds (a * b) * v = a * (b * v)

let v be Element of T; :: thesis: (a * b) * v = a * (b * v)

reconsider v1 = v as Element of (VectQuot (X,Y)) ;

thus (a * b) * v = (a * b) * v1

.= a * (b * v1) by RLVECT_1:def 7

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

end;let v be Element of T; :: thesis: (a * b) * v = a * (b * v)

reconsider v1 = v as Element of (VectQuot (X,Y)) ;

thus (a * b) * v = (a * b) * v1

.= a * (b * v1) by RLVECT_1:def 7

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

now :: thesis: for v being Element of T holds 1 * v = v

then A11:
T is scalar-unital
;let v be Element of T; :: thesis: 1 * v = v

reconsider v1 = v as Element of (VectQuot (X,Y)) ;

thus 1 * v = 1 * v1

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

end;reconsider v1 = v as Element of (VectQuot (X,Y)) ;

thus 1 * v = 1 * v1

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

A13: ||.(0. T).|| = lower_bound (NormVSets (X,Y,(0. X))) by A3, DeNorm, LMQ13;

then A14: ||.(0. T).|| <= ||.(0. X).|| by LMQ23;

then A15: T is reflexive by A13, LMQ23;

now :: thesis: for z being Element of T st ||.z.|| = 0 holds

z = 0. T

then A22:
T is discerning
;z = 0. T

let z be Element of T; :: thesis: ( ||.z.|| = 0 implies z = 0. T )

assume A16: ||.z.|| = 0 ; :: thesis: z = 0. T

reconsider z1 = z as Element of (VectQuot (X,Y)) ;

consider v being Point of X such that

A17: z1 = v + Y by LMQ07;

A18: 0 = lower_bound (NormVSets (X,Y,v)) by A3, A16, A17, DeNorm;

for e being Real st 0 < e holds

ex w being VECTOR of X st

( w in CY & ||.(v - w).|| <= e )

then v + Y = the carrier of Y by RLSUB_1:48;

hence z = 0. T by A17, LMQ13; :: thesis: verum

end;assume A16: ||.z.|| = 0 ; :: thesis: z = 0. T

reconsider z1 = z as Element of (VectQuot (X,Y)) ;

consider v being Point of X such that

A17: z1 = v + Y by LMQ07;

A18: 0 = lower_bound (NormVSets (X,Y,v)) by A3, A16, A17, DeNorm;

for e being Real st 0 < e holds

ex w being VECTOR of X st

( w in CY & ||.(v - w).|| <= e )

proof

then
v in Y
by A2, CLOSE1;
let e be Real; :: thesis: ( 0 < e implies ex w being VECTOR of X st

( w in CY & ||.(v - w).|| <= e ) )

set g = lower_bound (NormVSets (X,Y,v));

assume 0 < e ; :: thesis: ex w being VECTOR of X st

( w in CY & ||.(v - w).|| <= e )

then consider r being Real such that

A19: ( r in NormVSets (X,Y,v) & r < (lower_bound (NormVSets (X,Y,v))) + e ) by SEQ_4:def 2;

consider x being VECTOR of X such that

A20: ( r = ||.x.|| & x in v + Y ) by A19;

consider u being Point of X such that

A21: ( x = v + u & u in Y ) by A20;

set w = - u;

take - u ; :: thesis: ( - u in CY & ||.(v - (- u)).|| <= e )

- u in Y by A21, RLSUB_1:22;

hence - u in CY by A2; :: thesis: ||.(v - (- u)).|| <= e

thus ||.(v - (- u)).|| <= e by A18, A19, A20, A21, RLVECT_1:17; :: thesis: verum

end;( w in CY & ||.(v - w).|| <= e ) )

set g = lower_bound (NormVSets (X,Y,v));

assume 0 < e ; :: thesis: ex w being VECTOR of X st

( w in CY & ||.(v - w).|| <= e )

then consider r being Real such that

A19: ( r in NormVSets (X,Y,v) & r < (lower_bound (NormVSets (X,Y,v))) + e ) by SEQ_4:def 2;

consider x being VECTOR of X such that

A20: ( r = ||.x.|| & x in v + Y ) by A19;

consider u being Point of X such that

A21: ( x = v + u & u in Y ) by A20;

set w = - u;

take - u ; :: thesis: ( - u in CY & ||.(v - (- u)).|| <= e )

- u in Y by A21, RLSUB_1:22;

hence - u in CY by A2; :: thesis: ||.(v - (- u)).|| <= e

thus ||.(v - (- u)).|| <= e by A18, A19, A20, A21, RLVECT_1:17; :: thesis: verum

then v + Y = the carrier of Y by RLSUB_1:48;

hence z = 0. T by A17, LMQ13; :: thesis: verum

now :: thesis: for a being Real

for v, w being Element of T holds

( ||.(a * v).|| = |.a.| * ||.v.|| & ||.(v + w).|| <= ||.v.|| + ||.w.|| )

then
T is RealNormSpace-like
;for v, w being Element of T holds

( ||.(a * v).|| = |.a.| * ||.v.|| & ||.(v + w).|| <= ||.v.|| + ||.w.|| )

let a be Real; :: thesis: for v, w being Element of T holds

( ||.(a * v).|| = |.a.| * ||.v.|| & ||.(v + w).|| <= ||.v.|| + ||.w.|| )

let v, w be Element of T; :: thesis: ( ||.(a * v).|| = |.a.| * ||.v.|| & ||.(v + w).|| <= ||.v.|| + ||.w.|| )

reconsider v1 = v, w1 = w as Element of (VectQuot (X,Y)) ;

thus ||.(a * v).|| = |.a.| * ||.v.|| :: thesis: ||.(v + w).|| <= ||.v.|| + ||.w.||

end;( ||.(a * v).|| = |.a.| * ||.v.|| & ||.(v + w).|| <= ||.v.|| + ||.w.|| )

let v, w be Element of T; :: thesis: ( ||.(a * v).|| = |.a.| * ||.v.|| & ||.(v + w).|| <= ||.v.|| + ||.w.|| )

reconsider v1 = v, w1 = w as Element of (VectQuot (X,Y)) ;

thus ||.(a * v).|| = |.a.| * ||.v.|| :: thesis: ||.(v + w).|| <= ||.v.|| + ||.w.||

proof
end;

thus
||.(v + w).|| <= ||.v.|| + ||.w.||
:: thesis: verumper cases
( a = 0 or not a = 0 )
;

end;

suppose A23:
a = 0
; :: thesis: ||.(a * v).|| = |.a.| * ||.v.||

then 0. T =
a * v1
by RLVECT_1:10

.= a * v ;

hence ||.(a * v).|| = |.a.| * ||.v.|| by A13, A14, A23, COMPLEX1:44, LMQ23; :: thesis: verum

end;.= a * v ;

hence ||.(a * v).|| = |.a.| * ||.v.|| by A13, A14, A23, COMPLEX1:44, LMQ23; :: thesis: verum

suppose A24:
not a = 0
; :: thesis: ||.(a * v).|| = |.a.| * ||.v.||

then A25:
0 < |.a.|
by COMPLEX1:47;

consider vv1 being Point of X such that

A26: v1 = vv1 + Y by LMQ07;

A27: ||.v.|| = lower_bound (NormVSets (X,Y,vv1)) by A3, A26, DeNorm;

a * v = a * v1

.= (a * vv1) + Y by A26, LMQ09 ;

then A29: ||.(a * v).|| = lower_bound (NormVSets (X,Y,(a * vv1))) by A3, DeNorm;

for r being ExtReal st r in NormVSets (X,Y,(a * vv1)) holds

|.a.| * ||.v.|| <= r

then A36: |.a.| * ||.v.|| <= ||.(a * v).|| by A29, XXREAL_2:def 4;

for r being ExtReal st r in NormVSets (X,Y,vv1) holds

(1 / |.a.|) * ||.(a * v).|| <= r

0 <= |.a.| by COMPLEX1:46;

then |.a.| * ((1 / |.a.|) * ||.(a * v).||) <= |.a.| * ||.v.|| by A27, A43, XREAL_1:64, XXREAL_2:def 4;

then (|.a.| * (1 / |.a.|)) * ||.(a * v).|| <= |.a.| * ||.v.|| ;

then 1 * ||.(a * v).|| <= |.a.| * ||.v.|| by A25, XCMPLX_1:106;

hence ||.(a * v).|| = |.a.| * ||.v.|| by A36, XXREAL_0:1; :: thesis: verum

end;consider vv1 being Point of X such that

A26: v1 = vv1 + Y by LMQ07;

A27: ||.v.|| = lower_bound (NormVSets (X,Y,vv1)) by A3, A26, DeNorm;

a * v = a * v1

.= (a * vv1) + Y by A26, LMQ09 ;

then A29: ||.(a * v).|| = lower_bound (NormVSets (X,Y,(a * vv1))) by A3, DeNorm;

for r being ExtReal st r in NormVSets (X,Y,(a * vv1)) holds

|.a.| * ||.v.|| <= r

proof

then
|.a.| * ||.v.|| is LowerBound of NormVSets (X,Y,(a * vv1))
by XXREAL_2:def 2;
let r be ExtReal; :: thesis: ( r in NormVSets (X,Y,(a * vv1)) implies |.a.| * ||.v.|| <= r )

assume r in NormVSets (X,Y,(a * vv1)) ; :: thesis: |.a.| * ||.v.|| <= r

then consider x being VECTOR of X such that

A30: ( r = ||.x.|| & x in (a * vv1) + Y ) ;

consider y being VECTOR of X such that

A31: ( x = (a * vv1) + y & y in Y ) by A30;

A32: (a * vv1) + y = (a * vv1) + (1 * y) by RLVECT_1:def 8

.= (a * vv1) + ((a * (1 / a)) * y) by A24, XCMPLX_1:106

.= (a * vv1) + (a * ((1 / a) * y)) by RLVECT_1:def 7

.= a * (vv1 + ((1 / a) * y)) by RLVECT_1:def 5 ;

A33: (1 / a) * y in Y by A31, RLSUB_1:21;

A34: ||.((a * vv1) + y).|| = |.a.| * ||.(vv1 + ((1 / a) * y)).|| by A32, NORMSP_1:def 1;

vv1 + ((1 / a) * y) in vv1 + Y by A33;

then ||.(vv1 + ((1 / a) * y)).|| in NormVSets (X,Y,vv1) ;

then ||.v.|| <= ||.(vv1 + ((1 / a) * y)).|| by A27, SEQ_4:def 2;

hence |.a.| * ||.v.|| <= r by A25, A30, A31, A34, XREAL_1:64; :: thesis: verum

end;assume r in NormVSets (X,Y,(a * vv1)) ; :: thesis: |.a.| * ||.v.|| <= r

then consider x being VECTOR of X such that

A30: ( r = ||.x.|| & x in (a * vv1) + Y ) ;

consider y being VECTOR of X such that

A31: ( x = (a * vv1) + y & y in Y ) by A30;

A32: (a * vv1) + y = (a * vv1) + (1 * y) by RLVECT_1:def 8

.= (a * vv1) + ((a * (1 / a)) * y) by A24, XCMPLX_1:106

.= (a * vv1) + (a * ((1 / a) * y)) by RLVECT_1:def 7

.= a * (vv1 + ((1 / a) * y)) by RLVECT_1:def 5 ;

A33: (1 / a) * y in Y by A31, RLSUB_1:21;

A34: ||.((a * vv1) + y).|| = |.a.| * ||.(vv1 + ((1 / a) * y)).|| by A32, NORMSP_1:def 1;

vv1 + ((1 / a) * y) in vv1 + Y by A33;

then ||.(vv1 + ((1 / a) * y)).|| in NormVSets (X,Y,vv1) ;

then ||.v.|| <= ||.(vv1 + ((1 / a) * y)).|| by A27, SEQ_4:def 2;

hence |.a.| * ||.v.|| <= r by A25, A30, A31, A34, XREAL_1:64; :: thesis: verum

then A36: |.a.| * ||.v.|| <= ||.(a * v).|| by A29, XXREAL_2:def 4;

for r being ExtReal st r in NormVSets (X,Y,vv1) holds

(1 / |.a.|) * ||.(a * v).|| <= r

proof

then A43:
(1 / |.a.|) * ||.(a * v).|| is LowerBound of NormVSets (X,Y,vv1)
by XXREAL_2:def 2;
let r be ExtReal; :: thesis: ( r in NormVSets (X,Y,vv1) implies (1 / |.a.|) * ||.(a * v).|| <= r )

assume r in NormVSets (X,Y,vv1) ; :: thesis: (1 / |.a.|) * ||.(a * v).|| <= r

then consider x being VECTOR of X such that

A37: ( r = ||.x.|| & x in vv1 + Y ) ;

consider y being VECTOR of X such that

A38: ( x = vv1 + y & y in Y ) by A37;

A39: vv1 + y = 1 * (vv1 + y) by RLVECT_1:def 8

.= ((1 / a) * a) * (vv1 + y) by A24, XCMPLX_1:106

.= (1 / a) * (a * (vv1 + y)) by RLVECT_1:def 7

.= (1 / a) * ((a * vv1) + (a * y)) by RLVECT_1:def 5 ;

A40: a * y in Y by A38, RLSUB_1:21;

A41: ||.(vv1 + y).|| = |.(1 / a).| * ||.((a * vv1) + (a * y)).|| by A39, NORMSP_1:def 1;

(a * vv1) + (a * y) in (a * vv1) + Y by A40;

then ||.((a * vv1) + (a * y)).|| in NormVSets (X,Y,(a * vv1)) ;

then A42: ||.(a * v).|| <= ||.((a * vv1) + (a * y)).|| by A29, SEQ_4:def 2;

0 <= |.(1 / a).| by COMPLEX1:46;

then |.(1 / a).| * ||.(a * v).|| <= |.(1 / a).| * ||.((a * vv1) + (a * y)).|| by A42, XREAL_1:64;

hence (1 / |.a.|) * ||.(a * v).|| <= r by A37, A38, A41, COMPLEX1:80; :: thesis: verum

end;assume r in NormVSets (X,Y,vv1) ; :: thesis: (1 / |.a.|) * ||.(a * v).|| <= r

then consider x being VECTOR of X such that

A37: ( r = ||.x.|| & x in vv1 + Y ) ;

consider y being VECTOR of X such that

A38: ( x = vv1 + y & y in Y ) by A37;

A39: vv1 + y = 1 * (vv1 + y) by RLVECT_1:def 8

.= ((1 / a) * a) * (vv1 + y) by A24, XCMPLX_1:106

.= (1 / a) * (a * (vv1 + y)) by RLVECT_1:def 7

.= (1 / a) * ((a * vv1) + (a * y)) by RLVECT_1:def 5 ;

A40: a * y in Y by A38, RLSUB_1:21;

A41: ||.(vv1 + y).|| = |.(1 / a).| * ||.((a * vv1) + (a * y)).|| by A39, NORMSP_1:def 1;

(a * vv1) + (a * y) in (a * vv1) + Y by A40;

then ||.((a * vv1) + (a * y)).|| in NormVSets (X,Y,(a * vv1)) ;

then A42: ||.(a * v).|| <= ||.((a * vv1) + (a * y)).|| by A29, SEQ_4:def 2;

0 <= |.(1 / a).| by COMPLEX1:46;

then |.(1 / a).| * ||.(a * v).|| <= |.(1 / a).| * ||.((a * vv1) + (a * y)).|| by A42, XREAL_1:64;

hence (1 / |.a.|) * ||.(a * v).|| <= r by A37, A38, A41, COMPLEX1:80; :: thesis: verum

0 <= |.a.| by COMPLEX1:46;

then |.a.| * ((1 / |.a.|) * ||.(a * v).||) <= |.a.| * ||.v.|| by A27, A43, XREAL_1:64, XXREAL_2:def 4;

then (|.a.| * (1 / |.a.|)) * ||.(a * v).|| <= |.a.| * ||.v.|| ;

then 1 * ||.(a * v).|| <= |.a.| * ||.v.|| by A25, XCMPLX_1:106;

hence ||.(a * v).|| = |.a.| * ||.v.|| by A36, XXREAL_0:1; :: thesis: verum

proof

consider vv1 being Point of X such that

A44: v1 = vv1 + Y by LMQ07;

A45: ||.v.|| = lower_bound (NormVSets (X,Y,vv1)) by A3, A44, DeNorm;

consider ww1 being Point of X such that

A46: w1 = ww1 + Y by LMQ07;

A47: ||.w.|| = lower_bound (NormVSets (X,Y,ww1)) by A3, A46, DeNorm;

v + w = v1 + w1

.= (vv1 + ww1) + Y by A44, A46, LMQ11 ;

then A49: ||.(v + w).|| = lower_bound (NormVSets (X,Y,(vv1 + ww1))) by A3, DeNorm;

A50: for y1, y2 being Point of X st y1 in Y & y2 in Y holds

||.(v + w).|| <= ||.(vv1 + y1).|| + ||.(ww1 + y2).||

||.(v + w).|| - ||.w.|| <= ||.(vv1 + y1).||

||.(v + w).|| - ||.w.|| <= r

then (||.(v + w).|| - ||.w.||) + ||.w.|| <= ||.v.|| + ||.w.|| by A45, XREAL_1:6, XXREAL_2:def 4;

hence ||.(v + w).|| <= ||.v.|| + ||.w.|| ; :: thesis: verum

end;A44: v1 = vv1 + Y by LMQ07;

A45: ||.v.|| = lower_bound (NormVSets (X,Y,vv1)) by A3, A44, DeNorm;

consider ww1 being Point of X such that

A46: w1 = ww1 + Y by LMQ07;

A47: ||.w.|| = lower_bound (NormVSets (X,Y,ww1)) by A3, A46, DeNorm;

v + w = v1 + w1

.= (vv1 + ww1) + Y by A44, A46, LMQ11 ;

then A49: ||.(v + w).|| = lower_bound (NormVSets (X,Y,(vv1 + ww1))) by A3, DeNorm;

A50: for y1, y2 being Point of X st y1 in Y & y2 in Y holds

||.(v + w).|| <= ||.(vv1 + y1).|| + ||.(ww1 + y2).||

proof

A52:
for y1 being Point of X st y1 in Y holds
let y1, y2 be Point of X; :: thesis: ( y1 in Y & y2 in Y implies ||.(v + w).|| <= ||.(vv1 + y1).|| + ||.(ww1 + y2).|| )

assume ( y1 in Y & y2 in Y ) ; :: thesis: ||.(v + w).|| <= ||.(vv1 + y1).|| + ||.(ww1 + y2).||

then y1 + y2 in Y by RLSUB_1:20;

then (vv1 + ww1) + (y1 + y2) in (vv1 + ww1) + Y ;

then ||.((vv1 + ww1) + (y1 + y2)).|| in NormVSets (X,Y,(vv1 + ww1)) ;

then A51: lower_bound (NormVSets (X,Y,(vv1 + ww1))) <= ||.((vv1 + ww1) + (y1 + y2)).|| by SEQ_4:def 2;

||.((vv1 + ww1) + (y1 + y2)).|| = ||.(((vv1 + ww1) + y1) + y2).|| by RLVECT_1:def 3

.= ||.(((vv1 + y1) + ww1) + y2).|| by RLVECT_1:def 3

.= ||.((vv1 + y1) + (ww1 + y2)).|| by RLVECT_1:def 3 ;

then ||.((vv1 + ww1) + (y1 + y2)).|| <= ||.(vv1 + y1).|| + ||.(ww1 + y2).|| by NORMSP_1:def 1;

hence ||.(v + w).|| <= ||.(vv1 + y1).|| + ||.(ww1 + y2).|| by A49, A51, XXREAL_0:2; :: thesis: verum

end;assume ( y1 in Y & y2 in Y ) ; :: thesis: ||.(v + w).|| <= ||.(vv1 + y1).|| + ||.(ww1 + y2).||

then y1 + y2 in Y by RLSUB_1:20;

then (vv1 + ww1) + (y1 + y2) in (vv1 + ww1) + Y ;

then ||.((vv1 + ww1) + (y1 + y2)).|| in NormVSets (X,Y,(vv1 + ww1)) ;

then A51: lower_bound (NormVSets (X,Y,(vv1 + ww1))) <= ||.((vv1 + ww1) + (y1 + y2)).|| by SEQ_4:def 2;

||.((vv1 + ww1) + (y1 + y2)).|| = ||.(((vv1 + ww1) + y1) + y2).|| by RLVECT_1:def 3

.= ||.(((vv1 + y1) + ww1) + y2).|| by RLVECT_1:def 3

.= ||.((vv1 + y1) + (ww1 + y2)).|| by RLVECT_1:def 3 ;

then ||.((vv1 + ww1) + (y1 + y2)).|| <= ||.(vv1 + y1).|| + ||.(ww1 + y2).|| by NORMSP_1:def 1;

hence ||.(v + w).|| <= ||.(vv1 + y1).|| + ||.(ww1 + y2).|| by A49, A51, XXREAL_0:2; :: thesis: verum

||.(v + w).|| - ||.w.|| <= ||.(vv1 + y1).||

proof

for r being ExtReal st r in NormVSets (X,Y,vv1) holds
let y1 be Point of X; :: thesis: ( y1 in Y implies ||.(v + w).|| - ||.w.|| <= ||.(vv1 + y1).|| )

assume A53: y1 in Y ; :: thesis: ||.(v + w).|| - ||.w.|| <= ||.(vv1 + y1).||

||.(v + w).|| - ||.(vv1 + y1).|| <= r

then (||.(v + w).|| - ||.(vv1 + y1).||) + ||.(vv1 + y1).|| <= ||.w.|| + ||.(vv1 + y1).|| by A47, XREAL_1:6, XXREAL_2:def 4;

then ||.(v + w).|| - ||.w.|| <= (||.w.|| + ||.(vv1 + y1).||) - ||.w.|| by XREAL_1:9;

hence ||.(v + w).|| - ||.w.|| <= ||.(vv1 + y1).|| ; :: thesis: verum

end;assume A53: y1 in Y ; :: thesis: ||.(v + w).|| - ||.w.|| <= ||.(vv1 + y1).||

A54: now :: thesis: for y2 being Point of X st y2 in Y holds

||.(v + w).|| - ||.(vv1 + y1).|| <= ||.(ww1 + y2).||

for r being ExtReal st r in NormVSets (X,Y,ww1) holds ||.(v + w).|| - ||.(vv1 + y1).|| <= ||.(ww1 + y2).||

let y2 be Point of X; :: thesis: ( y2 in Y implies ||.(v + w).|| - ||.(vv1 + y1).|| <= ||.(ww1 + y2).|| )

assume y2 in Y ; :: thesis: ||.(v + w).|| - ||.(vv1 + y1).|| <= ||.(ww1 + y2).||

then ||.(v + w).|| - ||.(vv1 + y1).|| <= (||.(vv1 + y1).|| + ||.(ww1 + y2).||) - ||.(vv1 + y1).|| by A50, A53, XREAL_1:9;

hence ||.(v + w).|| - ||.(vv1 + y1).|| <= ||.(ww1 + y2).|| ; :: thesis: verum

end;assume y2 in Y ; :: thesis: ||.(v + w).|| - ||.(vv1 + y1).|| <= ||.(ww1 + y2).||

then ||.(v + w).|| - ||.(vv1 + y1).|| <= (||.(vv1 + y1).|| + ||.(ww1 + y2).||) - ||.(vv1 + y1).|| by A50, A53, XREAL_1:9;

hence ||.(v + w).|| - ||.(vv1 + y1).|| <= ||.(ww1 + y2).|| ; :: thesis: verum

||.(v + w).|| - ||.(vv1 + y1).|| <= r

proof

then
||.(v + w).|| - ||.(vv1 + y1).|| is LowerBound of NormVSets (X,Y,ww1)
by XXREAL_2:def 2;
let r be ExtReal; :: thesis: ( r in NormVSets (X,Y,ww1) implies ||.(v + w).|| - ||.(vv1 + y1).|| <= r )

assume r in NormVSets (X,Y,ww1) ; :: thesis: ||.(v + w).|| - ||.(vv1 + y1).|| <= r

then consider x being VECTOR of X such that

A55: ( r = ||.x.|| & x in ww1 + Y ) ;

consider y2 being VECTOR of X such that

A56: ( x = ww1 + y2 & y2 in Y ) by A55;

thus ||.(v + w).|| - ||.(vv1 + y1).|| <= r by A54, A55, A56; :: thesis: verum

end;assume r in NormVSets (X,Y,ww1) ; :: thesis: ||.(v + w).|| - ||.(vv1 + y1).|| <= r

then consider x being VECTOR of X such that

A55: ( r = ||.x.|| & x in ww1 + Y ) ;

consider y2 being VECTOR of X such that

A56: ( x = ww1 + y2 & y2 in Y ) by A55;

thus ||.(v + w).|| - ||.(vv1 + y1).|| <= r by A54, A55, A56; :: thesis: verum

then (||.(v + w).|| - ||.(vv1 + y1).||) + ||.(vv1 + y1).|| <= ||.w.|| + ||.(vv1 + y1).|| by A47, XREAL_1:6, XXREAL_2:def 4;

then ||.(v + w).|| - ||.w.|| <= (||.w.|| + ||.(vv1 + y1).||) - ||.w.|| by XREAL_1:9;

hence ||.(v + w).|| - ||.w.|| <= ||.(vv1 + y1).|| ; :: thesis: verum

||.(v + w).|| - ||.w.|| <= r

proof

then
||.(v + w).|| - ||.w.|| is LowerBound of NormVSets (X,Y,vv1)
by XXREAL_2:def 2;
let r be ExtReal; :: thesis: ( r in NormVSets (X,Y,vv1) implies ||.(v + w).|| - ||.w.|| <= r )

assume r in NormVSets (X,Y,vv1) ; :: thesis: ||.(v + w).|| - ||.w.|| <= r

then consider x being VECTOR of X such that

A58: ( r = ||.x.|| & x in vv1 + Y ) ;

consider y1 being VECTOR of X such that

A59: ( x = vv1 + y1 & y1 in Y ) by A58;

thus ||.(v + w).|| - ||.w.|| <= r by A52, A58, A59; :: thesis: verum

end;assume r in NormVSets (X,Y,vv1) ; :: thesis: ||.(v + w).|| - ||.w.|| <= r

then consider x being VECTOR of X such that

A58: ( r = ||.x.|| & x in vv1 + Y ) ;

consider y1 being VECTOR of X such that

A59: ( x = vv1 + y1 & y1 in Y ) by A58;

thus ||.(v + w).|| - ||.w.|| <= r by A52, A58, A59; :: thesis: verum

then (||.(v + w).|| - ||.w.||) + ||.w.|| <= ||.v.|| + ||.w.|| by A45, XREAL_1:6, XXREAL_2:def 4;

hence ||.(v + w).|| <= ||.v.|| + ||.w.|| ; :: thesis: verum

then reconsider T = T as strict RealNormSpace by A4, A5, A6, A7, A8, A9, A10, A11, A15, A22;

take T ; :: thesis: ( RLSStruct(# the carrier of T, the ZeroF of T, the addF of T, the Mult of T #) = VectQuot (X,Y) & the normF of T = NormCoset (X,Y) )

thus ( RLSStruct(# the carrier of T, the ZeroF of T, the addF of T, the Mult of T #) = VectQuot (X,Y) & the normF of T = NormCoset (X,Y) ) ; :: thesis: verum