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

.= modetrans (L1,S,T) by A9, FUNCT_2:63

.= LB1 by LOPBAN_1:def 11 ; :: thesis: verum

( 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

thus LB =
modetrans (L,S,T)
by LOPBAN_1:def 11
let z be Point of S; :: thesis: (modetrans (L,S,T)) . z = (modetrans (L1,S,T)) . z

end;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 ) )end;

hence
(modetrans (L,S,T)) . z = (modetrans (L1,S,T)) . z
; :: thesis: verumper cases
( z = 0. S or z <> 0. S )
;

end;

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;.= 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

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 )

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_{1}( 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_{1}(n)
from FUNCT_2:sch 4();

then reconsider s = s as 0. S -convergent sequence of S by Def4;

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;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

then consider r being Real_Sequence such that
deffunc H_{1}( Nat) -> set = 1 / ($1 + (n0 + 1));

consider r being Real_Sequence such that

A17: for n being Nat holds r . n = H_{1}(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 )

end;consider r being Real_Sequence such that

A17: for n being Nat holds r . n = H

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

thus
( r is convergent & lim r = 0 )
by A17, SEQ_4:31; :: thesis: verum
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 . 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

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

consider s being sequence of S such that

A20: for n being Element of NAT holds s . n = H

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

then A22:
s is non-zero
by Th7;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;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

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

then
( s is convergent & lim s = 0. S )
by Th19, Th20;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;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

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))

(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;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

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

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;
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 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

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

.= modetrans (L1,S,T) by A9, FUNCT_2:63

.= LB1 by LOPBAN_1:def 11 ; :: thesis: verum