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 )
A5: 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;
then reconsider L = LB as Element of BoundedLinearOperators S,T ;
reconsider L1 = LB1 as Element of BoundedLinearOperators S,T by A5;
assume that
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) = (LB . (x - x0)) + (R /. (x - x0)) ) and
A7: 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
N c= dom f and
A8: 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 A6;
consider R being REST of S,T such that
A9: for x being Point of S st x in N holds
(f /. x) - (f /. x0) = (LB . (x - x0)) + (R /. (x - x0)) by A8;
consider N1 being Neighbourhood of x0 such that
N1 c= dom f and
A10: 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 A7;
consider R1 being REST of S,T such that
A11: for x being Point of S st x in N1 holds
(f /. x) - (f /. x0) = (LB1 . (x - x0)) + (R1 /. (x - x0)) by A10;
A12: 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 A13: 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 A13, RLVECT_1:23 ;
:: thesis: verum

end;

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

consider N0 being Neighbourhood of x0 such that
A15: ( N0 c= N & N0 c= N1 ) by Th1;
consider g being Real such that
A16: 0 < g and
A17: { 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;
set n1 = n0 + 1;
A19: 0 <= n0 by NAT_1:2;
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 A16, XREAL_1:70;
then ||.z.|| < (n0 + 1) * g by A16, XCMPLX_1:88;
then A20: ||.z.|| / (n0 + 1) < g by A19, XREAL_1:85;
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 )
( n0 + 1 <= n + (n0 + 1) & 0 <= ||.z.|| ) by NAT_1:12, NORMSP_1:8;
then A22: ||.z.|| / (n + (n0 + 1)) <= ||.z.|| / (n0 + 1) by A19, XREAL_1:120;
0 <= n by NAT_1:2;
then 0 < 1 * ((n + (n0 + 1)) " ) by A19;
then A23: 0 < 1 / (n + (n0 + 1)) by XCMPLX_0:def 9;
hence r . n > 0 by A21; :: thesis: ((r . n) * z) + x0 in N0
||.((((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 A23, ABSVALUE:def 1
.= ||.z.|| / (n + (n0 + 1)) by XCMPLX_1:100 ;
then ||.((((r . n) * z) + x0) - x0).|| < g by A20, A22, 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 A21, NAT_1:2, SEQ_4:43; :: thesis: lim r = 0
thus lim r = 0 by A21, NAT_1:2, SEQ_4:44; :: thesis: verum

end;

then consider r being Real_Sequence such that
A24: for n being Element of NAT holds
( r . n = 1 / (n + (n0 + 1)) & r . n > 0 & ((r . n) * z) + x0 in N0 ) and
r is convergent and
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
A25: for n being Element of NAT holds s . n = H₁(n) from FUNCT_2:sch 4();

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 A25;
then ( r . n = 0 or z = 0. S ) by RLVECT_1:24;
hence contradiction by A14, A24; :: thesis: verum

end;

then A26: s is non-zero by Th7;

now

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

end;

then ( s is convergent & lim s = 0. S ) by A19, Th22, Th23;
then reconsider s = s as convergent_to_0 sequence of S by A26, Def4;

A27: 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 that
A28: x in N and
A29: x in N1 ; :: thesis: (L . (x - x0)) + (R /. (x - x0)) = (L1 . (x - x0)) + (R1 /. (x - x0))
(f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) by A9, A28;
hence (L . (x - x0)) + (R /. (x - x0)) = (L1 . (x - x0)) + (R1 /. (x - x0)) by A11, A29; :: thesis: verum

end;

now

R1 is total by Def5;
then dom R1 = the carrier of S by PARTFUN1:def 4;
then A30: rng s c= dom R1 ;
R is total by Def5;
then dom R = the carrier of S by PARTFUN1:def 4;
then A31: rng s c= dom R ;
let n be Nat; :: thesis: (L . z) - (L1 . z) = (||.z.|| * (((||.s.|| " ) (#) (R1 /* s)) - ((||.s.|| " ) (#) (R /* s)))) . n
set x = ((r . n) * z) + x0;
A32: (((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 ;
A33: n in NAT by ORDINAL1:def 13;
then A34: r . n <> 0 by A24;
s is non-zero by Def4;
then s . n <> 0. S by A33, Th7;
then A35: ||.(s . n).|| <> 0 by NORMSP_1:def 2;
A36: r . n > 0 by A24, A33;
||.(s . n).|| = ||.((r . n) * z).|| by A25, A33
.= (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 A34, 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 A35, XCMPLX_1:60
.= (r . n) " ;
then A37: ||.z.|| * ((||.s.|| . n) " ) = (r . n) " by A33, NORMSP_1:def 10;
((r . n) * z) + x0 in N0 by A24, A33;
then (L . ((r . n) * z)) + (R /. ((r . n) * z)) = (L1 . ((r . n) * z)) + (R1 /. ((r . n) * z)) by A27, A15, A32;
then A38: (((r . n) " ) * (L . ((r . n) * z))) + (((r . n) " ) * (R /. ((r . n) * z))) = ((r . n) " ) * ((L1 . ((r . n) * z)) + (R1 /. ((r . n) * z))) by RLVECT_1:def 9;
A39: ((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 A34, XCMPLX_1:60
.= L1 . z by RLVECT_1:def 9 ;
((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 A34, XCMPLX_1:60
.= L . z by RLVECT_1:def 9 ;
then A40: (L . z) + (((r . n) " ) * (R /. ((r . n) * z))) = (L1 . z) + (((r . n) " ) * (R1 /. ((r . n) * z))) by A38, A39, RLVECT_1:def 9;
A41: ((r . n) " ) * (R1 /. ((r . n) * z)) = ((r . n) " ) * (R1 /. (s . n)) by A25, A33
.= (||.z.|| * ((||.s.|| " ) . n)) * (R1 /. (s . n)) by A37, VALUED_1:10
.= ||.z.|| * (((||.s.|| " ) . n) * (R1 /. (s . n))) by RLVECT_1:def 9
.= ||.z.|| * (((||.s.|| " ) . n) * ((R1 /* s) . n)) by A33, A30, FUNCT_2:186
.= ||.z.|| * (((||.s.|| " ) (#) (R1 /* s)) . n) by A33, Def2 ;
((r . n) " ) * (R /. ((r . n) * z)) = ((r . n) " ) * (R /. (s . n)) by A25, A33
.= (||.z.|| * ((||.s.|| " ) . n)) * (R /. (s . n)) by A37, VALUED_1:10
.= ||.z.|| * (((||.s.|| " ) . n) * (R /. (s . n))) by RLVECT_1:def 9
.= ||.z.|| * (((||.s.|| " ) . n) * ((R /* s) . n)) by A33, A31, FUNCT_2:186
.= ||.z.|| * (((||.s.|| " ) (#) (R /* s)) . n) by A33, Def2 ;
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 A40, A41, 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 A33, NORMSP_1:def 6;
hence (L . z) - (L1 . z) = (||.z.|| * (((||.s.|| " ) (#) (R1 /* s)) - ((||.s.|| " ) (#) (R /* s)))) . n by A33, NORMSP_1:def 8; :: thesis: verum

end;

then ( ||.z.|| * (((||.s.|| " ) (#) (R1 /* s)) - ((||.s.|| " ) (#) (R /* s))) is constant & (||.z.|| * (((||.s.|| " ) (#) (R1 /* s)) - ((||.s.|| " ) (#) (R /* s)))) . 1 = (L . z) - (L1 . z) ) by VALUED_0:def 18;
then A42: lim (||.z.|| * (((||.s.|| " ) (#) (R1 /* s)) - ((||.s.|| " ) (#) (R /* s)))) = (L . z) - (L1 . z) by Th21;
A43: ( (||.s.|| " ) (#) (R /* s) is convergent & (||.s.|| " ) (#) (R1 /* s) is convergent ) by Def5;
( lim ((||.s.|| " ) (#) (R /* s)) = 0. T & lim ((||.s.|| " ) (#) (R1 /* s)) = 0. T ) by Def5;
then A44: lim (((||.s.|| " ) (#) (R1 /* s)) - ((||.s.|| " ) (#) (R /* s))) = (0. T) - (0. T) by A43, 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 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 A42, 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 A12, FUNCT_2:113
.= LB1 by LOPBAN_1:def 12 ; :: thesis: verum
thus verum ; :: thesis: verum