let X, Y, Z be RealNormSpace; :: thesis: for f, g being Point of (R_NormSpace_of_BoundedBilinearOperators (X,Y,Z))

for a being Real holds

( ( ||.f.|| = 0 implies f = 0. (R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)) ) & ( f = 0. (R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)) implies ||.f.|| = 0 ) & ||.(a * f).|| = |.a.| * ||.f.|| & ||.(f + g).|| <= ||.f.|| + ||.g.|| )

let f, g be Point of (R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)); :: thesis: for a being Real holds

( ( ||.f.|| = 0 implies f = 0. (R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)) ) & ( f = 0. (R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)) implies ||.f.|| = 0 ) & ||.(a * f).|| = |.a.| * ||.f.|| & ||.(f + g).|| <= ||.f.|| + ||.g.|| )

let a be Real; :: thesis: ( ( ||.f.|| = 0 implies f = 0. (R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)) ) & ( f = 0. (R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)) implies ||.f.|| = 0 ) & ||.(a * f).|| = |.a.| * ||.f.|| & ||.(f + g).|| <= ||.f.|| + ||.g.|| )

for a being Real holds

( ( ||.f.|| = 0 implies f = 0. (R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)) ) & ( f = 0. (R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)) implies ||.f.|| = 0 ) & ||.(a * f).|| = |.a.| * ||.f.|| & ||.(f + g).|| <= ||.f.|| + ||.g.|| )

let f, g be Point of (R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)); :: thesis: for a being Real holds

( ( ||.f.|| = 0 implies f = 0. (R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)) ) & ( f = 0. (R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)) implies ||.f.|| = 0 ) & ||.(a * f).|| = |.a.| * ||.f.|| & ||.(f + g).|| <= ||.f.|| + ||.g.|| )

let a be Real; :: thesis: ( ( ||.f.|| = 0 implies f = 0. (R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)) ) & ( f = 0. (R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)) implies ||.f.|| = 0 ) & ||.(a * f).|| = |.a.| * ||.f.|| & ||.(f + g).|| <= ||.f.|| + ||.g.|| )

A1: now :: thesis: ( f = 0. (R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)) implies ||.f.|| = 0 )

A9:
||.(f + g).|| <= ||.f.|| + ||.g.||
assume A2:
f = 0. (R_NormSpace_of_BoundedBilinearOperators (X,Y,Z))
; :: thesis: ||.f.|| = 0

thus ||.f.|| = 0 :: thesis: verum

end;thus ||.f.|| = 0 :: thesis: verum

proof

reconsider g = f as Lipschitzian BilinearOperator of X,Y,Z by Def9;

set z = the carrier of [:X,Y:] --> (0. Z);

reconsider z = the carrier of [:X,Y:] --> (0. Z) as Function of the carrier of [:X,Y:], the carrier of Z ;

consider r0 being object such that

A3: r0 in PreNorms g by XBOOLE_0:def 1;

reconsider r0 = r0 as Real by A3;

A4: ( ( for s being Real st s in PreNorms g holds

s <= 0 ) implies upper_bound (PreNorms g) <= 0 ) by SEQ_4:45;

A6: z = g by A2, Th31;

then upper_bound (PreNorms g) = 0 by A3, A4, A7, SEQ_4:def 1;

hence ||.f.|| = 0 by Th30; :: thesis: verum

end;set z = the carrier of [:X,Y:] --> (0. Z);

reconsider z = the carrier of [:X,Y:] --> (0. Z) as Function of the carrier of [:X,Y:], the carrier of Z ;

consider r0 being object such that

A3: r0 in PreNorms g by XBOOLE_0:def 1;

reconsider r0 = r0 as Real by A3;

A4: ( ( for s being Real st s in PreNorms g holds

s <= 0 ) implies upper_bound (PreNorms g) <= 0 ) by SEQ_4:45;

A6: z = g by A2, Th31;

A7: now :: thesis: for r being Real st r in PreNorms g holds

( 0 <= r & r <= 0 )

then
0 <= r0
by A3;( 0 <= r & r <= 0 )

let r be Real; :: thesis: ( r in PreNorms g implies ( 0 <= r & r <= 0 ) )

assume r in PreNorms g ; :: thesis: ( 0 <= r & r <= 0 )

then consider t being VECTOR of X, s being VECTOR of Y such that

A8: r = ||.(g . (t,s)).|| and

( ||.t.|| <= 1 & ||.s.|| <= 1 ) ;

[t,s] is Point of [:X,Y:] ;

then g . (t,s) = 0. Z by A6, FUNCOP_1:7;

hence ( 0 <= r & r <= 0 ) by A8; :: thesis: verum

end;assume r in PreNorms g ; :: thesis: ( 0 <= r & r <= 0 )

then consider t being VECTOR of X, s being VECTOR of Y such that

A8: r = ||.(g . (t,s)).|| and

( ||.t.|| <= 1 & ||.s.|| <= 1 ) ;

[t,s] is Point of [:X,Y:] ;

then g . (t,s) = 0. Z by A6, FUNCOP_1:7;

hence ( 0 <= r & r <= 0 ) by A8; :: thesis: verum

then upper_bound (PreNorms g) = 0 by A3, A4, A7, SEQ_4:def 1;

hence ||.f.|| = 0 by Th30; :: thesis: verum

proof

A20:
||.(a * f).|| = |.a.| * ||.f.||
reconsider f1 = f, g1 = g, h1 = f + g as Lipschitzian BilinearOperator of X,Y,Z by Def9;

A10: ( ( for s being Real st s in PreNorms h1 holds

s <= ||.f.|| + ||.g.|| ) implies upper_bound (PreNorms h1) <= ||.f.|| + ||.g.|| ) by SEQ_4:45;

end;A10: ( ( for s being Real st s in PreNorms h1 holds

s <= ||.f.|| + ||.g.|| ) implies upper_bound (PreNorms h1) <= ||.f.|| + ||.g.|| ) by SEQ_4:45;

A11: now :: thesis: for t being VECTOR of X

for s being VECTOR of Y st ||.t.|| <= 1 & ||.s.|| <= 1 holds

||.(h1 . (t,s)).|| <= ||.f.|| + ||.g.||

for s being VECTOR of Y st ||.t.|| <= 1 & ||.s.|| <= 1 holds

||.(h1 . (t,s)).|| <= ||.f.|| + ||.g.||

let t be VECTOR of X; :: thesis: for s being VECTOR of Y st ||.t.|| <= 1 & ||.s.|| <= 1 holds

||.(h1 . (t,s)).|| <= ||.f.|| + ||.g.||

let s be VECTOR of Y; :: thesis: ( ||.t.|| <= 1 & ||.s.|| <= 1 implies ||.(h1 . (t,s)).|| <= ||.f.|| + ||.g.|| )

assume A12: ( ||.t.|| <= 1 & ||.s.|| <= 1 ) ; :: thesis: ||.(h1 . (t,s)).|| <= ||.f.|| + ||.g.||

A13: ||.t.|| * ||.s.|| <= 1 * 1 by A12, XREAL_1:66;

0 <= ||.g.|| by Th33;

then A14: ||.g.|| * (||.t.|| * ||.s.||) <= ||.g.|| * 1 by A13, XREAL_1:64;

0 <= ||.f.|| by Th33;

then ||.f.|| * (||.t.|| * ||.s.||) <= ||.f.|| * 1 by A13, XREAL_1:64;

then A15: ((||.f.|| * ||.t.||) * ||.s.||) + ((||.g.|| * ||.t.||) * ||.s.||) <= (||.f.|| * 1) + (||.g.|| * 1) by A14, XREAL_1:7;

A16: ||.((f1 . (t,s)) + (g1 . (t,s))).|| <= ||.(f1 . (t,s)).|| + ||.(g1 . (t,s)).|| by NORMSP_1:def 1;

A17: ||.(g1 . (t,s)).|| <= (||.g.|| * ||.t.||) * ||.s.|| by Th32;

||.(f1 . (t,s)).|| <= (||.f.|| * ||.t.||) * ||.s.|| by Th32;

then ||.(f1 . (t,s)).|| + ||.(g1 . (t,s)).|| <= ((||.f.|| * ||.t.||) * ||.s.||) + ((||.g.|| * ||.t.||) * ||.s.||) by A17, XREAL_1:7;

then A18: ||.(f1 . (t,s)).|| + ||.(g1 . (t,s)).|| <= ||.f.|| + ||.g.|| by A15, XXREAL_0:2;

||.(h1 . (t,s)).|| = ||.((f1 . (t,s)) + (g1 . (t,s))).|| by Th35;

hence ||.(h1 . (t,s)).|| <= ||.f.|| + ||.g.|| by A16, A18, XXREAL_0:2; :: thesis: verum

end;||.(h1 . (t,s)).|| <= ||.f.|| + ||.g.||

let s be VECTOR of Y; :: thesis: ( ||.t.|| <= 1 & ||.s.|| <= 1 implies ||.(h1 . (t,s)).|| <= ||.f.|| + ||.g.|| )

assume A12: ( ||.t.|| <= 1 & ||.s.|| <= 1 ) ; :: thesis: ||.(h1 . (t,s)).|| <= ||.f.|| + ||.g.||

A13: ||.t.|| * ||.s.|| <= 1 * 1 by A12, XREAL_1:66;

0 <= ||.g.|| by Th33;

then A14: ||.g.|| * (||.t.|| * ||.s.||) <= ||.g.|| * 1 by A13, XREAL_1:64;

0 <= ||.f.|| by Th33;

then ||.f.|| * (||.t.|| * ||.s.||) <= ||.f.|| * 1 by A13, XREAL_1:64;

then A15: ((||.f.|| * ||.t.||) * ||.s.||) + ((||.g.|| * ||.t.||) * ||.s.||) <= (||.f.|| * 1) + (||.g.|| * 1) by A14, XREAL_1:7;

A16: ||.((f1 . (t,s)) + (g1 . (t,s))).|| <= ||.(f1 . (t,s)).|| + ||.(g1 . (t,s)).|| by NORMSP_1:def 1;

A17: ||.(g1 . (t,s)).|| <= (||.g.|| * ||.t.||) * ||.s.|| by Th32;

||.(f1 . (t,s)).|| <= (||.f.|| * ||.t.||) * ||.s.|| by Th32;

then ||.(f1 . (t,s)).|| + ||.(g1 . (t,s)).|| <= ((||.f.|| * ||.t.||) * ||.s.||) + ((||.g.|| * ||.t.||) * ||.s.||) by A17, XREAL_1:7;

then A18: ||.(f1 . (t,s)).|| + ||.(g1 . (t,s)).|| <= ||.f.|| + ||.g.|| by A15, XXREAL_0:2;

||.(h1 . (t,s)).|| = ||.((f1 . (t,s)) + (g1 . (t,s))).|| by Th35;

hence ||.(h1 . (t,s)).|| <= ||.f.|| + ||.g.|| by A16, A18, XXREAL_0:2; :: thesis: verum

now :: thesis: for r being Real st r in PreNorms h1 holds

r <= ||.f.|| + ||.g.||

hence
||.(f + g).|| <= ||.f.|| + ||.g.||
by A10, Th30; :: thesis: verumr <= ||.f.|| + ||.g.||

let r be Real; :: thesis: ( r in PreNorms h1 implies r <= ||.f.|| + ||.g.|| )

assume r in PreNorms h1 ; :: thesis: r <= ||.f.|| + ||.g.||

then ex t being VECTOR of X ex s being VECTOR of Y st

( r = ||.(h1 . (t,s)).|| & ||.t.|| <= 1 & ||.s.|| <= 1 ) ;

hence r <= ||.f.|| + ||.g.|| by A11; :: thesis: verum

end;assume r in PreNorms h1 ; :: thesis: r <= ||.f.|| + ||.g.||

then ex t being VECTOR of X ex s being VECTOR of Y st

( r = ||.(h1 . (t,s)).|| & ||.t.|| <= 1 & ||.s.|| <= 1 ) ;

hence r <= ||.f.|| + ||.g.|| by A11; :: thesis: verum

proof

reconsider f1 = f, h1 = a * f as Lipschitzian BilinearOperator of X,Y,Z by Def9;

A21: ( ( for s being Real st s in PreNorms h1 holds

s <= |.a.| * ||.f.|| ) implies upper_bound (PreNorms h1) <= |.a.| * ||.f.|| ) by SEQ_4:45;

hence ||.(a * f).|| = |.a.| * ||.f.|| by A29, XXREAL_0:1; :: thesis: verum

end;A21: ( ( for s being Real st s in PreNorms h1 holds

s <= |.a.| * ||.f.|| ) implies upper_bound (PreNorms h1) <= |.a.| * ||.f.|| ) by SEQ_4:45;

A22: now :: thesis: for t being VECTOR of X

for s being VECTOR of Y st ||.t.|| <= 1 & ||.s.|| <= 1 holds

||.(h1 . (t,s)).|| <= |.a.| * ||.f.||

for s being VECTOR of Y st ||.t.|| <= 1 & ||.s.|| <= 1 holds

||.(h1 . (t,s)).|| <= |.a.| * ||.f.||

A23:
0 <= ||.f.||
by Th33;

let t be VECTOR of X; :: thesis: for s being VECTOR of Y st ||.t.|| <= 1 & ||.s.|| <= 1 holds

||.(h1 . (t,s)).|| <= |.a.| * ||.f.||

let s be VECTOR of Y; :: thesis: ( ||.t.|| <= 1 & ||.s.|| <= 1 implies ||.(h1 . (t,s)).|| <= |.a.| * ||.f.|| )

assume ( ||.t.|| <= 1 & ||.s.|| <= 1 ) ; :: thesis: ||.(h1 . (t,s)).|| <= |.a.| * ||.f.||

then ||.t.|| * ||.s.|| <= 1 * 1 by XREAL_1:66;

then A24: ||.f.|| * (||.t.|| * ||.s.||) <= ||.f.|| * 1 by A23, XREAL_1:64;

||.(f1 . (t,s)).|| <= (||.f.|| * ||.t.||) * ||.s.|| by Th32;

then A25: ||.(f1 . (t,s)).|| <= ||.f.|| by A24, XXREAL_0:2;

A26: ||.(a * (f1 . (t,s))).|| = |.a.| * ||.(f1 . (t,s)).|| by NORMSP_1:def 1;

A27: 0 <= |.a.| by COMPLEX1:46;

||.(h1 . (t,s)).|| = ||.(a * (f1 . (t,s))).|| by Th36;

hence ||.(h1 . (t,s)).|| <= |.a.| * ||.f.|| by A25, A26, A27, XREAL_1:64; :: thesis: verum

end;let t be VECTOR of X; :: thesis: for s being VECTOR of Y st ||.t.|| <= 1 & ||.s.|| <= 1 holds

||.(h1 . (t,s)).|| <= |.a.| * ||.f.||

let s be VECTOR of Y; :: thesis: ( ||.t.|| <= 1 & ||.s.|| <= 1 implies ||.(h1 . (t,s)).|| <= |.a.| * ||.f.|| )

assume ( ||.t.|| <= 1 & ||.s.|| <= 1 ) ; :: thesis: ||.(h1 . (t,s)).|| <= |.a.| * ||.f.||

then ||.t.|| * ||.s.|| <= 1 * 1 by XREAL_1:66;

then A24: ||.f.|| * (||.t.|| * ||.s.||) <= ||.f.|| * 1 by A23, XREAL_1:64;

||.(f1 . (t,s)).|| <= (||.f.|| * ||.t.||) * ||.s.|| by Th32;

then A25: ||.(f1 . (t,s)).|| <= ||.f.|| by A24, XXREAL_0:2;

A26: ||.(a * (f1 . (t,s))).|| = |.a.| * ||.(f1 . (t,s)).|| by NORMSP_1:def 1;

A27: 0 <= |.a.| by COMPLEX1:46;

||.(h1 . (t,s)).|| = ||.(a * (f1 . (t,s))).|| by Th36;

hence ||.(h1 . (t,s)).|| <= |.a.| * ||.f.|| by A25, A26, A27, XREAL_1:64; :: thesis: verum

A28: now :: thesis: for r being Real st r in PreNorms h1 holds

r <= |.a.| * ||.f.||

r <= |.a.| * ||.f.||

let r be Real; :: thesis: ( r in PreNorms h1 implies r <= |.a.| * ||.f.|| )

assume r in PreNorms h1 ; :: thesis: r <= |.a.| * ||.f.||

then ex t being VECTOR of X ex s being VECTOR of Y st

( r = ||.(h1 . (t,s)).|| & ||.t.|| <= 1 & ||.s.|| <= 1 ) ;

hence r <= |.a.| * ||.f.|| by A22; :: thesis: verum

end;assume r in PreNorms h1 ; :: thesis: r <= |.a.| * ||.f.||

then ex t being VECTOR of X ex s being VECTOR of Y st

( r = ||.(h1 . (t,s)).|| & ||.t.|| <= 1 & ||.s.|| <= 1 ) ;

hence r <= |.a.| * ||.f.|| by A22; :: thesis: verum

A29: now :: thesis: ( ( a <> 0 & |.a.| * ||.f.|| <= ||.(a * f).|| ) or ( a = 0 & |.a.| * ||.f.|| = ||.(a * f).|| ) )end;

||.(a * f).|| <= |.a.| * ||.f.||
by A21, A28, Th30;per cases
( a <> 0 or a = 0 )
;

end;

case A30:
a <> 0
; :: thesis: |.a.| * ||.f.|| <= ||.(a * f).||

s <= (|.a.| ") * ||.(a * f).|| ) implies upper_bound (PreNorms f1) <= (|.a.| ") * ||.(a * f).|| ) by SEQ_4:45;

A40: 0 <= |.a.| by COMPLEX1:46;

||.f.|| <= (|.a.| ") * ||.(a * f).|| by A38, A39, Th30;

then |.a.| * ||.f.|| <= |.a.| * ((|.a.| ") * ||.(a * f).||) by A40, XREAL_1:64;

then A41: |.a.| * ||.f.|| <= (|.a.| * (|.a.| ")) * ||.(a * f).|| ;

|.a.| <> 0 by A30, COMPLEX1:47;

then |.a.| * ||.f.|| <= 1 * ||.(a * f).|| by A41, XCMPLX_0:def 7;

hence |.a.| * ||.f.|| <= ||.(a * f).|| ; :: thesis: verum

end;

A31: now :: thesis: for t being VECTOR of X

for s being VECTOR of Y st ||.t.|| <= 1 & ||.s.|| <= 1 holds

||.(f1 . (t,s)).|| <= (|.a.| ") * ||.(a * f).||

for s being VECTOR of Y st ||.t.|| <= 1 & ||.s.|| <= 1 holds

||.(f1 . (t,s)).|| <= (|.a.| ") * ||.(a * f).||

A32:
0 <= ||.(a * f).||
by Th33;

let t be VECTOR of X; :: thesis: for s being VECTOR of Y st ||.t.|| <= 1 & ||.s.|| <= 1 holds

||.(f1 . (t,s)).|| <= (|.a.| ") * ||.(a * f).||

let s be VECTOR of Y; :: thesis: ( ||.t.|| <= 1 & ||.s.|| <= 1 implies ||.(f1 . (t,s)).|| <= (|.a.| ") * ||.(a * f).|| )

assume ( ||.t.|| <= 1 & ||.s.|| <= 1 ) ; :: thesis: ||.(f1 . (t,s)).|| <= (|.a.| ") * ||.(a * f).||

then ||.t.|| * ||.s.|| <= 1 * 1 by XREAL_1:66;

then A33: ||.(a * f).|| * (||.t.|| * ||.s.||) <= ||.(a * f).|| * 1 by A32, XREAL_1:64;

||.(h1 . (t,s)).|| <= (||.(a * f).|| * ||.t.||) * ||.s.|| by Th32;

then A34: ||.(h1 . (t,s)).|| <= ||.(a * f).|| by A33, XXREAL_0:2;

h1 . (t,s) = a * (f1 . (t,s)) by Th36;

then A35: (a ") * (h1 . (t,s)) = ((a ") * a) * (f1 . (t,s)) by RLVECT_1:def 7

.= 1 * (f1 . (t,s)) by A30, XCMPLX_0:def 7

.= f1 . (t,s) by RLVECT_1:def 8 ;

A36: |.(a ").| = |.(1 * (a ")).|

.= |.(1 / a).| by XCMPLX_0:def 9

.= 1 / |.a.| by ABSVALUE:7

.= 1 * (|.a.| ") by XCMPLX_0:def 9

.= |.a.| " ;

A37: 0 <= |.(a ").| by COMPLEX1:46;

||.((a ") * (h1 . (t,s))).|| = |.(a ").| * ||.(h1 . (t,s)).|| by NORMSP_1:def 1;

hence ||.(f1 . (t,s)).|| <= (|.a.| ") * ||.(a * f).|| by A34, A35, A36, A37, XREAL_1:64; :: thesis: verum

end;let t be VECTOR of X; :: thesis: for s being VECTOR of Y st ||.t.|| <= 1 & ||.s.|| <= 1 holds

||.(f1 . (t,s)).|| <= (|.a.| ") * ||.(a * f).||

let s be VECTOR of Y; :: thesis: ( ||.t.|| <= 1 & ||.s.|| <= 1 implies ||.(f1 . (t,s)).|| <= (|.a.| ") * ||.(a * f).|| )

assume ( ||.t.|| <= 1 & ||.s.|| <= 1 ) ; :: thesis: ||.(f1 . (t,s)).|| <= (|.a.| ") * ||.(a * f).||

then ||.t.|| * ||.s.|| <= 1 * 1 by XREAL_1:66;

then A33: ||.(a * f).|| * (||.t.|| * ||.s.||) <= ||.(a * f).|| * 1 by A32, XREAL_1:64;

||.(h1 . (t,s)).|| <= (||.(a * f).|| * ||.t.||) * ||.s.|| by Th32;

then A34: ||.(h1 . (t,s)).|| <= ||.(a * f).|| by A33, XXREAL_0:2;

h1 . (t,s) = a * (f1 . (t,s)) by Th36;

then A35: (a ") * (h1 . (t,s)) = ((a ") * a) * (f1 . (t,s)) by RLVECT_1:def 7

.= 1 * (f1 . (t,s)) by A30, XCMPLX_0:def 7

.= f1 . (t,s) by RLVECT_1:def 8 ;

A36: |.(a ").| = |.(1 * (a ")).|

.= |.(1 / a).| by XCMPLX_0:def 9

.= 1 / |.a.| by ABSVALUE:7

.= 1 * (|.a.| ") by XCMPLX_0:def 9

.= |.a.| " ;

A37: 0 <= |.(a ").| by COMPLEX1:46;

||.((a ") * (h1 . (t,s))).|| = |.(a ").| * ||.(h1 . (t,s)).|| by NORMSP_1:def 1;

hence ||.(f1 . (t,s)).|| <= (|.a.| ") * ||.(a * f).|| by A34, A35, A36, A37, XREAL_1:64; :: thesis: verum

A38: now :: thesis: for r being Real st r in PreNorms f1 holds

r <= (|.a.| ") * ||.(a * f).||

A39:
( ( for s being Real st s in PreNorms f1 holds r <= (|.a.| ") * ||.(a * f).||

let r be Real; :: thesis: ( r in PreNorms f1 implies r <= (|.a.| ") * ||.(a * f).|| )

assume r in PreNorms f1 ; :: thesis: r <= (|.a.| ") * ||.(a * f).||

then ex t being VECTOR of X ex s being VECTOR of Y st

( r = ||.(f1 . (t,s)).|| & ||.t.|| <= 1 & ||.s.|| <= 1 ) ;

hence r <= (|.a.| ") * ||.(a * f).|| by A31; :: thesis: verum

end;assume r in PreNorms f1 ; :: thesis: r <= (|.a.| ") * ||.(a * f).||

then ex t being VECTOR of X ex s being VECTOR of Y st

( r = ||.(f1 . (t,s)).|| & ||.t.|| <= 1 & ||.s.|| <= 1 ) ;

hence r <= (|.a.| ") * ||.(a * f).|| by A31; :: thesis: verum

s <= (|.a.| ") * ||.(a * f).|| ) implies upper_bound (PreNorms f1) <= (|.a.| ") * ||.(a * f).|| ) by SEQ_4:45;

A40: 0 <= |.a.| by COMPLEX1:46;

||.f.|| <= (|.a.| ") * ||.(a * f).|| by A38, A39, Th30;

then |.a.| * ||.f.|| <= |.a.| * ((|.a.| ") * ||.(a * f).||) by A40, XREAL_1:64;

then A41: |.a.| * ||.f.|| <= (|.a.| * (|.a.| ")) * ||.(a * f).|| ;

|.a.| <> 0 by A30, COMPLEX1:47;

then |.a.| * ||.f.|| <= 1 * ||.(a * f).|| by A41, XCMPLX_0:def 7;

hence |.a.| * ||.f.|| <= ||.(a * f).|| ; :: thesis: verum

case A42:
a = 0
; :: thesis: |.a.| * ||.f.|| = ||.(a * f).||

reconsider fz = f as VECTOR of (R_VectorSpace_of_BoundedBilinearOperators (X,Y,Z)) ;

A43: a * f = a * fz

.= 0. (R_VectorSpace_of_BoundedBilinearOperators (X,Y,Z)) by A42, RLVECT_1:10

.= 0. (R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)) ;

thus |.a.| * ||.f.|| = 0 * ||.f.|| by A42, ABSVALUE:2

.= ||.(a * f).|| by A43, Th34 ; :: thesis: verum

end;A43: a * f = a * fz

.= 0. (R_VectorSpace_of_BoundedBilinearOperators (X,Y,Z)) by A42, RLVECT_1:10

.= 0. (R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)) ;

thus |.a.| * ||.f.|| = 0 * ||.f.|| by A42, ABSVALUE:2

.= ||.(a * f).|| by A43, Th34 ; :: thesis: verum

hence ||.(a * f).|| = |.a.| * ||.f.|| by A29, XXREAL_0:1; :: thesis: verum

now :: thesis: ( ||.f.|| = 0 implies f = 0. (R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)) )

hence
( ( ||.f.|| = 0 implies f = 0. (R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)) ) & ( f = 0. (R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)) implies ||.f.|| = 0 ) & ||.(a * f).|| = |.a.| * ||.f.|| & ||.(f + g).|| <= ||.f.|| + ||.g.|| )
by A1, A9, A20; :: thesis: verumreconsider g = f as Lipschitzian BilinearOperator of X,Y,Z by Def9;

set z = the carrier of [:X,Y:] --> (0. Z);

reconsider z = the carrier of [:X,Y:] --> (0. Z) as Function of the carrier of [:X,Y:], the carrier of Z ;

assume A44: ||.f.|| = 0 ; :: thesis: f = 0. (R_NormSpace_of_BoundedBilinearOperators (X,Y,Z))

hence f = 0. (R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)) by Th31; :: thesis: verum

end;set z = the carrier of [:X,Y:] --> (0. Z);

reconsider z = the carrier of [:X,Y:] --> (0. Z) as Function of the carrier of [:X,Y:], the carrier of Z ;

assume A44: ||.f.|| = 0 ; :: thesis: f = 0. (R_NormSpace_of_BoundedBilinearOperators (X,Y,Z))

now :: thesis: for t being VECTOR of X

for s being VECTOR of Y holds g . (t,s) = z . (t,s)

then
g = z
by BINOP_1:2;for s being VECTOR of Y holds g . (t,s) = z . (t,s)

let t be VECTOR of X; :: thesis: for s being VECTOR of Y holds g . (t,s) = z . (t,s)

let s be VECTOR of Y; :: thesis: g . (t,s) = z . (t,s)

A45: [t,s] is Point of [:X,Y:] ;

||.(g . (t,s)).|| <= (||.f.|| * ||.t.||) * ||.s.|| by Th32;

then ||.(g . (t,s)).|| = 0 by A44;

hence g . (t,s) = 0. Z by NORMSP_0:def 5

.= z . (t,s) by A45, FUNCOP_1:7 ;

:: thesis: verum

end;let s be VECTOR of Y; :: thesis: g . (t,s) = z . (t,s)

A45: [t,s] is Point of [:X,Y:] ;

||.(g . (t,s)).|| <= (||.f.|| * ||.t.||) * ||.s.|| by Th32;

then ||.(g . (t,s)).|| = 0 by A44;

hence g . (t,s) = 0. Z by NORMSP_0:def 5

.= z . (t,s) by A45, FUNCOP_1:7 ;

:: thesis: verum

hence f = 0. (R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)) by Th31; :: thesis: verum