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 S1[ object , object ] means X = [Y,(T . Y)];
A2: for z being object st z in the carrier of () holds
ex x being object st
( x in the carrier of X & S1[z,x] )
proof
let z be object ; :: thesis: ( z in the carrier of () implies ex x being object st
( x in the carrier of X & S1[z,x] ) )

assume A3: z in the carrier of () ; :: thesis: ex x being object st
( x in the carrier of X & S1[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 ;
hence ex x being object st
( x in the carrier of X & S1[z,x] ) by A4; :: thesis: verum
end;
consider J being Function of (),X such that
A5: for z being object st z in the carrier of () holds
S1[z,J . z] from A6: graphNSP T is complete by ;
A7: ( graphNSP T is Subspace of [:X,Y:] & the normF of () = the normF of [:X,Y:] | the carrier of () ) by Th9;
A8: for x being VECTOR of ()
for r being Real holds J . (r * x) = r * (J . x)
proof
let x be VECTOR of (); :: 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 ;
then r * x = [(r * (J . x)),(r * (T . (J . x)))] by ;
hence J . (r * x) = r * (J . x) by ; :: thesis: verum
end;
for x, y being VECTOR of () holds J . (x + y) = (J . x) + (J . y)
proof
let x, y be VECTOR of (); :: 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 ;
then x + y = [((J . x) + (J . y)),((T . (J . x)) + (T . (J . y)))] by ;
hence J . (x + y) = (J . x) + (J . y) by ; :: thesis: verum
end;
then reconsider J = J as LinearOperator of (),X by ;
J is Lipschitzian
proof
A14: now :: thesis: for x being Point of () holds ||.(J . x).|| <= 1 *
let x be Point of (); :: thesis: ||.(J . x).|| <= 1 *
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 ;
hence ||.(J . x).|| <= 1 * by FUNCT_1:49; :: thesis: verum
end;
take 1 ; :: according to LOPBAN_1:def 8 :: thesis: ( 0 <= 1 & ( for b1 being Element of the carrier of () holds ||.(J . b1).|| <= 1 * ||.b1.|| ) )
thus ( 0 <= 1 & ( for b1 being Element of the carrier of () holds ||.(J . b1).|| <= 1 * ||.b1.|| ) ) by A14; :: thesis: verum
end;
then reconsider J = J as Lipschitzian LinearOperator of (),X ;
now :: thesis: for x, y being object st x in the carrier of () & y in the carrier of () & J . x = J . y holds
x = y
let x, y be object ; :: thesis: ( x in the carrier of () & y in the carrier of () & J . x = J . y implies x = y )
assume A16: ( x in the carrier of () & y in the carrier of () & J . x = J . y ) ; :: thesis: x = y
then reconsider x1 = x as Point of () ;
x1 = [(J . x1),(T . (J . x1))] by A5;
hence x = y by ; :: 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 ;
then reconsider x = [y1,(T . y1)] as Point of () 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,() by A17, Th7, A6;
consider K being Real such that
A19: ( 0 <= K & ( for x being VECTOR of X holds ||.(L . x).|| <= K * ) ) by LOPBAN_1:def 8;
now :: thesis: for y being Point of X holds ||.(T . y).|| <= K *
let y be Point of X; :: thesis: ||.(T . y).|| <= K *
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 () by FUNCT_1:1;
A20: x = [(J . x),(T . (J . x))] by A5;
A21: ||.(L . y).|| <= K * by A19;
x in the carrier of () ;
then A22: x in dom J by FUNCT_2:def 1;
A23: L . y = L . (J . x) by
.= x by ;
reconsider x1 = x as Point of [:X,Y:] ;
||.x1.|| = by FUNCT_1:49;
then ||.(T . y).|| <= ||.(L . y).|| by ;
hence ||.(T . y).|| <= K * by ; :: thesis: verum
end;
hence T is Lipschitzian by A19; :: thesis: verum