let E, F, G be RealNormSpace; :: thesis:
let LP be Point of (R_NormSpace_of_BoundedLinearOperators ([:E,F:],G)); :: thesis:
reconsider L = LP as Lipschitzian LinearOperator of [:E,F:],G by LOPBAN_1:def 9;
consider L1 being Lipschitzian LinearOperator of E,G, L2 being Lipschitzian LinearOperator of F,G such that
A1: for x being Point of E
for y being Point of F holds L . [x,y] = (L1 . x) + (L2 . y) and
A2: for x being Point of E holds L1 . x = L /. [x,(0. F)] and
A3: for y being Point of F holds L2 . y = L /. [(0. E),y] by Th2;
reconsider LP1 = L1 as Point of (R_NormSpace_of_BoundedLinearOperators (E,G)) by LOPBAN_1:def 9;
reconsider LP2 = L2 as Point of (R_NormSpace_of_BoundedLinearOperators (F,G)) by LOPBAN_1:def 9;
take LP1 ; :: thesis:
take LP2 ; :: thesis:
thus for x being Point of E
for y being Point of F holds LP . [x,y] = (LP1 . x) + (LP2 . y) by A1; :: thesis:
thus for x being Point of E holds LP1 . x = LP . [x,(0. F)] :: thesis:

let x be Point of E; :: thesis:
thus LP1 . x = L /. [x,(0. F)] by A2
.= LP . [x,(0. F)] ; :: thesis:

end;

thus for y being Point of F holds LP2 . y = LP . [(0. E),y] :: thesis:

let y be Point of F; :: thesis:
thus LP2 . y = L /. [(0. E),y] by A3
.= LP . [(0. E),y] ; :: thesis:

end;

end;

let t be Real; :: thesis:
assume t in PreNorms L1 ; :: thesis:
then consider x being Point of E such that
A18: ( t = ||.(L1 . x).|| & ||.x.|| <= 1 ) ;
reconsider w = [x,(0. F)] as Point of [:E,F:] ;
A19: ||.w.|| <= 1 by A18, NDIFF_8:2;
A20: L . w = (L1 . x) + (L2 . (0. F)) by A1
.= (L1 . x) + (0. G) by LOPBAN_7:3
.= L1 . x by RLVECT_1:def 4 ;
A21: ||.(L . w).|| <= ||.LP.|| * ||.w.|| by LOPBAN_1:32;
||.LP.|| * ||.w.|| <= ||.LP.|| * 1 by A19, XREAL_1:64;
hence t <= ||.LP.|| by A18, A20, A21, XXREAL_0:2; :: thesis:

end;

let t be Real; :: thesis:
assume t in PreNorms L2 ; :: thesis:
then consider x being Point of F such that
A24: ( t = ||.(L2 . x).|| & ||.x.|| <= 1 ) ;
reconsider w = [(0. E),x] as Point of [:E,F:] ;
A25: ||.x.|| = ||.w.|| by NDIFF_8:3;
A26: L . w = (L1 . (0. E)) + (L2 . x) by A1
.= (0. G) + (L2 . x) by LOPBAN_7:3
.= L2 . x by RLVECT_1:def 4 ;
A27: ||.(L . w).|| <= ||.LP.|| * ||.w.|| by LOPBAN_1:32;
||.LP.|| * ||.w.|| <= ||.LP.|| * 1 by A24, A25, XREAL_1:64;
hence t <= ||.LP.|| by A24, A26, A27, XXREAL_0:2; :: thesis:

end;