let E, F be RealNormSpace; :: thesis: ex L10 being Lipschitzian LinearOperator of E,[:E,F:] st
for dx being Point of E holds L10 . dx = [dx,(0. F)]
defpred S₁[ object , object ] means ex dx being Point of E st
( dx = $1 & $2 = [dx,(0. F)] );
A1: for x being object st x in the carrier of E 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 E implies ex y being object st
( y in the carrier of [:E,F:] & S₁[x,y] ) )
assume x in the carrier of E ; :: thesis: ex y being object st
( y in the carrier of [:E,F:] & S₁[x,y] )
then reconsider V1 = x as Point of E ;
take y = [V1,(0. F)]; :: 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 E, the carrier of [:E,F:] such that
A2: for x being object st x in the carrier of E holds
S₁[x,L1 . x] from FUNCT_2:sch 1(A1);
A3: for dx being Point of E holds L1 . dx = [dx,(0. F)]

proof

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

end;

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

proof

let x, y be Element of E; :: thesis: L1 . (x + y) = (L1 . x) + (L1 . y)
A4: L1 . x = [x,(0. F)] by A3;
A5: L1 . y = [y,(0. F)] by A3;
thus L1 . (x + y) = [(x + y),(0. F)] by A3
.= [(x + y),((0. F) + (0. F))] 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 E
for a being Real holds L1 . (a * x) = a * (L1 . x)

proof

let x be VECTOR of E; :: 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 = [x,(0. F)] by A3;
thus L1 . (a * x) = [(a * x),(0. F)] by A3
.= [(a * x),(a * (0. F))] by RLVECT_1:10
.= a * (L1 . x) by A7, PRVECT_3:18 ; :: thesis: verum

end;

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

proof

let x be VECTOR of E; :: thesis: ||.(L1 . x).|| <= 1 * ||.x.||
L1 . x = [x,(0. F)] by A3;
then ||.(L1 . x).|| <= ||.x.|| + ||.(0. F).|| 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 L10 being Lipschitzian LinearOperator of E,[:E,F:] st
for dx being Point of E holds L10 . dx = [dx,(0. F)] by A3; :: thesis: verum