let T be LinearOperator of X,Y; :: thesis: ( T is closed implies T is Lipschitzian )
assume A1: T is closed ; :: thesis: T is Lipschitzian
defpred S₁[ object , object ] means X = [Y,(T . Y)];
A2: for z being object st z in the carrier of (graphNSP T) holds
ex x being object st
( x in the carrier of X & S₁[z,x] )

proof

let z be object ; :: thesis: ( z in the carrier of (graphNSP T) implies ex x being object st
( x in the carrier of X & S₁[z,x] ) )
assume A3: z in the carrier of (graphNSP T) ; :: thesis: ex x being object st
( x in the carrier of X & S₁[z,x] )
then consider x, y being object such that
A4: z = [x,y] by RELAT_1:def 1;
( x in dom T & y = T . x ) by FUNCT_1:1, A4, A3;
hence ex x being object st
( x in the carrier of X & S₁[z,x] ) by A4; :: thesis: verum

end;

consider J being Function of (graphNSP T),X such that
A5: for z being object st z in the carrier of (graphNSP T) holds
S₁[z,J . z] from FUNCT_2:sch 1(A2);
A6: graphNSP T is complete by Th11, A1;
A7: ( graphNSP T is Subspace of [:X,Y:] & the normF of (graphNSP T) = the normF of [:X,Y:] | the carrier of (graphNSP T) ) by Th9;
A8: for x being VECTOR of (graphNSP T)
for r being Real holds J . (r * x) = r * (J . x)

proof

let x be VECTOR of (graphNSP T); :: thesis: for r being Real holds J . (r * x) = r * (J . x)
let r be Real; :: thesis: J . (r * x) = r * (J . x)
A9: x = [(J . x),(T . (J . x))] by A5;
A10: r * x = [(J . (r * x)),(T . (J . (r * x)))] by A5;
x in graph T ;
then reconsider x1 = x as Point of [:X,Y:] ;
r * x1 = r * x by A7, RLSUB_1:14;
then r * x = [(r * (J . x)),(r * (T . (J . x)))] by PRVECT_3:18, A9;
hence J . (r * x) = r * (J . x) by A10, XTUPLE_0:1; :: thesis: verum

end;

for x, y being VECTOR of (graphNSP T) holds J . (x + y) = (J . x) + (J . y)

proof

let x, y be VECTOR of (graphNSP T); :: thesis: J . (x + y) = (J . x) + (J . y)
A11: x = [(J . x),(T . (J . x))] by A5;
A12: y = [(J . y),(T . (J . y))] by A5;
A13: x + y = [(J . (x + y)),(T . (J . (x + y)))] by A5;
( x in graph T & y in graph T ) ;
then reconsider x1 = x, y1 = y as Point of [:X,Y:] ;
x1 + y1 = x + y by A7, RLSUB_1:13;
then x + y = [((J . x) + (J . y)),((T . (J . x)) + (T . (J . y)))] by PRVECT_3:18, A11, A12;
hence J . (x + y) = (J . x) + (J . y) by A13, XTUPLE_0:1; :: thesis: verum

end;

then reconsider J = J as LinearOperator of (graphNSP T),X by A8, LOPBAN_1:def 5, VECTSP_1:def 20;
J is Lipschitzian

proof

A14: now :: thesis: for x being Point of (graphNSP T) holds ||.(J . x).|| <= 1 * ||.x.||

let x be Point of (graphNSP T); :: thesis: ||.(J . x).|| <= 1 * ||.x.||
x in graph T ;
then reconsider x1 = x as Point of [:X,Y:] ;
A15: x1 = [(J . x),(T . (J . x))] by A5;
||.(J . x).|| <= ||.x1.|| by A15, Th15;
hence ||.(J . x).|| <= 1 * ||.x.|| by FUNCT_1:49; :: thesis: verum

end;

take 1 ; :: according to LOPBAN_1:def 8 :: thesis: ( 0 <= 1 & ( for b₁ being Element of the carrier of (graphNSP T) holds ||.(J . b₁).|| <= 1 * ||.b₁.|| ) )
thus ( 0 <= 1 & ( for b₁ being Element of the carrier of (graphNSP T) holds ||.(J . b₁).|| <= 1 * ||.b₁.|| ) ) by A14; :: thesis: verum

end;

then reconsider J = J as Lipschitzian LinearOperator of (graphNSP T),X ;

now :: thesis: for x, y being object st x in the carrier of (graphNSP T) & y in the carrier of (graphNSP T) & J . x = J . y holds
x = y

let x, y be object ; :: thesis: ( x in the carrier of (graphNSP T) & y in the carrier of (graphNSP T) & J . x = J . y implies x = y )
assume A16: ( x in the carrier of (graphNSP T) & y in the carrier of (graphNSP T) & J . x = J . y ) ; :: thesis: x = y
then reconsider x1 = x as Point of (graphNSP T) ;
x1 = [(J . x1),(T . (J . x1))] by A5;
hence x = y by A5, A16; :: thesis: verum

end;

then A17: J is one-to-one by FUNCT_2:19;
for y being object holds
( y in rng J iff y in the carrier of X )

proof

let y be object ; :: thesis: ( y in rng J iff y in the carrier of X )

now :: thesis: ( y in the carrier of X implies y in rng J )

assume A18: y in the carrier of X ; :: thesis: y in rng J
then reconsider y1 = y as Point of X ;
y1 in dom T by A18, FUNCT_2:def 1;
then reconsider x = [y1,(T . y1)] as Point of (graphNSP T) by FUNCT_1:1;
x = [(J . x),(T . (J . x))] by A5;
then y1 = J . x by XTUPLE_0:1;
hence y in rng J by FUNCT_2:112; :: thesis: verum

end;

hence ( y in rng J iff y in the carrier of X ) ; :: thesis: verum

end;

then J is onto by TARSKI:2;
then reconsider L = J " as Lipschitzian LinearOperator of X,(graphNSP T) by A17, Th7, A6;
consider K being Real such that
A19: ( 0 <= K & ( for x being VECTOR of X holds ||.(L . x).|| <= K * ||.x.|| ) ) by LOPBAN_1:def 8;

now :: thesis: for y being Point of X holds ||.(T . y).|| <= K * ||.y.||

let y be Point of X; :: thesis: ||.(T . y).|| <= K * ||.y.||
y in the carrier of X ;
then y in dom T by FUNCT_2:def 1;
then reconsider x = [y,(T . y)] as Point of (graphNSP T) by FUNCT_1:1;
A20: x = [(J . x),(T . (J . x))] by A5;
A21: ||.(L . y).|| <= K * ||.y.|| by A19;
x in the carrier of (graphNSP T) ;
then A22: x in dom J by FUNCT_2:def 1;
A23: L . y = L . (J . x) by XTUPLE_0:1, A20
.= x by FUNCT_1:34, A17, A22 ;
reconsider x1 = x as Point of [:X,Y:] ;
||.x1.|| = ||.x.|| by FUNCT_1:49;
then ||.(T . y).|| <= ||.(L . y).|| by A23, Th15;
hence ||.(T . y).|| <= K * ||.y.|| by A21, XXREAL_0:2; :: thesis: verum

end;

hence T is Lipschitzian by A19; :: thesis: verum