let E, F be RealNormSpace; :: thesis: ex L20 being Lipschitzian LinearOperator of F,[:E,F:] st
for dy being Point of F holds L20 . dy = [(0. E),dy]
defpred S₁[ object , object ] means ex dx being Point of F st
( dx = $1 & $2 = [(0. E),dx] );
A1: for x being object st x in the carrier of F holds
ex y being object st
( y in the carrier of [:E,F:] & S₁[x,y] )

proof

let x be object ; :: thesis: ( x in the carrier of F implies ex y being object st
( y in the carrier of [:E,F:] & S₁[x,y] ) )
assume x in the carrier of F ; :: thesis: ex y being object st
( y in the carrier of [:E,F:] & S₁[x,y] )
then reconsider V1 = x as Point of F ;
take y = [(0. E),V1]; :: thesis: ( y in the carrier of [:E,F:] & S₁[x,y] )
thus ( y in the carrier of [:E,F:] & S₁[x,y] ) ; :: thesis: verum

end;

consider L1 being Function of the carrier of F, the carrier of [:E,F:] such that
A2: for x being object st x in the carrier of F holds
S₁[x,L1 . x] from FUNCT_2:sch 1(A1);
A3: for dx being Point of F holds L1 . dx = [(0. E),dx]

proof

let dx be Point of F; :: thesis: L1 . dx = [(0. E),dx]
ex V1 being Point of F st
( V1 = dx & L1 . dx = [(0. E),V1] ) by A2;
hence L1 . dx = [(0. E),dx] ; :: thesis: verum

end;

for x, y being Element of F holds L1 . (x + y) = (L1 . x) + (L1 . y)

proof

let x, y be Element of F; :: thesis: L1 . (x + y) = (L1 . x) + (L1 . y)
A4: L1 . x = [(0. E),x] by A3;
A5: L1 . y = [(0. E),y] by A3;
thus L1 . (x + y) = [(0. E),(x + y)] by A3
.= [((0. E) + (0. E)),(x + y)] by RLVECT_1:4
.= (L1 . x) + (L1 . y) by A4, A5, PRVECT_3:18 ; :: thesis: verum

end;

then A6: L1 is additive ;
for x being VECTOR of F
for a being Real holds L1 . (a * x) = a * (L1 . x)

proof

let x be VECTOR of F; :: thesis: for a being Real holds L1 . (a * x) = a * (L1 . x)
let a be Real; :: thesis: L1 . (a * x) = a * (L1 . x)
A7: L1 . x = [(0. E),x] by A3;
thus L1 . (a * x) = [(0. E),(a * x)] by A3
.= [(a * (0. E)),(a * x)] by RLVECT_1:10
.= a * (L1 . x) by A7, PRVECT_3:18 ; :: thesis: verum

end;

then reconsider L1 = L1 as LinearOperator of F,[:E,F:] by A6, LOPBAN_1:def 5;
set K = 1;
for x being VECTOR of F holds ||.(L1 . x).|| <= 1 * ||.x.||

proof

let x be VECTOR of F; :: thesis: ||.(L1 . x).|| <= 1 * ||.x.||
L1 . x = [(0. E),x] by A3;
then ||.(L1 . x).|| <= ||.x.|| + ||.(0. E).|| by Th17;
then ||.(L1 . x).|| <= (1 * ||.x.||) + 0 by NORMSP_1:1;
hence ||.(L1 . x).|| <= 1 * ||.x.|| ; :: thesis: verum

end;

then L1 is Lipschitzian by LOPBAN_1:def 8;
hence ex L20 being Lipschitzian LinearOperator of F,[:E,F:] st
for dy being Point of F holds L20 . dy = [(0. E),dy] by A3; :: thesis: verum