let LB, LB1 be Point of (R_NormSpace_of_BoundedLinearOperators S,T); :: thesis: ( ex N being Neighbourhood of x0 st
( N c= dom f & ex R being REST of S,T st
for x being Point of S st x in N holds
(f /. x) - (f /. x0) = (LB . (x - x0)) + (R /. (x - x0)) ) & ex N being Neighbourhood of x0 st
( N c= dom f & ex R being REST of S,T st
for x being Point of S st x in N holds
(f /. x) - (f /. x0) = (LB1 . (x - x0)) + (R /. (x - x0)) ) implies LB = LB1 )
A4: R_NormSpace_of_BoundedLinearOperators S,T = NORMSTR(# (BoundedLinearOperators S,T),(Zero_ (BoundedLinearOperators S,T),(R_VectorSpace_of_LinearOperators S,T)),(Add_ (BoundedLinearOperators S,T),(R_VectorSpace_of_LinearOperators S,T)),(Mult_ (BoundedLinearOperators S,T),(R_VectorSpace_of_LinearOperators S,T)),(BoundedLinearOperatorsNorm S,T) #) by LOPBAN_1:def 15;
assume that
A5: ex N being Neighbourhood of x0 st
( N c= dom f & ex R being REST of S,T st
for x being Point of S st x in N holds
(f /. x) - (f /. x0) = (LB . (x - x0)) + (R /. (x - x0)) ) and
A6: ex N being Neighbourhood of x0 st
( N c= dom f & ex R being REST of S,T st
for x being Point of S st x in N holds
(f /. x) - (f /. x0) = (LB1 . (x - x0)) + (R /. (x - x0)) ) ; :: thesis: LB = LB1
consider N being Neighbourhood of x0 such that
A7: ( N c= dom f & ex R being REST of S,T st
for x being Point of S st x in N holds
(f /. x) - (f /. x0) = (LB . (x - x0)) + (R /. (x - x0)) ) by A5;
consider R being REST of S,T such that
A8: for x being Point of S st x in N holds
(f /. x) - (f /. x0) = (LB . (x - x0)) + (R /. (x - x0)) by A7;
consider N1 being Neighbourhood of x0 such that
A9: ( N1 c= dom f & ex R being REST of S,T st
for x being Point of S st x in N1 holds
(f /. x) - (f /. x0) = (LB1 . (x - x0)) + (R /. (x - x0)) ) by A6;
consider R1 being REST of S,T such that
A10: for x being Point of S st x in N1 holds
(f /. x) - (f /. x0) = (LB1 . (x - x0)) + (R1 /. (x - x0)) by A9;
reconsider L = LB as Element of BoundedLinearOperators S,T by A4;
reconsider L1 = LB1 as Element of BoundedLinearOperators S,T by A4;
A11: for z being Point of S holds (modetrans L,S,T) . z = (modetrans L1,S,T) . z

proof

let z be Point of S; :: thesis: (modetrans L,S,T) . z = (modetrans L1,S,T) . z

now

per cases ( z = 0. S or z <> 0. S ) ;

case A12: z = 0. S ; :: thesis: (modetrans L,S,T) . z = (modetrans L1,S,T) . z

hence (modetrans L,S,T) . z = (modetrans L,S,T) . (0 * z) by RLVECT_1:23
.= 0 * ((modetrans L,S,T) . z) by LOPBAN_1:def 6
.= 0. T by RLVECT_1:23
.= 0 * ((modetrans L1,S,T) . z) by RLVECT_1:23
.= (modetrans L1,S,T) . (0 * z) by LOPBAN_1:def 6
.= (modetrans L1,S,T) . z by A12, RLVECT_1:23 ;
:: thesis: verum

end;

case A13: z <> 0. S ; :: thesis: (modetrans L,S,T) . z = (modetrans L1,S,T) . z

A14: now

let x be Point of S; :: thesis: ( x in N & x in N1 implies (L . (x - x0)) + (R /. (x - x0)) = (L1 . (x - x0)) + (R1 /. (x - x0)) )
assume A15: ( x in N & x in N1 ) ; :: thesis: (L . (x - x0)) + (R /. (x - x0)) = (L1 . (x - x0)) + (R1 /. (x - x0))
then (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) by A8;
hence (L . (x - x0)) + (R /. (x - x0)) = (L1 . (x - x0)) + (R1 /. (x - x0)) by A10, A15; :: thesis: verum

end;

consider N0 being Neighbourhood of x0 such that
A16: ( N0 c= N & N0 c= N1 ) by Th1;
consider g being Real such that
A17: ( 0 < g & { y where y is Point of S : ||.(y - x0).|| < g } c= N0 ) by NFCONT_1:def 3;
consider n0 being Element of NAT such that
A18: ||.z.|| / g < n0 by SEQ_4:10;
0 <= n0 by NAT_1:2;
then A19: 0 < n0 + 1 ;
n0 <= n0 + 1 by NAT_1:11;
then ||.z.|| / g < n0 + 1 by A18, XXREAL_0:2;
then (||.z.|| / g) * g < (n0 + 1) * g by A17, XREAL_1:70;
then ||.z.|| < (n0 + 1) * g by A17, XCMPLX_1:88;
then A20: ||.z.|| / (n0 + 1) < g by A19, XREAL_1:85;
set n1 = n0 + 1;
ex r being Real_Sequence st
( ( for n being Element of NAT holds
( r . n = 1 / (n + (n0 + 1)) & r . n > 0 & ((r . n) * z) + x0 in N0 ) ) & r is convergent & lim r = 0 )

proof

deffunc H₁( Element of NAT ) -> Element of REAL = 1 / ($1 + (n0 + 1));
consider r being Real_Sequence such that
A21: for n being Element of NAT holds r . n = H₁(n) from SEQ_1:sch 1();
take r ; :: thesis: ( ( for n being Element of NAT holds
( r . n = 1 / (n + (n0 + 1)) & r . n > 0 & ((r . n) * z) + x0 in N0 ) ) & r is convergent & lim r = 0 )
thus for n being Element of NAT holds
( r . n = 1 / (n + (n0 + 1)) & r . n > 0 & ((r . n) * z) + x0 in N0 ) :: thesis: ( r is convergent & lim r = 0 )

proof

let n be Element of NAT ; :: thesis: ( r . n = 1 / (n + (n0 + 1)) & r . n > 0 & ((r . n) * z) + x0 in N0 )
thus r . n = 1 / (n + (n0 + 1)) by A21; :: thesis: ( r . n > 0 & ((r . n) * z) + x0 in N0 )
0 <= n by NAT_1:2;
then 0 + 0 < (n0 + 1) + n by A19;
then 0 < 1 * ((n + (n0 + 1)) " ) ;
then A22: 0 < 1 / (n + (n0 + 1)) by XCMPLX_0:def 9;
hence r . n > 0 by A21; :: thesis: ((r . n) * z) + x0 in N0
A23: n0 + 1 <= n + (n0 + 1) by NAT_1:12;
0 <= ||.z.|| by NORMSP_1:8;
then A24: ||.z.|| / (n + (n0 + 1)) <= ||.z.|| / (n0 + 1) by A19, A23, XREAL_1:120;
||.((((r . n) * z) + x0) - x0).|| = ||.(((r . n) * z) + (x0 - x0)).|| by RLVECT_1:def 6
.= ||.(((r . n) * z) + (0. S)).|| by RLVECT_1:28
.= ||.((r . n) * z).|| by RLVECT_1:10
.= ||.((1 / (n + (n0 + 1))) * z).|| by A21
.= (abs (1 / (n + (n0 + 1)))) * ||.z.|| by NORMSP_1:def 2
.= (1 / (n + (n0 + 1))) * ||.z.|| by A22, ABSVALUE:def 1
.= ||.z.|| / (n + (n0 + 1)) by XCMPLX_1:100 ;
then ||.((((r . n) * z) + x0) - x0).|| < g by A20, A24, XXREAL_0:2;
then ((r . n) * z) + x0 in { y where y is Point of S : ||.(y - x0).|| < g } ;
hence ((r . n) * z) + x0 in N0 by A17; :: thesis: verum

end;

thus r is convergent by A19, A21, SEQ_4:43; :: thesis: lim r = 0
thus lim r = 0 by A19, A21, SEQ_4:44; :: thesis: verum

end;

then consider r being Real_Sequence such that
A25: ( ( for n being Element of NAT holds
( r . n = 1 / (n + (n0 + 1)) & r . n > 0 & ((r . n) * z) + x0 in N0 ) ) & r is convergent & lim r = 0 ) ;
deffunc H₁( Element of NAT ) -> Element of the carrier of S = (r . $1) * z;
consider s being sequence of S such that
A26: for n being Element of NAT holds s . n = H₁(n) from FUNCT_2:sch 4();
( s is non-zero & s is convergent & lim s = 0. S )

proof

now

let n be Element of NAT ; :: thesis: not s . n = 0. S
assume s . n = 0. S ; :: thesis: contradiction
then (r . n) * z = 0. S by A26;
then ( r . n = 0 or z = 0. S ) by RLVECT_1:24;
hence contradiction by A13, A25; :: thesis: verum

end;

hence s is non-zero by Th7; :: thesis: ( s is convergent & lim s = 0. S )

now

let n be Element of NAT ; :: thesis: s . n = (1 / (n + (n0 + 1))) * z
thus s . n = (r . n) * z by A26
.= (1 / (n + (n0 + 1))) * z by A25 ; :: thesis: verum

end;

hence ( s is convergent & lim s = 0. S ) by A19, Th22, Th23; :: thesis: verum

end;

then reconsider s = s as convergent_to_0 sequence of S by Def4;

A27: now

let n be Nat; :: thesis: (L . z) - (L1 . z) = (||.z.|| * (((||.s.|| " ) (#) (R1 /* s)) - ((||.s.|| " ) (#) (R /* s)))) . n
set x = ((r . n) * z) + x0;
A28: (((r . n) * z) + x0) - x0 = ((r . n) * z) + (x0 - x0) by RLVECT_1:def 6
.= ((r . n) * z) + (0. S) by RLVECT_1:28
.= (r . n) * z by RLVECT_1:10 ;
X: n in NAT by ORDINAL1:def 13;
then ((r . n) * z) + x0 in N0 by A25;
then A29: (L . ((r . n) * z)) + (R /. ((r . n) * z)) = (L1 . ((r . n) * z)) + (R1 /. ((r . n) * z)) by A14, A16, A28;
A30: r . n <> 0 by A25, X;
A31: (((r . n) " ) * (L . ((r . n) * z))) + (((r . n) " ) * (R /. ((r . n) * z))) = ((r . n) " ) * ((L1 . ((r . n) * z)) + (R1 /. ((r . n) * z))) by A29, RLVECT_1:def 9;
A32: ((r . n) " ) * (L . ((r . n) * z)) = ((r . n) " ) * ((modetrans L,S,T) . ((r . n) * z)) by LOPBAN_1:def 12
.= ((r . n) " ) * ((r . n) * ((modetrans L,S,T) . z)) by LOPBAN_1:def 6
.= ((r . n) " ) * ((r . n) * (L . z)) by LOPBAN_1:def 12
.= (((r . n) " ) * (r . n)) * (L . z) by RLVECT_1:def 9
.= ((r . n) / (r . n)) * (L . z) by XCMPLX_0:def 9
.= 1 * (L . z) by A30, XCMPLX_1:60
.= L . z by RLVECT_1:def 9 ;
((r . n) " ) * (L1 . ((r . n) * z)) = ((r . n) " ) * ((modetrans L1,S,T) . ((r . n) * z)) by LOPBAN_1:def 12
.= ((r . n) " ) * ((r . n) * ((modetrans L1,S,T) . z)) by LOPBAN_1:def 6
.= ((r . n) " ) * ((r . n) * (L1 . z)) by LOPBAN_1:def 12
.= (((r . n) " ) * (r . n)) * (L1 . z) by RLVECT_1:def 9
.= ((r . n) / (r . n)) * (L1 . z) by XCMPLX_0:def 9
.= 1 * (L1 . z) by A30, XCMPLX_1:60
.= L1 . z by RLVECT_1:def 9 ;
then A33: (L . z) + (((r . n) " ) * (R /. ((r . n) * z))) = (L1 . z) + (((r . n) " ) * (R1 /. ((r . n) * z))) by A31, A32, RLVECT_1:def 9;
R is total by Def5;
then dom R = the carrier of S by PARTFUN1:def 4;
then A34: rng s c= dom R ;
R1 is total by Def5;
then dom R1 = the carrier of S by PARTFUN1:def 4;
then A35: rng s c= dom R1 ;
A36: r . n > 0 by A25, X;
s is non-zero by Def4;
then s . n <> 0. S by Th7, X;
then A37: ||.(s . n).|| <> 0 by NORMSP_1:def 2;
||.(s . n).|| = ||.((r . n) * z).|| by A26, X
.= (abs (r . n)) * ||.z.|| by NORMSP_1:def 2
.= (r . n) * ||.z.|| by A36, ABSVALUE:def 1 ;
then ((r . n) " ) * ||.(s . n).|| = (((r . n) " ) * (r . n)) * ||.z.||
.= ((r . n) / (r . n)) * ||.z.|| by XCMPLX_0:def 9
.= 1 * ||.z.|| by A30, XCMPLX_1:60
.= ||.z.|| ;
then ||.z.|| * (||.(s . n).|| " ) = ((r . n) " ) * (||.(s . n).|| * (||.(s . n).|| " ))
.= ((r . n) " ) * (||.(s . n).|| / ||.(s . n).||) by XCMPLX_0:def 9
.= ((r . n) " ) * 1 by A37, XCMPLX_1:60
.= (r . n) " ;
then A38: ||.z.|| * ((||.s.|| . n) " ) = (r . n) " by X, NORMSP_1:def 10;
A39: ((r . n) " ) * (R /. ((r . n) * z)) = ((r . n) " ) * (R /. (s . n)) by A26, X
.= (||.z.|| * ((||.s.|| " ) . n)) * (R /. (s . n)) by A38, VALUED_1:10
.= ||.z.|| * (((||.s.|| " ) . n) * (R /. (s . n))) by RLVECT_1:def 9
.= ||.z.|| * (((||.s.|| " ) . n) * ((R /* s) . n)) by A34, X, FUNCT_2:186
.= ||.z.|| * (((||.s.|| " ) (#) (R /* s)) . n) by Def2, X ;
((r . n) " ) * (R1 /. ((r . n) * z)) = ((r . n) " ) * (R1 /. (s . n)) by A26, X
.= (||.z.|| * ((||.s.|| " ) . n)) * (R1 /. (s . n)) by A38, VALUED_1:10
.= ||.z.|| * (((||.s.|| " ) . n) * (R1 /. (s . n))) by RLVECT_1:def 9
.= ||.z.|| * (((||.s.|| " ) . n) * ((R1 /* s) . n)) by A35, X, FUNCT_2:186
.= ||.z.|| * (((||.s.|| " ) (#) (R1 /* s)) . n) by Def2, X ;
then (L . z) + ((||.z.|| * (((||.s.|| " ) (#) (R /* s)) . n)) - (||.z.|| * (((||.s.|| " ) (#) (R /* s)) . n))) = ((L1 . z) + (||.z.|| * (((||.s.|| " ) (#) (R1 /* s)) . n))) - (||.z.|| * (((||.s.|| " ) (#) (R /* s)) . n)) by A33, A39, RLVECT_1:def 6;
then (L . z) + (0. T) = ((L1 . z) + (||.z.|| * (((||.s.|| " ) (#) (R1 /* s)) . n))) - (||.z.|| * (((||.s.|| " ) (#) (R /* s)) . n)) by RLVECT_1:28;
then L . z = ((L1 . z) + (||.z.|| * (((||.s.|| " ) (#) (R1 /* s)) . n))) - (||.z.|| * (((||.s.|| " ) (#) (R /* s)) . n)) by RLVECT_1:def 7;
then (L . z) - (L1 . z) = (- (L1 . z)) + ((L1 . z) + ((||.z.|| * (((||.s.|| " ) (#) (R1 /* s)) . n)) - (||.z.|| * (((||.s.|| " ) (#) (R /* s)) . n)))) by RLVECT_1:def 6;
then (L . z) - (L1 . z) = ((- (L1 . z)) + (L1 . z)) + ((||.z.|| * (((||.s.|| " ) (#) (R1 /* s)) . n)) - (||.z.|| * (((||.s.|| " ) (#) (R /* s)) . n))) by RLVECT_1:def 6;
then (L . z) - (L1 . z) = (0. T) + ((||.z.|| * (((||.s.|| " ) (#) (R1 /* s)) . n)) - (||.z.|| * (((||.s.|| " ) (#) (R /* s)) . n))) by RLVECT_1:16;
then (L . z) - (L1 . z) = (||.z.|| * (((||.s.|| " ) (#) (R1 /* s)) . n)) - (||.z.|| * (((||.s.|| " ) (#) (R /* s)) . n)) by RLVECT_1:10;
then (L . z) - (L1 . z) = ||.z.|| * ((((||.s.|| " ) (#) (R1 /* s)) . n) - (((||.s.|| " ) (#) (R /* s)) . n)) by RLVECT_1:48;
then (L . z) - (L1 . z) = ||.z.|| * ((((||.s.|| " ) (#) (R1 /* s)) - ((||.s.|| " ) (#) (R /* s))) . n) by X, NORMSP_1:def 6;
hence (L . z) - (L1 . z) = (||.z.|| * (((||.s.|| " ) (#) (R1 /* s)) - ((||.s.|| " ) (#) (R /* s)))) . n by X, NORMSP_1:def 8; :: thesis: verum

end;

then A40: ||.z.|| * (((||.s.|| " ) (#) (R1 /* s)) - ((||.s.|| " ) (#) (R /* s))) is constant by VALUED_0:def 18;
(||.z.|| * (((||.s.|| " ) (#) (R1 /* s)) - ((||.s.|| " ) (#) (R /* s)))) . 1 = (L . z) - (L1 . z) by A27;
then A41: lim (||.z.|| * (((||.s.|| " ) (#) (R1 /* s)) - ((||.s.|| " ) (#) (R /* s)))) = (L . z) - (L1 . z) by A40, Th21;
A42: ( (||.s.|| " ) (#) (R /* s) is convergent & lim ((||.s.|| " ) (#) (R /* s)) = 0. T ) by Def5;
A43: ( (||.s.|| " ) (#) (R1 /* s) is convergent & lim ((||.s.|| " ) (#) (R1 /* s)) = 0. T ) by Def5;
then A44: lim (((||.s.|| " ) (#) (R1 /* s)) - ((||.s.|| " ) (#) (R /* s))) = (0. T) - (0. T) by A42, NORMSP_1:43
.= 0. T by RLVECT_1:26 ;
A45: lim (||.z.|| * (((||.s.|| " ) (#) (R1 /* s)) - ((||.s.|| " ) (#) (R /* s)))) = ||.z.|| * (lim (((||.s.|| " ) (#) (R1 /* s)) - ((||.s.|| " ) (#) (R /* s)))) by A42, A43, NORMSP_1:35, NORMSP_1:45
.= 0. T by A44, RLVECT_1:23 ;
thus (modetrans L,S,T) . z = L . z by LOPBAN_1:def 12
.= L1 . z by A41, A45, RLVECT_1:35
.= (modetrans L1,S,T) . z by LOPBAN_1:def 12 ; :: thesis: verum

end;

end;

end;

hence (modetrans L,S,T) . z = (modetrans L1,S,T) . z ; :: thesis: verum

end;

thus LB = modetrans L,S,T by LOPBAN_1:def 12
.= modetrans L1,S,T by A11, FUNCT_2:113
.= LB1 by LOPBAN_1:def 12 ; :: thesis: verum
thus verum ; :: thesis: verum