let LB, LB1 be Point of ; :: 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(# (),(Zero_ ((),())),(Add_ ((),())),(Mult_ ((),())),() #) 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 ;
:: 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 ;
then (||.z.|| / g) * g < (n0 + 1) * g by ;
then ||.z.|| < (n0 + 1) * g by ;
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 H1( Nat) -> set = 1 / (\$1 + (n0 + 1));
consider r being Real_Sequence such that
A17: for n being Nat holds r . n = H1(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 <= ) by ;
then A18: ||.z.|| / (n + (n0 + 1)) <= / (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))).| * by NORMSP_1:def 1
.= (1 / (n + (n0 + 1))) * by ABSVALUE:def 1
.= / (n + (n0 + 1)) by XCMPLX_1:99 ;
then ||.((((r . n) * z) + x0) - x0).|| < g by ;
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 ; :: 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 H1( 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 = H1(n) from
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 ;
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 ;
:: thesis: verum
end;
then ( s is convergent & lim s = 0. S ) by ;
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 ;
hence (L . (x - x0)) + (R /. (x - x0)) = (L1 . (x - x0)) + (R1 /. (x - x0)) by ; :: thesis: verum
end;
now :: thesis: for n being Nat holds (L . z) - (L1 . z) = ( * ((() (#) (R1 /* 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) = ( * ((() (#) (R1 /* 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 ;
then A32: ||.(s . n).|| <> 0 by NORMSP_0:def 5;
A33: r . n > 0 by ;
||.(s . n).|| = ||.((r . n) * z).|| by
.= |.(r . n).| * by NORMSP_1:def 1
.= (r . n) * by ;
then ((r . n) ") * ||.(s . n).|| = (((r . n) ") * (r . n)) *
.= ((r . n) / (r . n)) * by XCMPLX_0:def 9
.= 1 * by
.= ;
then * (||.(s . n).|| ") = ((r . n) ") * (||.(s . n).|| * (||.(s . n).|| "))
.= ((r . n) ") * (||.(s . n).|| / ||.(s . n).||) by XCMPLX_0:def 9
.= ((r . n) ") * 1 by
.= (r . n) " ;
then A34: ||.z.|| * (( . n) ") = (r . n) " by NORMSP_0:def 4;
((r . n) * z) + x0 in N0 by ;
then (L . ((r . n) * z)) + (R /. ((r . n) * z)) = (L1 . ((r . n) * z)) + (R1 /. ((r . n) * z)) by ;
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
.= 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
.= 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 ;
A38: ((r . n) ") * (R1 /. ((r . n) * z)) = ((r . n) ") * (R1 /. (s . n)) by
.= ( * (() . n)) * (R1 /. (s . n)) by
.= * ((() . n) * (R1 /. (s . n))) by RLVECT_1:def 7
.= * ((() . n) * ((R1 /* s) . n)) by
.= * ((() (#) (R1 /* s)) . n) by Def2 ;
((r . n) ") * (R /. ((r . n) * z)) = ((r . n) ") * (R /. (s . n)) by
.= ( * (() . n)) * (R /. (s . n)) by
.= * ((() . n) * (R /. (s . n))) by RLVECT_1:def 7
.= * ((() . n) * ((R /* s) . n)) by
.= * ((() (#) (R /* s)) . n) by Def2 ;
then (L . z) + (( * ((() (#) (R /* s)) . n)) - ( * ((() (#) (R /* s)) . n))) = ((L1 . z) + ( * ((() (#) (R1 /* s)) . n))) - ( * ((() (#) (R /* s)) . n)) by ;
then (L . z) + (0. T) = ((L1 . z) + ( * ((() (#) (R1 /* s)) . n))) - ( * ((() (#) (R /* s)) . n)) by RLVECT_1:15;
then L . z = ((L1 . z) + ( * ((() (#) (R1 /* s)) . n))) - ( * ((() (#) (R /* s)) . n)) by RLVECT_1:def 4;
then (L . z) - (L1 . z) = (- (L1 . z)) + ((L1 . z) + (( * ((() (#) (R1 /* s)) . n)) - ( * ((() (#) (R /* s)) . n)))) by RLVECT_1:def 3;
then (L . z) - (L1 . z) = ((- (L1 . z)) + (L1 . z)) + (( * ((() (#) (R1 /* s)) . n)) - ( * ((() (#) (R /* s)) . n))) by RLVECT_1:def 3;
then (L . z) - (L1 . z) = (0. T) + (( * ((() (#) (R1 /* s)) . n)) - ( * ((() (#) (R /* s)) . n))) by RLVECT_1:5;
then (L . z) - (L1 . z) = ( * ((() (#) (R1 /* s)) . n)) - ( * ((() (#) (R /* s)) . n)) by RLVECT_1:4;
then (L . z) - (L1 . z) = * (((() (#) (R1 /* s)) . n) - ((() (#) (R /* s)) . n)) by RLVECT_1:34;
then (L . z) - (L1 . z) = * (((() (#) (R1 /* s)) - (() (#) (R /* s))) . n) by NORMSP_1:def 3;
hence (L . z) - (L1 . z) = ( * ((() (#) (R1 /* s)) - (() (#) (R /* s)))) . n by NORMSP_1:def 5; :: thesis: verum
end;
then ( ||.z.|| * ((() (#) (R1 /* s)) - (() (#) (R /* s))) is constant & ( * ((() (#) (R1 /* s)) - (() (#) (R /* s)))) . 1 = (L . z) - (L1 . z) ) by VALUED_0:def 18;
then A39: lim ( * ((() (#) (R1 /* s)) - (() (#) (R /* s)))) = (L . z) - (L1 . z) by Th18;
A40: ( (||.s.|| ") (#) (R /* s) is convergent & () (#) (R1 /* s) is convergent ) by ;
( lim (() (#) (R /* s)) = 0. T & lim (() (#) (R1 /* s)) = 0. T ) by ;
then A41: lim ((() (#) (R1 /* s)) - (() (#) (R /* s))) = (0. T) - (0. T) by
.= 0. T by RLVECT_1:13 ;
A42: lim ( * ((() (#) (R1 /* s)) - (() (#) (R /* s)))) = * (lim ((() (#) (R1 /* s)) - (() (#) (R /* s)))) by
.= 0. T by ;
thus (modetrans (L,S,T)) . z = L . z by LOPBAN_1:def 11
.= L1 . z by
.= (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
.= LB1 by LOPBAN_1:def 11 ; :: thesis: verum