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 RestFunc 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 RestFunc 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 )
A2: 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 14;
then reconsider L = LB as Element of BoundedLinearOperators (S,T) ;
reconsider L1 = LB1 as Element of BoundedLinearOperators (S,T) by A2;
assume that
A3: ex N being Neighbourhood of x0 st
( N c= dom f & ex R being RestFunc 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
A4: ex N being Neighbourhood of x0 st
( N c= dom f & ex R being RestFunc 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
A5: ex R being RestFunc 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 A3;
consider R being RestFunc of S,T such that
A6: for x being Point of S st x in N holds
(f /. x) - (f /. x0) = (LB . (x - x0)) + (R /. (x - x0)) by A5;
consider N1 being Neighbourhood of x0 such that
N1 c= dom f and
A7: ex R being RestFunc 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 A4;
consider R1 being RestFunc of S,T such that
A8: for x being Point of S st x in N1 holds
(f /. x) - (f /. x0) = (LB1 . (x - x0)) + (R1 /. (x - x0)) by A7;
A9: 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 :: thesis: ( ( z = 0. S & (modetrans (L,S,T)) . z = (modetrans (L1,S,T)) . z ) or ( z <> 0. S & (modetrans (L,S,T)) . z = (modetrans (L1,S,T)) . z ) )

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

case A10: 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:10
.= 0 * ((modetrans (L,S,T)) . z) by LOPBAN_1:def 5
.= 0. T by RLVECT_1:10
.= 0 * ((modetrans (L1,S,T)) . z) by RLVECT_1:10
.= (modetrans (L1,S,T)) . (0 * z) by LOPBAN_1:def 5
.= (modetrans (L1,S,T)) . z by A10, RLVECT_1:10 ;
:: thesis: verum

end;

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

consider N0 being Neighbourhood of x0 such that
A12: ( N0 c= N & N0 c= N1 ) by Th1;
consider g being Real such that
A13: 0 < g and
A14: { y where y is Point of S : ||.(y - x0).|| < g } c= N0 by NFCONT_1:def 1;
consider n0 being Nat such that
A15: ||.z.|| / g < n0 by SEQ_4:3;
set n1 = n0 + 1;
n0 <= n0 + 1 by NAT_1:11;
then ||.z.|| / g < n0 + 1 by A15, XXREAL_0:2;
then (||.z.|| / g) * g < (n0 + 1) * g by A13, XREAL_1:68;
then ||.z.|| < (n0 + 1) * g by A13, XCMPLX_1:87;
then A16: ||.z.|| / (n0 + 1) < g by XREAL_1:83;
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₁( Nat) -> set = 1 / ($1 + (n0 + 1));
consider r being Real_Sequence such that
A17: for n being 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 A17; :: thesis: ( r . n > 0 & ((r . n) * z) + x0 in N0 )
( n0 + 1 <= n + (n0 + 1) & 0 <= ||.z.|| ) by NAT_1:12, NORMSP_1:4;
then A18: ||.z.|| / (n + (n0 + 1)) <= ||.z.|| / (n0 + 1) by XREAL_1:118;
0 < 1 * ((n + (n0 + 1)) ") ;
then 0 < 1 / (n + (n0 + 1)) by XCMPLX_0:def 9;
hence r . n > 0 by A17; :: thesis: ((r . n) * z) + x0 in N0
||.((((r . n) * z) + x0) - x0).|| = ||.(((r . n) * z) + (x0 - x0)).|| by RLVECT_1:def 3
.= ||.(((r . n) * z) + (0. S)).|| by RLVECT_1:15
.= ||.((r . n) * z).|| by RLVECT_1:4
.= ||.((1 / (n + (n0 + 1))) * z).|| by A17
.= |.(1 / (n + (n0 + 1))).| * ||.z.|| by NORMSP_1:def 1
.= (1 / (n + (n0 + 1))) * ||.z.|| by ABSVALUE:def 1
.= ||.z.|| / (n + (n0 + 1)) by XCMPLX_1:99 ;
then ||.((((r . n) * z) + x0) - x0).|| < g by A16, A18, 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 A14; :: thesis: verum

end;

thus ( r is convergent & lim r = 0 ) by A17, SEQ_4:31; :: thesis: verum

end;

then consider r being Real_Sequence such that
A19: 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
A20: for n being Element of NAT holds s . n = H₁(n) from FUNCT_2:sch 4();

now :: thesis: for n being Nat holds not s . n = 0. S

let n be Nat; :: thesis: not s . n = 0. S
A21: n in NAT by ORDINAL1:def 12;
assume s . n = 0. S ; :: thesis: contradiction
then (r . n) * z = 0. S by A20, A21;
then ( r . n = 0 or z = 0. S ) by RLVECT_1:11;
hence contradiction by A11, A19, A21; :: thesis: verum

end;

then A22: s is non-zero by Th7;

now :: thesis: for n being Nat holds s . n = (1 / (n + (n0 + 1))) * z

let n be Nat; :: thesis: s . n = (1 / (n + (n0 + 1))) * z
A23: n in NAT by ORDINAL1:def 12;
hence s . n = (r . n) * z by A20
.= (1 / (n + (n0 + 1))) * z by A19, A23 ;
:: thesis: verum

end;

then ( s is convergent & lim s = 0. S ) by Th19, Th20;
then reconsider s = s as 0. S -convergent sequence of S by Def4;

A24: now :: thesis: for x being Point of S st x in N & x in N1 holds
(L . (x - x0)) + (R /. (x - x0)) = (L1 . (x - x0)) + (R1 /. (x - x0))

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
A25: x in N and
A26: 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 A6, A25;
hence (L . (x - x0)) + (R /. (x - x0)) = (L1 . (x - x0)) + (R1 /. (x - x0)) by A8, A26; :: thesis: verum

end;

now :: thesis: for n being Nat holds (L . z) - (L1 . z) = (||.z.|| * (((||.s.|| ") (#) (R1 /* s)) - ((||.s.|| ") (#) (R /* s)))) . n

R1 is total by Def5;
then dom R1 = the carrier of S by PARTFUN1:def 2;
then A27: rng s c= dom R1 ;
R is total by Def5;
then dom R = the carrier of S by PARTFUN1:def 2;
then A28: 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;
A29: (((r . n) * z) + x0) - x0 = ((r . n) * z) + (x0 - x0) by RLVECT_1:def 3
.= ((r . n) * z) + (0. S) by RLVECT_1:15
.= (r . n) * z by RLVECT_1:4 ;
A30: n in NAT by ORDINAL1:def 12;
then A31: r . n <> 0 by A19;
s . n <> 0. S by A22, Th7;
then A32: ||.(s . n).|| <> 0 by NORMSP_0:def 5;
A33: r . n > 0 by A19, A30;
||.(s . n).|| = ||.((r . n) * z).|| by A20, A30
.= |.(r . n).| * ||.z.|| by NORMSP_1:def 1
.= (r . n) * ||.z.|| by A33, 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 A31, 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 A32, XCMPLX_1:60
.= (r . n) " ;
then A34: ||.z.|| * ((||.s.|| . n) ") = (r . n) " by NORMSP_0:def 4;
((r . n) * z) + x0 in N0 by A19, A30;
then (L . ((r . n) * z)) + (R /. ((r . n) * z)) = (L1 . ((r . n) * z)) + (R1 /. ((r . n) * z)) by A24, A12, A29;
then A35: (((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 5;
A36: ((r . n) ") * (L1 . ((r . n) * z)) = ((r . n) ") * ((modetrans (L1,S,T)) . ((r . n) * z)) by LOPBAN_1:def 11
.= ((r . n) ") * ((r . n) * ((modetrans (L1,S,T)) . z)) by LOPBAN_1:def 5
.= ((r . n) ") * ((r . n) * (L1 . z)) by LOPBAN_1:def 11
.= (((r . n) ") * (r . n)) * (L1 . z) by RLVECT_1:def 7
.= ((r . n) / (r . n)) * (L1 . z) by XCMPLX_0:def 9
.= 1 * (L1 . z) by A31, XCMPLX_1:60
.= L1 . z by RLVECT_1:def 8 ;
((r . n) ") * (L . ((r . n) * z)) = ((r . n) ") * ((modetrans (L,S,T)) . ((r . n) * z)) by LOPBAN_1:def 11
.= ((r . n) ") * ((r . n) * ((modetrans (L,S,T)) . z)) by LOPBAN_1:def 5
.= ((r . n) ") * ((r . n) * (L . z)) by LOPBAN_1:def 11
.= (((r . n) ") * (r . n)) * (L . z) by RLVECT_1:def 7
.= ((r . n) / (r . n)) * (L . z) by XCMPLX_0:def 9
.= 1 * (L . z) by A31, XCMPLX_1:60
.= L . z by RLVECT_1:def 8 ;
then A37: (L . z) + (((r . n) ") * (R /. ((r . n) * z))) = (L1 . z) + (((r . n) ") * (R1 /. ((r . n) * z))) by A35, A36, RLVECT_1:def 5;
A38: ((r . n) ") * (R1 /. ((r . n) * z)) = ((r . n) ") * (R1 /. (s . n)) by A20, A30
.= (||.z.|| * ((||.s.|| ") . n)) * (R1 /. (s . n)) by A34, VALUED_1:10
.= ||.z.|| * (((||.s.|| ") . n) * (R1 /. (s . n))) by RLVECT_1:def 7
.= ||.z.|| * (((||.s.|| ") . n) * ((R1 /* s) . n)) by A30, A27, FUNCT_2:109
.= ||.z.|| * (((||.s.|| ") (#) (R1 /* s)) . n) by Def2 ;
((r . n) ") * (R /. ((r . n) * z)) = ((r . n) ") * (R /. (s . n)) by A20, A30
.= (||.z.|| * ((||.s.|| ") . n)) * (R /. (s . n)) by A34, VALUED_1:10
.= ||.z.|| * (((||.s.|| ") . n) * (R /. (s . n))) by RLVECT_1:def 7
.= ||.z.|| * (((||.s.|| ") . n) * ((R /* s) . n)) by A30, A28, FUNCT_2:109
.= ||.z.|| * (((||.s.|| ") (#) (R /* s)) . n) by 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 A37, A38, RLVECT_1:def 3;
then (L . z) + (0. T) = ((L1 . z) + (||.z.|| * (((||.s.|| ") (#) (R1 /* s)) . n))) - (||.z.|| * (((||.s.|| ") (#) (R /* s)) . n)) by RLVECT_1:15;
then L . z = ((L1 . z) + (||.z.|| * (((||.s.|| ") (#) (R1 /* s)) . n))) - (||.z.|| * (((||.s.|| ") (#) (R /* s)) . n)) by RLVECT_1:def 4;
then (L . z) - (L1 . z) = (- (L1 . z)) + ((L1 . z) + ((||.z.|| * (((||.s.|| ") (#) (R1 /* s)) . n)) - (||.z.|| * (((||.s.|| ") (#) (R /* s)) . n)))) by RLVECT_1:def 3;
then (L . z) - (L1 . z) = ((- (L1 . z)) + (L1 . z)) + ((||.z.|| * (((||.s.|| ") (#) (R1 /* s)) . n)) - (||.z.|| * (((||.s.|| ") (#) (R /* s)) . n))) by RLVECT_1:def 3;
then (L . z) - (L1 . z) = (0. T) + ((||.z.|| * (((||.s.|| ") (#) (R1 /* s)) . n)) - (||.z.|| * (((||.s.|| ") (#) (R /* s)) . n))) by RLVECT_1:5;
then (L . z) - (L1 . z) = (||.z.|| * (((||.s.|| ") (#) (R1 /* s)) . n)) - (||.z.|| * (((||.s.|| ") (#) (R /* s)) . n)) by RLVECT_1:4;
then (L . z) - (L1 . z) = ||.z.|| * ((((||.s.|| ") (#) (R1 /* s)) . n) - (((||.s.|| ") (#) (R /* s)) . n)) by RLVECT_1:34;
then (L . z) - (L1 . z) = ||.z.|| * ((((||.s.|| ") (#) (R1 /* s)) - ((||.s.|| ") (#) (R /* s))) . n) by NORMSP_1:def 3;
hence (L . z) - (L1 . z) = (||.z.|| * (((||.s.|| ") (#) (R1 /* s)) - ((||.s.|| ") (#) (R /* s)))) . n by NORMSP_1:def 5; :: 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 A39: lim (||.z.|| * (((||.s.|| ") (#) (R1 /* s)) - ((||.s.|| ") (#) (R /* s)))) = (L . z) - (L1 . z) by Th18;
A40: ( (||.s.|| ") (#) (R /* s) is convergent & (||.s.|| ") (#) (R1 /* s) is convergent ) by A22, Def5;
( lim ((||.s.|| ") (#) (R /* s)) = 0. T & lim ((||.s.|| ") (#) (R1 /* s)) = 0. T ) by A22, Def5;
then A41: lim (((||.s.|| ") (#) (R1 /* s)) - ((||.s.|| ") (#) (R /* s))) = (0. T) - (0. T) by A40, NORMSP_1:26
.= 0. T by RLVECT_1:13 ;
A42: lim (||.z.|| * (((||.s.|| ") (#) (R1 /* s)) - ((||.s.|| ") (#) (R /* s)))) = ||.z.|| * (lim (((||.s.|| ") (#) (R1 /* s)) - ((||.s.|| ") (#) (R /* s)))) by A40, NORMSP_1:20, NORMSP_1:28
.= 0. T by A41, RLVECT_1:10 ;
thus (modetrans (L,S,T)) . z = L . z by LOPBAN_1:def 11
.= L1 . z by A39, A42, RLVECT_1:21
.= (modetrans (L1,S,T)) . z by LOPBAN_1:def 11 ; :: 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 11
.= modetrans (L1,S,T) by A9, FUNCT_2:63
.= LB1 by LOPBAN_1:def 11 ; :: thesis: verum