let V, W be RealNormSpace; :: thesis: for L being Lipschitzian LinearOperator of V,W ex QL being Lipschitzian LinearOperator of (NVectQuot (V,(Ker L))),(Im L) ex PQL being Point of (R_NormSpace_of_BoundedLinearOperators ((NVectQuot (V,(Ker L))),(Im L))) ex PL being Point of (R_NormSpace_of_BoundedLinearOperators (V,W)) st

( QL is onto & QL is one-to-one & L = PL & QL = PQL & ||.PL.|| = ||.PQL.|| & ( for z being Point of (NVectQuot (V,(Ker L)))

for v being VECTOR of V st z = v + (Ker L) holds

QL . z = L . v ) )

let L be Lipschitzian LinearOperator of V,W; :: thesis: ex QL being Lipschitzian LinearOperator of (NVectQuot (V,(Ker L))),(Im L) ex PQL being Point of (R_NormSpace_of_BoundedLinearOperators ((NVectQuot (V,(Ker L))),(Im L))) ex PL being Point of (R_NormSpace_of_BoundedLinearOperators (V,W)) st

( QL is onto & QL is one-to-one & L = PL & QL = PQL & ||.PL.|| = ||.PQL.|| & ( for z being Point of (NVectQuot (V,(Ker L)))

for v being VECTOR of V st z = v + (Ker L) holds

QL . z = L . v ) )

A1: ( the carrier of (Ker L) = L " {(0. W)} & L " {(0. W)} is closed ) by KERCL01, KLXY1, LCL1, LOPBAN_7:6;

reconsider V1 = V as RealLinearSpace ;

reconsider W1 = W as RealLinearSpace ;

reconsider L1 = L as LinearOperator of V1,W1 ;

A2: ( RLSStruct(# the carrier of (NVectQuot (V,(Ker L))), the ZeroF of (NVectQuot (V,(Ker L))), the addF of (NVectQuot (V,(Ker L))), the Mult of (NVectQuot (V,(Ker L))) #) = VectQuot (V,(Ker L)) & the normF of (NVectQuot (V,(Ker L))) = NormCoset (V,(Ker L)) ) by A1, defQuotN;

A3: the carrier of (VectQuot (V,(Ker L))) = CosetSet (V,(Ker L)) by LMQ06;

consider QL1 being LinearOperator of (VectQuot (V1,(Ker L1))),(Im L1) such that

A4: ( QL1 is isomorphism & ( for z being Point of (VectQuot (V1,(Ker L1)))

for v being VECTOR of V1 st z = v + (Ker L1) holds

QL1 . z = L1 . v ) ) by LMQ21;

reconsider KL1 = Ker L1 as Subspace of V ;

A5: RLSStruct(# the carrier of (NVectQuot (V,(Ker L))), the ZeroF of (NVectQuot (V,(Ker L))), the addF of (NVectQuot (V,(Ker L))), the Mult of (NVectQuot (V,(Ker L))) #) = VectQuot (V,KL1) by A1, defQuotN;

reconsider QL = QL1 as Function of (NVectQuot (V,(Ker L))),(Im L) by A5;

A6: for v, w being Element of (NVectQuot (V,(Ker L))) holds QL . (v + w) = (QL . v) + (QL . w)

for r being Real holds QL . (r * v) = r * (QL . v)

then reconsider QL = QL as LinearOperator of (NVectQuot (V,(Ker L))),(Im L) ;

A7: R_NormSpace_of_BoundedLinearOperators (V,W) = NORMSTR(# (BoundedLinearOperators (V,W)),(Zero_ ((BoundedLinearOperators (V,W)),(R_VectorSpace_of_LinearOperators (V,W)))),(Add_ ((BoundedLinearOperators (V,W)),(R_VectorSpace_of_LinearOperators (V,W)))),(Mult_ ((BoundedLinearOperators (V,W)),(R_VectorSpace_of_LinearOperators (V,W)))),(BoundedLinearOperatorsNorm (V,W)) #) by LOPBAN_1:def 14;

reconsider PL = L as Point of (R_NormSpace_of_BoundedLinearOperators (V,W)) by A7, LOPBAN_1:def 9;

A8: for v being Point of (NVectQuot (V,(Ker L))) holds ||.(QL . v).|| <= ||.PL.|| * ||.v.||

take QL ; :: thesis: ex PQL being Point of (R_NormSpace_of_BoundedLinearOperators ((NVectQuot (V,(Ker L))),(Im L))) ex PL being Point of (R_NormSpace_of_BoundedLinearOperators (V,W)) st

( QL is onto & QL is one-to-one & L = PL & QL = PQL & ||.PL.|| = ||.PQL.|| & ( for z being Point of (NVectQuot (V,(Ker L)))

for v being VECTOR of V st z = v + (Ker L) holds

QL . z = L . v ) )

A19: R_NormSpace_of_BoundedLinearOperators ((NVectQuot (V,(Ker L))),(Im L)) = NORMSTR(# (BoundedLinearOperators ((NVectQuot (V,(Ker L))),(Im L))),(Zero_ ((BoundedLinearOperators ((NVectQuot (V,(Ker L))),(Im L))),(R_VectorSpace_of_LinearOperators ((NVectQuot (V,(Ker L))),(Im L))))),(Add_ ((BoundedLinearOperators ((NVectQuot (V,(Ker L))),(Im L))),(R_VectorSpace_of_LinearOperators ((NVectQuot (V,(Ker L))),(Im L))))),(Mult_ ((BoundedLinearOperators ((NVectQuot (V,(Ker L))),(Im L))),(R_VectorSpace_of_LinearOperators ((NVectQuot (V,(Ker L))),(Im L))))),(BoundedLinearOperatorsNorm ((NVectQuot (V,(Ker L))),(Im L))) #) by LOPBAN_1:def 14;

then reconsider PQL = QL as Point of (R_NormSpace_of_BoundedLinearOperators ((NVectQuot (V,(Ker L))),(Im L))) by LOPBAN_1:def 9;

A20: PreNorms QL = { ||.(QL . t).|| where t is VECTOR of (NVectQuot (V,(Ker L))) : ||.t.|| <= 1 } by LOPBAN_1:def 12;

then A24: ||.PQL.|| <= ||.PL.|| by A19, LOPBAN_1:30;

R_NormSpace_of_BoundedLinearOperators (V,W) = NORMSTR(# (BoundedLinearOperators (V,W)),(Zero_ ((BoundedLinearOperators (V,W)),(R_VectorSpace_of_LinearOperators (V,W)))),(Add_ ((BoundedLinearOperators (V,W)),(R_VectorSpace_of_LinearOperators (V,W)))),(Mult_ ((BoundedLinearOperators (V,W)),(R_VectorSpace_of_LinearOperators (V,W)))),(BoundedLinearOperatorsNorm (V,W)) #) by LOPBAN_1:def 14;

then A26: ||.PL.|| = upper_bound (PreNorms L) by LOPBAN_1:30;

A27: ( not PreNorms L is empty & PreNorms L is bounded_above ) by LOPBAN_1:27;

A28: PreNorms L = { ||.(L . t).|| where t is VECTOR of V : ||.t.|| <= 1 } by LOPBAN_1:def 12;

hence ex PQL being Point of (R_NormSpace_of_BoundedLinearOperators ((NVectQuot (V,(Ker L))),(Im L))) ex PL being Point of (R_NormSpace_of_BoundedLinearOperators (V,W)) st

( QL is onto & QL is one-to-one & L = PL & QL = PQL & ||.PL.|| = ||.PQL.|| & ( for z being Point of (NVectQuot (V,(Ker L)))

for v being VECTOR of V st z = v + (Ker L) holds

QL . z = L . v ) ) by A4, A5, A24, XXREAL_0:1; :: thesis: verum

( QL is onto & QL is one-to-one & L = PL & QL = PQL & ||.PL.|| = ||.PQL.|| & ( for z being Point of (NVectQuot (V,(Ker L)))

for v being VECTOR of V st z = v + (Ker L) holds

QL . z = L . v ) )

let L be Lipschitzian LinearOperator of V,W; :: thesis: ex QL being Lipschitzian LinearOperator of (NVectQuot (V,(Ker L))),(Im L) ex PQL being Point of (R_NormSpace_of_BoundedLinearOperators ((NVectQuot (V,(Ker L))),(Im L))) ex PL being Point of (R_NormSpace_of_BoundedLinearOperators (V,W)) st

( QL is onto & QL is one-to-one & L = PL & QL = PQL & ||.PL.|| = ||.PQL.|| & ( for z being Point of (NVectQuot (V,(Ker L)))

for v being VECTOR of V st z = v + (Ker L) holds

QL . z = L . v ) )

A1: ( the carrier of (Ker L) = L " {(0. W)} & L " {(0. W)} is closed ) by KERCL01, KLXY1, LCL1, LOPBAN_7:6;

reconsider V1 = V as RealLinearSpace ;

reconsider W1 = W as RealLinearSpace ;

reconsider L1 = L as LinearOperator of V1,W1 ;

A2: ( RLSStruct(# the carrier of (NVectQuot (V,(Ker L))), the ZeroF of (NVectQuot (V,(Ker L))), the addF of (NVectQuot (V,(Ker L))), the Mult of (NVectQuot (V,(Ker L))) #) = VectQuot (V,(Ker L)) & the normF of (NVectQuot (V,(Ker L))) = NormCoset (V,(Ker L)) ) by A1, defQuotN;

A3: the carrier of (VectQuot (V,(Ker L))) = CosetSet (V,(Ker L)) by LMQ06;

consider QL1 being LinearOperator of (VectQuot (V1,(Ker L1))),(Im L1) such that

A4: ( QL1 is isomorphism & ( for z being Point of (VectQuot (V1,(Ker L1)))

for v being VECTOR of V1 st z = v + (Ker L1) holds

QL1 . z = L1 . v ) ) by LMQ21;

reconsider KL1 = Ker L1 as Subspace of V ;

A5: RLSStruct(# the carrier of (NVectQuot (V,(Ker L))), the ZeroF of (NVectQuot (V,(Ker L))), the addF of (NVectQuot (V,(Ker L))), the Mult of (NVectQuot (V,(Ker L))) #) = VectQuot (V,KL1) by A1, defQuotN;

reconsider QL = QL1 as Function of (NVectQuot (V,(Ker L))),(Im L) by A5;

A6: for v, w being Element of (NVectQuot (V,(Ker L))) holds QL . (v + w) = (QL . v) + (QL . w)

proof

for v being VECTOR of (NVectQuot (V,(Ker L)))
let v, w be Element of (NVectQuot (V,(Ker L))); :: thesis: QL . (v + w) = (QL . v) + (QL . w)

reconsider v1 = v, w1 = w as Element of (VectQuot (V1,(Ker L1))) by A5;

thus QL . (v + w) = QL1 . (v1 + w1) by A5

.= (QL1 . v1) + (QL1 . w1) by VECTSP_1:def 20

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

end;reconsider v1 = v, w1 = w as Element of (VectQuot (V1,(Ker L1))) by A5;

thus QL . (v + w) = QL1 . (v1 + w1) by A5

.= (QL1 . v1) + (QL1 . w1) by VECTSP_1:def 20

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

for r being Real holds QL . (r * v) = r * (QL . v)

proof

then
( QL is additive & QL is homogeneous )
by A6, LOPBAN_1:def 5;
let v be VECTOR of (NVectQuot (V,(Ker L))); :: thesis: for r being Real holds QL . (r * v) = r * (QL . v)

let r be Real; :: thesis: QL . (r * v) = r * (QL . v)

reconsider v1 = v as Element of (VectQuot (V1,(Ker L1))) by A5;

thus QL . (r * v) = QL1 . (r * v1) by A5

.= r * (QL1 . v1) by LOPBAN_1:def 5

.= r * (QL . v) ; :: thesis: verum

end;let r be Real; :: thesis: QL . (r * v) = r * (QL . v)

reconsider v1 = v as Element of (VectQuot (V1,(Ker L1))) by A5;

thus QL . (r * v) = QL1 . (r * v1) by A5

.= r * (QL1 . v1) by LOPBAN_1:def 5

.= r * (QL . v) ; :: thesis: verum

then reconsider QL = QL as LinearOperator of (NVectQuot (V,(Ker L))),(Im L) ;

A7: R_NormSpace_of_BoundedLinearOperators (V,W) = NORMSTR(# (BoundedLinearOperators (V,W)),(Zero_ ((BoundedLinearOperators (V,W)),(R_VectorSpace_of_LinearOperators (V,W)))),(Add_ ((BoundedLinearOperators (V,W)),(R_VectorSpace_of_LinearOperators (V,W)))),(Mult_ ((BoundedLinearOperators (V,W)),(R_VectorSpace_of_LinearOperators (V,W)))),(BoundedLinearOperatorsNorm (V,W)) #) by LOPBAN_1:def 14;

reconsider PL = L as Point of (R_NormSpace_of_BoundedLinearOperators (V,W)) by A7, LOPBAN_1:def 9;

A8: for v being Point of (NVectQuot (V,(Ker L))) holds ||.(QL . v).|| <= ||.PL.|| * ||.v.||

proof

reconsider QL = QL as Lipschitzian LinearOperator of (NVectQuot (V,(Ker L))),(Im L) by A8, LOPBAN_1:def 8;
let v be Point of (NVectQuot (V,(Ker L))); :: thesis: ||.(QL . v).|| <= ||.PL.|| * ||.v.||

reconsider v1 = v as Element of (VectQuot (V,(Ker L))) by A5;

consider vv1 being Point of V such that

A9: v1 = vv1 + (Ker L) by LMQ07;

A10: ||.v.|| = (NormCoset (V,(Ker L))) . v1 by A1, defQuotN

.= lower_bound (NormVSets (V,(Ker L),vv1)) by A3, A9, DeNorm ;

end;reconsider v1 = v as Element of (VectQuot (V,(Ker L))) by A5;

consider vv1 being Point of V such that

A9: v1 = vv1 + (Ker L) by LMQ07;

A10: ||.v.|| = (NormCoset (V,(Ker L))) . v1 by A1, defQuotN

.= lower_bound (NormVSets (V,(Ker L),vv1)) by A3, A9, DeNorm ;

per cases
( ||.PL.|| = 0 or ||.PL.|| <> 0 )
;

end;

suppose
||.PL.|| = 0
; :: thesis: ||.(QL . v).|| <= ||.PL.|| * ||.v.||

then
PL = 0. (R_NormSpace_of_BoundedLinearOperators (V,W))
by NORMSP_0:def 5;

then A11: the carrier of V --> (0. W) = L by LOPBAN_1:31;

QL . v = L . vv1 by A4, A9

.= 0. W by A11, FUNCOP_1:7 ;

then ||.(QL . v).|| = ||.(0. W).|| by SUBTH0;

hence ||.(QL . v).|| <= ||.PL.|| * ||.v.|| ; :: thesis: verum

end;then A11: the carrier of V --> (0. W) = L by LOPBAN_1:31;

QL . v = L . vv1 by A4, A9

.= 0. W by A11, FUNCOP_1:7 ;

then ||.(QL . v).|| = ||.(0. W).|| by SUBTH0;

hence ||.(QL . v).|| <= ||.PL.|| * ||.v.|| ; :: thesis: verum

suppose A12:
||.PL.|| <> 0
; :: thesis: ||.(QL . v).|| <= ||.PL.|| * ||.v.||

set a = ||.PL.||;

A13: for y being VECTOR of V st y in Ker L holds

(1 / ||.PL.||) * ||.(QL . v).|| <= ||.(vv1 + y).||

(1 / ||.PL.||) * ||.(QL . v).|| <= r

||.PL.|| * ((1 / ||.PL.||) * ||.(QL . v).||) <= ||.PL.|| * ||.v.|| by A10, A18, XREAL_1:64, XXREAL_2:def 4;

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

then 1 * ||.(QL . v).|| <= ||.PL.|| * ||.v.|| by A12, XCMPLX_1:106;

hence ||.(QL . v).|| <= ||.PL.|| * ||.v.|| ; :: thesis: verum

end;A13: for y being VECTOR of V st y in Ker L holds

(1 / ||.PL.||) * ||.(QL . v).|| <= ||.(vv1 + y).||

proof

for r being ExtReal st r in NormVSets (V,(Ker L),vv1) holds
let y be VECTOR of V; :: thesis: ( y in Ker L implies (1 / ||.PL.||) * ||.(QL . v).|| <= ||.(vv1 + y).|| )

assume y in Ker L ; :: thesis: (1 / ||.PL.||) * ||.(QL . v).|| <= ||.(vv1 + y).||

then y in L " {(0. W)} by KLXY1, LCL1;

then A14: ( y in the carrier of V & L . y in {(0. W)} ) by FUNCT_2:38;

A15: QL . v = L . vv1 by A4, A9

.= (L . vv1) + (0. W) by RLVECT_1:4

.= (L . vv1) + (L . y) by A14, TARSKI:def 1

.= L . (vv1 + y) by VECTSP_1:def 20 ;

(1 / ||.PL.||) * ||.(L . (vv1 + y)).|| <= (1 / ||.PL.||) * (||.PL.|| * ||.(vv1 + y).||) by LOPBAN_1:32, XREAL_1:64;

then (1 / ||.PL.||) * ||.(L . (vv1 + y)).|| <= ((1 / ||.PL.||) * ||.PL.||) * ||.(vv1 + y).|| ;

then (1 / ||.PL.||) * ||.(L . (vv1 + y)).|| <= 1 * ||.(vv1 + y).|| by A12, XCMPLX_1:106;

hence (1 / ||.PL.||) * ||.(QL . v).|| <= ||.(vv1 + y).|| by A15, SUBTH0; :: thesis: verum

end;assume y in Ker L ; :: thesis: (1 / ||.PL.||) * ||.(QL . v).|| <= ||.(vv1 + y).||

then y in L " {(0. W)} by KLXY1, LCL1;

then A14: ( y in the carrier of V & L . y in {(0. W)} ) by FUNCT_2:38;

A15: QL . v = L . vv1 by A4, A9

.= (L . vv1) + (0. W) by RLVECT_1:4

.= (L . vv1) + (L . y) by A14, TARSKI:def 1

.= L . (vv1 + y) by VECTSP_1:def 20 ;

(1 / ||.PL.||) * ||.(L . (vv1 + y)).|| <= (1 / ||.PL.||) * (||.PL.|| * ||.(vv1 + y).||) by LOPBAN_1:32, XREAL_1:64;

then (1 / ||.PL.||) * ||.(L . (vv1 + y)).|| <= ((1 / ||.PL.||) * ||.PL.||) * ||.(vv1 + y).|| ;

then (1 / ||.PL.||) * ||.(L . (vv1 + y)).|| <= 1 * ||.(vv1 + y).|| by A12, XCMPLX_1:106;

hence (1 / ||.PL.||) * ||.(QL . v).|| <= ||.(vv1 + y).|| by A15, SUBTH0; :: thesis: verum

(1 / ||.PL.||) * ||.(QL . v).|| <= r

proof

then A18:
(1 / ||.PL.||) * ||.(QL . v).|| is LowerBound of NormVSets (V,(Ker L),vv1)
by XXREAL_2:def 2;
let r be ExtReal; :: thesis: ( r in NormVSets (V,(Ker L),vv1) implies (1 / ||.PL.||) * ||.(QL . v).|| <= r )

assume r in NormVSets (V,(Ker L),vv1) ; :: thesis: (1 / ||.PL.||) * ||.(QL . v).|| <= r

then consider x being VECTOR of V such that

A16: ( r = ||.x.|| & x in vv1 + (Ker L) ) ;

consider y being VECTOR of V such that

A17: ( x = vv1 + y & y in Ker L ) by A16;

thus (1 / ||.PL.||) * ||.(QL . v).|| <= r by A13, A16, A17; :: thesis: verum

end;assume r in NormVSets (V,(Ker L),vv1) ; :: thesis: (1 / ||.PL.||) * ||.(QL . v).|| <= r

then consider x being VECTOR of V such that

A16: ( r = ||.x.|| & x in vv1 + (Ker L) ) ;

consider y being VECTOR of V such that

A17: ( x = vv1 + y & y in Ker L ) by A16;

thus (1 / ||.PL.||) * ||.(QL . v).|| <= r by A13, A16, A17; :: thesis: verum

||.PL.|| * ((1 / ||.PL.||) * ||.(QL . v).||) <= ||.PL.|| * ||.v.|| by A10, A18, XREAL_1:64, XXREAL_2:def 4;

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

then 1 * ||.(QL . v).|| <= ||.PL.|| * ||.v.|| by A12, XCMPLX_1:106;

hence ||.(QL . v).|| <= ||.PL.|| * ||.v.|| ; :: thesis: verum

take QL ; :: thesis: ex PQL being Point of (R_NormSpace_of_BoundedLinearOperators ((NVectQuot (V,(Ker L))),(Im L))) ex PL being Point of (R_NormSpace_of_BoundedLinearOperators (V,W)) st

( QL is onto & QL is one-to-one & L = PL & QL = PQL & ||.PL.|| = ||.PQL.|| & ( for z being Point of (NVectQuot (V,(Ker L)))

for v being VECTOR of V st z = v + (Ker L) holds

QL . z = L . v ) )

A19: R_NormSpace_of_BoundedLinearOperators ((NVectQuot (V,(Ker L))),(Im L)) = NORMSTR(# (BoundedLinearOperators ((NVectQuot (V,(Ker L))),(Im L))),(Zero_ ((BoundedLinearOperators ((NVectQuot (V,(Ker L))),(Im L))),(R_VectorSpace_of_LinearOperators ((NVectQuot (V,(Ker L))),(Im L))))),(Add_ ((BoundedLinearOperators ((NVectQuot (V,(Ker L))),(Im L))),(R_VectorSpace_of_LinearOperators ((NVectQuot (V,(Ker L))),(Im L))))),(Mult_ ((BoundedLinearOperators ((NVectQuot (V,(Ker L))),(Im L))),(R_VectorSpace_of_LinearOperators ((NVectQuot (V,(Ker L))),(Im L))))),(BoundedLinearOperatorsNorm ((NVectQuot (V,(Ker L))),(Im L))) #) by LOPBAN_1:def 14;

then reconsider PQL = QL as Point of (R_NormSpace_of_BoundedLinearOperators ((NVectQuot (V,(Ker L))),(Im L))) by LOPBAN_1:def 9;

A20: PreNorms QL = { ||.(QL . t).|| where t is VECTOR of (NVectQuot (V,(Ker L))) : ||.t.|| <= 1 } by LOPBAN_1:def 12;

now :: thesis: for r being Real st r in PreNorms QL holds

r <= ||.PL.||

then
upper_bound (PreNorms QL) <= ||.PL.||
by SEQ_4:45;r <= ||.PL.||

let r be Real; :: thesis: ( r in PreNorms QL implies r <= ||.PL.|| )

assume r in PreNorms QL ; :: thesis: r <= ||.PL.||

then consider v being VECTOR of (NVectQuot (V,(Ker L))) such that

A21: r = ||.(QL . v).|| and

A22: ||.v.|| <= 1 by A20;

A23: ||.(QL . v).|| <= ||.PL.|| * ||.v.|| by A8;

||.PL.|| * ||.v.|| <= ||.PL.|| * 1 by A22, XREAL_1:64;

hence r <= ||.PL.|| by A21, A23, XXREAL_0:2; :: thesis: verum

end;assume r in PreNorms QL ; :: thesis: r <= ||.PL.||

then consider v being VECTOR of (NVectQuot (V,(Ker L))) such that

A21: r = ||.(QL . v).|| and

A22: ||.v.|| <= 1 by A20;

A23: ||.(QL . v).|| <= ||.PL.|| * ||.v.|| by A8;

||.PL.|| * ||.v.|| <= ||.PL.|| * 1 by A22, XREAL_1:64;

hence r <= ||.PL.|| by A21, A23, XXREAL_0:2; :: thesis: verum

then A24: ||.PQL.|| <= ||.PL.|| by A19, LOPBAN_1:30;

R_NormSpace_of_BoundedLinearOperators (V,W) = NORMSTR(# (BoundedLinearOperators (V,W)),(Zero_ ((BoundedLinearOperators (V,W)),(R_VectorSpace_of_LinearOperators (V,W)))),(Add_ ((BoundedLinearOperators (V,W)),(R_VectorSpace_of_LinearOperators (V,W)))),(Mult_ ((BoundedLinearOperators (V,W)),(R_VectorSpace_of_LinearOperators (V,W)))),(BoundedLinearOperatorsNorm (V,W)) #) by LOPBAN_1:def 14;

then A26: ||.PL.|| = upper_bound (PreNorms L) by LOPBAN_1:30;

A27: ( not PreNorms L is empty & PreNorms L is bounded_above ) by LOPBAN_1:27;

A28: PreNorms L = { ||.(L . t).|| where t is VECTOR of V : ||.t.|| <= 1 } by LOPBAN_1:def 12;

now :: thesis: for s being Real st 0 < s holds

||.PL.|| <= ||.PQL.|| + (1 * s)

then
||.PL.|| <= ||.PQL.||
by LMINEQ;||.PL.|| <= ||.PQL.|| + (1 * s)

let s be Real; :: thesis: ( 0 < s implies ||.PL.|| <= ||.PQL.|| + (1 * s) )

assume 0 < s ; :: thesis: ||.PL.|| <= ||.PQL.|| + (1 * s)

then consider p being Real such that

A29: ( p in PreNorms L & ||.PL.|| - s < p ) by A26, A27, SEQ_4:def 1;

consider vv1 being VECTOR of V such that

A30: p = ||.(L . vv1).|| and

A31: ||.vv1.|| <= 1 by A28, A29;

A32: lower_bound (NormVSets (V,(Ker L),vv1)) <= ||.vv1.|| by LMQ23;

reconsider v = vv1 + (Ker L) as Point of (NVectQuot (V,(Ker L))) by A2, LMQ07;

||.v.|| = lower_bound (NormVSets (V,(Ker L),vv1)) by A2, DeNorm;

then A33: ||.v.|| <= 1 by A31, A32, XXREAL_0:2;

QL . v = L . vv1 by A4, A5;

then A34: ||.(QL . v).|| = ||.(L . vv1).|| by SUBTH0;

A35: ||.(QL . v).|| <= ||.PQL.|| * ||.v.|| by LOPBAN_1:32;

||.PQL.|| * ||.v.|| <= ||.PQL.|| * 1 by A33, XREAL_1:64;

then ||.(QL . v).|| <= ||.PQL.|| by A35, XXREAL_0:2;

then ||.PL.|| - s <= ||.PQL.|| by A29, A30, A34, XXREAL_0:2;

then (||.PL.|| - s) + s <= ||.PQL.|| + s by XREAL_1:6;

hence ||.PL.|| <= ||.PQL.|| + (1 * s) ; :: thesis: verum

end;assume 0 < s ; :: thesis: ||.PL.|| <= ||.PQL.|| + (1 * s)

then consider p being Real such that

A29: ( p in PreNorms L & ||.PL.|| - s < p ) by A26, A27, SEQ_4:def 1;

consider vv1 being VECTOR of V such that

A30: p = ||.(L . vv1).|| and

A31: ||.vv1.|| <= 1 by A28, A29;

A32: lower_bound (NormVSets (V,(Ker L),vv1)) <= ||.vv1.|| by LMQ23;

reconsider v = vv1 + (Ker L) as Point of (NVectQuot (V,(Ker L))) by A2, LMQ07;

||.v.|| = lower_bound (NormVSets (V,(Ker L),vv1)) by A2, DeNorm;

then A33: ||.v.|| <= 1 by A31, A32, XXREAL_0:2;

QL . v = L . vv1 by A4, A5;

then A34: ||.(QL . v).|| = ||.(L . vv1).|| by SUBTH0;

A35: ||.(QL . v).|| <= ||.PQL.|| * ||.v.|| by LOPBAN_1:32;

||.PQL.|| * ||.v.|| <= ||.PQL.|| * 1 by A33, XREAL_1:64;

then ||.(QL . v).|| <= ||.PQL.|| by A35, XXREAL_0:2;

then ||.PL.|| - s <= ||.PQL.|| by A29, A30, A34, XXREAL_0:2;

then (||.PL.|| - s) + s <= ||.PQL.|| + s by XREAL_1:6;

hence ||.PL.|| <= ||.PQL.|| + (1 * s) ; :: thesis: verum

hence ex PQL being Point of (R_NormSpace_of_BoundedLinearOperators ((NVectQuot (V,(Ker L))),(Im L))) ex PL being Point of (R_NormSpace_of_BoundedLinearOperators (V,W)) st

( QL is onto & QL is one-to-one & L = PL & QL = PQL & ||.PL.|| = ||.PQL.|| & ( for z being Point of (NVectQuot (V,(Ker L)))

for v being VECTOR of V st z = v + (Ker L) holds

QL . z = L . v ) ) by A4, A5, A24, XXREAL_0:1; :: thesis: verum