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)

proof

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;

for v being VECTOR of (NVectQuot (V,(Ker L)))
for r being Real holds QL . (r * v) = r * (QL . v)

proof

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;

then ( QL is additive & QL is homogeneous ) by A6, LOPBAN_1:def 5;
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

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 ;

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

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;

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).||

proof

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;

for r being ExtReal st r in NormVSets (V,(Ker L),vv1) holds
(1 / ||.PL.||) * ||.(QL . v).|| <= r

proof

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;

then A18: (1 / ||.PL.||) * ||.(QL . v).|| is LowerBound of NormVSets (V,(Ker L),vv1) by XXREAL_2:def 2;
||.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;

end;

end;

reconsider QL = QL as Lipschitzian LinearOperator of (NVectQuot (V,(Ker L))),(Im L) by A8, LOPBAN_1:def 8;
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.||

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;

then upper_bound (PreNorms QL) <= ||.PL.|| by SEQ_4:45;
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)

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;

then ||.PL.|| <= ||.PQL.|| by LMINEQ;
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