let n be Nat; for A, B being RealNormSpace-Sequence
for X, Y being RealNormSpace st len A = n + 1 & A | n = B & X = A . (n + 1) holds
NestingLB (A,Y) = R_NormSpace_of_BoundedLinearOperators (X,(NestingLB (B,Y)))
let A, B be RealNormSpace-Sequence; for X, Y being RealNormSpace st len A = n + 1 & A | n = B & X = A . (n + 1) holds
NestingLB (A,Y) = R_NormSpace_of_BoundedLinearOperators (X,(NestingLB (B,Y)))
let X, Y be RealNormSpace; ( len A = n + 1 & A | n = B & X = A . (n + 1) implies NestingLB (A,Y) = R_NormSpace_of_BoundedLinearOperators (X,(NestingLB (B,Y))) )
assume A1:
( len A = n + 1 & A | n = B & X = A . (n + 1) )
; NestingLB (A,Y) = R_NormSpace_of_BoundedLinearOperators (X,(NestingLB (B,Y)))
consider f being Function such that
A2:
( dom f = NAT & NestingLB (A,Y) = f . (len A) & f . 0 = Y & ( for j being Nat st j < len A holds
ex V being RealNormSpace ex k being Element of dom A st
( V = f . j & j + 1 = k & f . (j + 1) = R_NormSpace_of_BoundedLinearOperators ((A . k),V) ) ) )
by Def3;
A3:
len B = n
by A1, FINSEQ_3:53;
then
len B < len A
by A1, NAT_1:13;
then consider V being RealNormSpace, k being Element of dom A such that
A4:
( V = f . (len B) & (len B) + 1 = k & f . ((len B) + 1) = R_NormSpace_of_BoundedLinearOperators ((A . k),V) )
by A2;
A5:
for j being Nat st j < len B holds
ex V being RealNormSpace ex k being Element of dom B st
( V = f . j & j + 1 = k & f . (j + 1) = R_NormSpace_of_BoundedLinearOperators ((B . k),V) )
proof
let j be
Nat;
( j < len B implies ex V being RealNormSpace ex k being Element of dom B st
( V = f . j & j + 1 = k & f . (j + 1) = R_NormSpace_of_BoundedLinearOperators ((B . k),V) ) )
assume A6:
j < len B
;
ex V being RealNormSpace ex k being Element of dom B st
( V = f . j & j + 1 = k & f . (j + 1) = R_NormSpace_of_BoundedLinearOperators ((B . k),V) )
then
j < len A
by A1, A3, NAT_1:13;
then consider V being
RealNormSpace,
k being
Element of
dom A such that A7:
(
V = f . j &
j + 1
= k &
f . (j + 1) = R_NormSpace_of_BoundedLinearOperators (
(A . k),
V) )
by A2;
A8:
j + 1
<= len B
by A6, NAT_1:13;
1
<= j + 1
by NAT_1:11;
then A9:
j + 1
in Seg (len B)
by A8;
then reconsider k1 =
j + 1 as
Element of
dom B by FINSEQ_1:def 3;
A . k = B . k1
by A1, A7, A9, FUNCT_1:49, A3;
hence
ex
V being
RealNormSpace ex
k being
Element of
dom B st
(
V = f . j &
j + 1
= k &
f . (j + 1) = R_NormSpace_of_BoundedLinearOperators (
(B . k),
V) )
by A7;
verum
end;
A10:
A . k = X
by A1, A4, FINSEQ_3:53;
thus NestingLB (A,Y) =
f . k
by A1, A2, A4, FINSEQ_3:53
.=
R_NormSpace_of_BoundedLinearOperators (X,(NestingLB (B,Y)))
by A2, A4, A5, A10, Def3
; verum