set SE = R_NormSpace_of_BoundedLinearOperators (S,E);
set SF = R_NormSpace_of_BoundedLinearOperators (S,F);
set SEF = R_NormSpace_of_BoundedLinearOperators (S,[:E,F:]);
defpred S1[ Element of (R_NormSpace_of_BoundedLinearOperators (S,E)), Element of (R_NormSpace_of_BoundedLinearOperators (S,F)), object ] means ex f being Lipschitzian LinearOperator of S,E ex g being Lipschitzian LinearOperator of S,F st
( $1 = f & $2 = g & $3 = <:f,g:> );
A1: for x being Element of [#] (R_NormSpace_of_BoundedLinearOperators (S,E))
for y being Element of [#] (R_NormSpace_of_BoundedLinearOperators (S,F)) ex z being Element of [#] (R_NormSpace_of_BoundedLinearOperators (S,[:E,F:])) st S1[x,y,z]
proof
let x be Element of [#] (R_NormSpace_of_BoundedLinearOperators (S,E)); :: thesis: for y being Element of [#] (R_NormSpace_of_BoundedLinearOperators (S,F)) ex z being Element of [#] (R_NormSpace_of_BoundedLinearOperators (S,[:E,F:])) st S1[x,y,z]
let y be Element of [#] (R_NormSpace_of_BoundedLinearOperators (S,F)); :: thesis: ex z being Element of [#] (R_NormSpace_of_BoundedLinearOperators (S,[:E,F:])) st S1[x,y,z]
reconsider L1 = x as Lipschitzian LinearOperator of S,E by LOPBAN_1:def 9;
reconsider L2 = y as Lipschitzian LinearOperator of S,F by LOPBAN_1:def 9;
set L = <:L1,L2:>;
A2: dom <:L1,L2:> = (dom L1) /\ (dom L2) by FUNCT_3:def 7
.= the carrier of S /\ (dom L2) by FUNCT_2:def 1
.= the carrier of S /\ the carrier of S by FUNCT_2:def 1
.= the carrier of S ;
reconsider L = <:L1,L2:> as Function of S,[:E,F:] ;
A3: ( L1 is additive & L2 is additive ) ;
for x, y being Element of S holds L . (x + y) = (L . x) + (L . y)
proof
let x, y be Element of S; :: thesis: L . (x + y) = (L . x) + (L . y)
A4: L . x = [(L1 . x),(L2 . x)] by A2, FUNCT_3:def 7;
A5: L . y = [(L1 . y),(L2 . y)] by A2, FUNCT_3:def 7;
thus L . (x + y) = [(L1 . (x + y)),(L2 . (x + y))] by A2, FUNCT_3:def 7
.= [((L1 . x) + (L1 . y)),(L2 . (x + y))] by A3
.= [((L1 . x) + (L1 . y)),((L2 . x) + (L2 . y))] by A3
.= (L . x) + (L . y) by A4, A5, PRVECT_3:18 ; :: thesis: verum
end;
then A6: L is additive ;
for x being VECTOR of S
for a being Real holds L . (a * x) = a * (L . x)
proof
let x be VECTOR of S; :: thesis: for a being Real holds L . (a * x) = a * (L . x)
let a be Real; :: thesis: L . (a * x) = a * (L . x)
A7: L . x = [(L1 . x),(L2 . x)] by A2, FUNCT_3:def 7;
thus L . (a * x) = [(L1 . (a * x)),(L2 . (a * x))] by A2, FUNCT_3:def 7
.= [(a * (L1 . x)),(L2 . (a * x))] by LOPBAN_1:def 5
.= [(a * (L1 . x)),(a * (L2 . x))] by LOPBAN_1:def 5
.= a * (L . x) by A7, PRVECT_3:18 ; :: thesis: verum
end;
then reconsider L = L as LinearOperator of S,[:E,F:] by A6, LOPBAN_1:def 5;
reconsider PL1 = L1 as Point of (R_NormSpace_of_BoundedLinearOperators (S,E)) ;
reconsider PL2 = L2 as Point of (R_NormSpace_of_BoundedLinearOperators (S,F)) ;
set K = ||.PL1.|| + ||.PL2.||;
( 0 <= ||.PL1.|| & 0 <= ||.PL2.|| ) by NORMSP_1:4;
then A8: 0 + 0 <= ||.PL1.|| + ||.PL2.|| by XREAL_1:7;
for x being VECTOR of S holds ||.(L . x).|| <= (||.PL1.|| + ||.PL2.||) * ||.x.||
proof
let x be VECTOR of S; :: thesis: ||.(L . x).|| <= (||.PL1.|| + ||.PL2.||) * ||.x.||
L . x = [(L1 . x),(L2 . x)] by FUNCT_3:def 7, A2;
then A9: ||.(L . x).|| <= ||.(L1 . x).|| + ||.(L2 . x).|| by Th17;
A10: ||.(L1 . x).|| <= ||.PL1.|| * ||.x.|| by LOPBAN_1:32;
||.(L2 . x).|| <= ||.PL2.|| * ||.x.|| by LOPBAN_1:32;
then ||.(L1 . x).|| + ||.(L2 . x).|| <= (||.PL1.|| * ||.x.||) + (||.PL2.|| * ||.x.||) by A10, XREAL_1:7;
hence ||.(L . x).|| <= (||.PL1.|| + ||.PL2.||) * ||.x.|| by A9, XXREAL_0:2; :: thesis: verum
end;
then L is Lipschitzian by A8, LOPBAN_1:def 8;
then reconsider L = L as Element of [#] (R_NormSpace_of_BoundedLinearOperators (S,[:E,F:])) by LOPBAN_1:def 9;
take L ; :: thesis: S1[x,y,L]
thus S1[x,y,L] ; :: thesis: verum
end;
consider G being Function of [:([#] (R_NormSpace_of_BoundedLinearOperators (S,E))),([#] (R_NormSpace_of_BoundedLinearOperators (S,F))):],([#] (R_NormSpace_of_BoundedLinearOperators (S,[:E,F:]))) such that
A11: for x being Element of [#] (R_NormSpace_of_BoundedLinearOperators (S,E))
for y being Element of [#] (R_NormSpace_of_BoundedLinearOperators (S,F)) holds S1[x,y,G . (x,y)] from BINOP_1:sch 3(A1);
 reconsider G = G as Function of [:(R_NormSpace_of_BoundedLinearOperators (S,E)),(R_NormSpace_of_BoundedLinearOperators (S,F)):],(R_NormSpace_of_BoundedLinearOperators (S,[:E,F:])) ;
A12: for f being Lipschitzian LinearOperator of S,E
for g being Lipschitzian LinearOperator of S,F holds G . (f,g) = <:f,g:>
proof
let f be Lipschitzian LinearOperator of S,E; :: thesis: for g being Lipschitzian LinearOperator of S,F holds G . (f,g) = <:f,g:>
let g be Lipschitzian LinearOperator of S,F; :: thesis: G . (f,g) = <:f,g:>
A13: f in [#] (R_NormSpace_of_BoundedLinearOperators (S,E)) by LOPBAN_1:def 9;
A14: g in [#] (R_NormSpace_of_BoundedLinearOperators (S,F)) by LOPBAN_1:def 9;
ex f1 being Lipschitzian LinearOperator of S,E ex g1 being Lipschitzian LinearOperator of S,F st
( f = f1 & g = g1 & G . (f,g) = <:f1,g1:> ) by A11, A13, A14;
hence G . (f,g) = <:f,g:> ; :: thesis: verum
end;
for x, y being Element of [:(R_NormSpace_of_BoundedLinearOperators (S,E)),(R_NormSpace_of_BoundedLinearOperators (S,F)):] holds G . (x + y) = (G . x) + (G . y)
proof
let x, y be Element of [:(R_NormSpace_of_BoundedLinearOperators (S,E)),(R_NormSpace_of_BoundedLinearOperators (S,F)):]; :: thesis: G . (x + y) = (G . x) + (G . y)
consider fx being Point of (R_NormSpace_of_BoundedLinearOperators (S,E)), gx being Point of (R_NormSpace_of_BoundedLinearOperators (S,F)) such that
A15: x = [fx,gx] by PRVECT_3:18;
consider fy being Point of (R_NormSpace_of_BoundedLinearOperators (S,E)), gy being Point of (R_NormSpace_of_BoundedLinearOperators (S,F)) such that
A16: y = [fy,gy] by PRVECT_3:18;
reconsider lfx = fx, lfy = fy as Lipschitzian LinearOperator of S,E by LOPBAN_1:def 9;
reconsider lgx = gx, lgy = gy as Lipschitzian LinearOperator of S,F by LOPBAN_1:def 9;
A17: G . x = G . (lfx,lgx) by A15, BINOP_1:def 1
.= <:lfx,lgx:> by A12 ;
A18: G . y = G . (lfy,lgy) by A16, BINOP_1:def 1
.= <:lfy,lgy:> by A12 ;
A19: fx + fy = lfx + lfy by Th11;
A20: gx + gy = lgx + lgy by Th11;
A21: lfx + lfy is Lipschitzian LinearOperator of S,E by A19, LOPBAN_1:def 9;
A22: lgx + lgy is Lipschitzian LinearOperator of S,F by A20, LOPBAN_1:def 9;
A23: G . (x + y) = G . [(fx + fy),(gx + gy)] by A15, A16, PRVECT_3:18
.= G . ((fx + fy),(gx + gy)) by BINOP_1:def 1
.= G . ((lfx + lfy),(lgx + lgy)) by A20, Th11
.= <:(lfx + lfy),(lgx + lgy):> by A12, A21, A22 ;
for s being VECTOR of S holds (G . (x + y)) . s = ((G . x) . s) + ((G . y) . s)
proof
let s be VECTOR of S; :: thesis: (G . (x + y)) . s = ((G . x) . s) + ((G . y) . s)
G . (x + y) is Lipschitzian LinearOperator of S,[:E,F:] by LOPBAN_1:def 9;
then dom (G . (x + y)) = [#] S by FUNCT_2:def 1;
then A24: (G . (x + y)) . s = [((lfx + lfy) . s),((lgx + lgy) . s)] by A23, FUNCT_3:def 7
.= [((fx + fy) . s),((gx + gy) . s)] by A20, Th11
.= [((fx . s) + (fy . s)),((gx + gy) . s)] by LOPBAN_1:35
.= [((fx . s) + (fy . s)),((gx . s) + (gy . s))] by LOPBAN_1:35 ;
G . x is Lipschitzian LinearOperator of S,[:E,F:] by LOPBAN_1:def 9;
then dom (G . x) = [#] S by FUNCT_2:def 1;
then A25: (G . x) . s = [(fx . s),(gx . s)] by A17, FUNCT_3:def 7;
G . y is Lipschitzian LinearOperator of S,[:E,F:] by LOPBAN_1:def 9;
then dom (G . y) = [#] S by FUNCT_2:def 1;
then (G . y) . s = [(fy . s),(gy . s)] by A18, FUNCT_3:def 7;
hence (G . (x + y)) . s = ((G . x) . s) + ((G . y) . s) by A24, A25, PRVECT_3:18; :: thesis: verum
end;
hence G . (x + y) = (G . x) + (G . y) by LOPBAN_1:35; :: thesis: verum
end;
then A26: G is additive ;
for x being VECTOR of [:(R_NormSpace_of_BoundedLinearOperators (S,E)),(R_NormSpace_of_BoundedLinearOperators (S,F)):]
for a being Real holds G . (a * x) = a * (G . x)
proof
let x be VECTOR of [:(R_NormSpace_of_BoundedLinearOperators (S,E)),(R_NormSpace_of_BoundedLinearOperators (S,F)):]; :: thesis: for a being Real holds G . (a * x) = a * (G . x)
let a be Real; :: thesis: G . (a * x) = a * (G . x)
consider fx being Point of (R_NormSpace_of_BoundedLinearOperators (S,E)), gx being Point of (R_NormSpace_of_BoundedLinearOperators (S,F)) such that
A27: x = [fx,gx] by PRVECT_3:18;
A28: a * x = [(a * fx),(a * gx)] by A27, PRVECT_3:18;
reconsider lfx = fx as Lipschitzian LinearOperator of S,E by LOPBAN_1:def 9;
reconsider lgx = gx as Lipschitzian LinearOperator of S,F by LOPBAN_1:def 9;
A29: a * fx = a (#) lfx by LOPBAN13:30;
A30: a * gx = a (#) lgx by LOPBAN13:30;
A31: G . x = G . (fx,gx) by A27, BINOP_1:def 1
.= <:lfx,lgx:> by A12 ;
A32: a (#) lfx is Lipschitzian LinearOperator of S,E by A29, LOPBAN_1:def 9;
A33: a (#) lgx is Lipschitzian LinearOperator of S,F by A30, LOPBAN_1:def 9;
A34: G . (a * x) = G . ((a * fx),(a * gx)) by A28, BINOP_1:def 1
.= <:(a (#) lfx),(a (#) lgx):> by A12, A29, A30, A32, A33 ;
for s being VECTOR of S holds (G . (a * x)) . s = a * ((G . x) . s)
proof
let s be VECTOR of S; :: thesis: (G . (a * x)) . s = a * ((G . x) . s)
G . (a * x) is Lipschitzian LinearOperator of S,[:E,F:] by LOPBAN_1:def 9;
then dom (G . (a * x)) = [#] S by FUNCT_2:def 1;
then A35: (G . (a * x)) . s = [((a (#) lfx) . s),((a (#) lgx) . s)] by A34, FUNCT_3:def 7
.= [((a * fx) . s),((a * gx) . s)] by A30, LOPBAN13:30
.= [(a * (fx . s)),((a * gx) . s)] by LOPBAN_1:36
.= [(a * (fx . s)),(a * (gx . s))] by LOPBAN_1:36 ;
G . x is Lipschitzian LinearOperator of S,[:E,F:] by LOPBAN_1:def 9;
then dom (G . x) = [#] S by FUNCT_2:def 1;
then A36: (G . x) . s = [(fx . s),(gx . s)] by A31, FUNCT_3:def 7;
thus (G . (a * x)) . s = a * ((G . x) . s) by A35, A36, PRVECT_3:18; :: thesis: verum
end;
hence G . (a * x) = a * (G . x) by LOPBAN_1:36; :: thesis: verum
end;
then reconsider G = G as LinearOperator of [:(R_NormSpace_of_BoundedLinearOperators (S,E)),(R_NormSpace_of_BoundedLinearOperators (S,F)):],(R_NormSpace_of_BoundedLinearOperators (S,[:E,F:])) by A26, LOPBAN_1:def 5;
set K = 2;
for x being VECTOR of [:(R_NormSpace_of_BoundedLinearOperators (S,E)),(R_NormSpace_of_BoundedLinearOperators (S,F)):] holds ||.(G . x).|| <= 2 * ||.x.||
proof
let x be VECTOR of [:(R_NormSpace_of_BoundedLinearOperators (S,E)),(R_NormSpace_of_BoundedLinearOperators (S,F)):]; :: thesis: ||.(G . x).|| <= 2 * ||.x.||
consider fx being Point of (R_NormSpace_of_BoundedLinearOperators (S,E)), gx being Point of (R_NormSpace_of_BoundedLinearOperators (S,F)) such that
A37: x = [fx,gx] by PRVECT_3:18;
A38: ( ||.fx.|| <= ||.x.|| & ||.gx.|| <= ||.x.|| ) by A37, NDIFF_8:21;
reconsider lfx = fx as Lipschitzian LinearOperator of S,E by LOPBAN_1:def 9;
reconsider lgx = gx as Lipschitzian LinearOperator of S,F by LOPBAN_1:def 9;
A39: G . x = G . (fx,gx) by A37, BINOP_1:def 1
.= <:lfx,lgx:> by A12 ;
A40: for s being VECTOR of S holds ||.((G . x) . s).|| <= (||.fx.|| + ||.gx.||) * ||.s.||
proof
let s be VECTOR of S; :: thesis: ||.((G . x) . s).|| <= (||.fx.|| + ||.gx.||) * ||.s.||
G . x is Lipschitzian LinearOperator of S,[:E,F:] by LOPBAN_1:def 9;
then dom (G . x) = [#] S by FUNCT_2:def 1;
then (G . x) . s = [(lfx . s),(lgx . s)] by A39, FUNCT_3:def 7;
then A41: ||.((G . x) . s).|| <= ||.(lfx . s).|| + ||.(lgx . s).|| by Th17;
A42: ||.(lfx . s).|| <= ||.fx.|| * ||.s.|| by LOPBAN_1:32;
||.(lgx . s).|| <= ||.gx.|| * ||.s.|| by LOPBAN_1:32;
then ||.(lfx . s).|| + ||.(lgx . s).|| <= (||.fx.|| * ||.s.||) + (||.gx.|| * ||.s.||) by A42, XREAL_1:7;
hence ||.((G . x) . s).|| <= (||.fx.|| + ||.gx.||) * ||.s.|| by A41, XXREAL_0:2; :: thesis: verum
end;
reconsider h1 = G . x as Lipschitzian LinearOperator of S,[:E,F:] by LOPBAN_1:def 9;
A43: now :: thesis: for r being Real st r in PreNorms h1 holds
r <= ||.fx.|| + ||.gx.||
let r be Real; :: thesis: ( r in PreNorms h1 implies r <= ||.fx.|| + ||.gx.|| )
assume r in PreNorms h1 ; :: thesis: r <= ||.fx.|| + ||.gx.||
then consider t being VECTOR of S such that
A44: ( r = ||.(h1 . t).|| & ||.t.|| <= 1 ) ;
A45: ||.(h1 . t).|| <= (||.fx.|| + ||.gx.||) * ||.t.|| by A40;
( 0 <= ||.fx.|| & 0 <= ||.gx.|| ) by NORMSP_1:4;
then 0 + 0 <= ||.fx.|| + ||.gx.|| by XREAL_1:7;
then (||.fx.|| + ||.gx.||) * ||.t.|| <= (||.fx.|| + ||.gx.||) * 1 by A44, XREAL_1:64;
hence r <= ||.fx.|| + ||.gx.|| by A44, A45, XXREAL_0:2; :: thesis: verum
end;
(BoundedLinearOperatorsNorm (S,[:E,F:])) . (G . x) = upper_bound (PreNorms h1) by LOPBAN_1:30;
then A46: ||.(G . x).|| <= ||.fx.|| + ||.gx.|| by A43, SEQ_4:45;
||.fx.|| + ||.gx.|| <= ||.x.|| + ||.x.|| by A38, XREAL_1:7;
hence ||.(G . x).|| <= 2 * ||.x.|| by A46, XXREAL_0:2; :: thesis: verum
end;
then reconsider G = G as Lipschitzian LinearOperator of [:(R_NormSpace_of_BoundedLinearOperators (S,E)),(R_NormSpace_of_BoundedLinearOperators (S,F)):],(R_NormSpace_of_BoundedLinearOperators (S,[:E,F:])) by LOPBAN_1:def 8;
take G ; :: thesis: for f being Lipschitzian LinearOperator of S,E
for g being Lipschitzian LinearOperator of S,F holds G . (f,g) = <:f,g:>
thus for f being Lipschitzian LinearOperator of S,E
for g being Lipschitzian LinearOperator of S,F holds G . (f,g) = <:f,g:> by A12; :: thesis: verum