reconsider x = len q as Element of D by A2;
reconsider r = 0 as Element of D by A2;
reconsider q5 = ((n -' (len q)) -' 1) --> r as XFinSequence of D ;
<%x%> ^ (FS2XFS q) <> {}
by Th27;
then reconsider p0 = (<%x%> ^ (FS2XFS q)) ^ q5 as non empty XFinSequence of D by Th27;
A3:
0 in dom <%x%>
by Lm1;
A4:
len <%x%> = 1
by Def4;
0 in Segm ((len <%x%>) + (len (FS2XFS q)))
by NAT_1:44;
then
0 in len (<%x%> ^ (FS2XFS q))
by Def3;
then A5: p0 . 0 =
(<%x%> ^ (FS2XFS q)) . 0
by Def3
.=
<%x%> . 0
by A3, Def3
.=
x
;
A6:
for i being Nat st 1 <= i & i <= len q holds
p0 . i = q . i
proof
let i be
Nat;
( 1 <= i & i <= len q implies p0 . i = q . i )
assume that A7:
1
<= i
and A8:
i <= len q
;
p0 . i = q . i
A9:
i -' 1
= i - 1
by XREAL_0:def 2, A7, XREAL_1:48;
i < i + 1
by NAT_1:13;
then
i - 1
< (i + 1) - 1
by XREAL_1:9;
then A10:
i -' 1
< len q
by A8, A9, XXREAL_0:2;
then
i -' 1
in Segm (len q)
by NAT_1:44;
then A11:
i -' 1
in len (FS2XFS q)
by Def8;
i < 1
+ (len q)
by A8, NAT_1:13;
then
i < (len <%x%>) + (len (FS2XFS q))
by A4, Def8;
then
i in Segm ((len <%x%>) + (len (FS2XFS q)))
by NAT_1:44;
then
i in len (<%x%> ^ (FS2XFS q))
by Def3;
then p0 . i =
(<%x%> ^ (FS2XFS q)) . (1 + (i -' 1))
by A9, Def3
.=
(FS2XFS q) . (i -' 1)
by A4, A11, Def3
.=
q . ((i -' 1) + 1)
by A10, Def8
.=
q . i
by A9
;
hence
p0 . i = q . i
;
verum
end;
A12:
n - (len q) > 0
by A1, XREAL_1:50;
then A13:
n -' (len q) = n - (len q)
by XREAL_0:def 2;
then
n -' (len q) >= 0 + 1
by A12, NAT_1:13;
then A14:
(n -' (len q)) - 1 >= 0
by XREAL_1:48;
A15:
len q5 = (n -' (len q)) -' 1
;
A16:
for j being Nat st len q < j & j < n holds
p0 . j = 0
proof
let j be
Nat;
( len q < j & j < n implies p0 . j = 0 )
assume that A17:
len q < j
and A18:
j < n
;
p0 . j = 0
A19:
len (<%x%> ^ (FS2XFS q)) =
(len <%x%>) + (len (FS2XFS q))
by Def3
.=
1
+ (len q)
by A4, Def8
;
len q < n
by A17, A18, XXREAL_0:2;
then A20:
n - (len q) > 0
by XREAL_1:50;
then A21:
n -' (len q) = n - (len q)
by XREAL_0:def 2;
then
n - (len q) >= 0 + 1
by A20, NAT_1:13;
then
(n -' (len q)) - 1
>= 0
by A21, XREAL_1:48;
then A22:
(n -' (len q)) -' 1
= n - ((len q) + 1)
by A21, XREAL_0:def 2;
1
+ (len q) <= j
by A17, NAT_1:13;
then A23:
j -' (1 + (len q)) = j - (1 + (len q))
by XREAL_0:def 2, XREAL_1:48;
j - ((len q) + 1) < n - ((len q) + 1)
by A18, XREAL_1:9;
then A24:
j -' (len (<%x%> ^ (FS2XFS q))) in Segm ((n -' (len q)) -' 1)
by A19, A23, A22, NAT_1:44;
j = (len (<%x%> ^ (FS2XFS q))) + (j -' (len (<%x%> ^ (FS2XFS q))))
by A19, A23;
then p0 . j =
q5 . (j -' (len (<%x%> ^ (FS2XFS q))))
by A15, A24, Def3
.=
0
;
hence
p0 . j = 0
;
verum
end;
len p0 =
(len (<%x%> ^ (FS2XFS q))) + (len q5)
by Def3
.=
((len <%x%>) + (len (FS2XFS q))) + (len q5)
by Def3
.=
(1 + (len (FS2XFS q))) + (len q5)
by Th30
.=
(1 + (len q)) + (len q5)
by Def8
.=
(1 + (len q)) + ((n -' (len q)) -' 1)
.=
(n - ((len q) + 1)) + ((len q) + 1)
by A13, A14, XREAL_0:def 2
.=
n
;
hence
ex b1 being non empty XFinSequence of D st
( len q = b1 . 0 & len b1 = n & ( for i being Nat st 1 <= i & i <= len q holds
b1 . i = q . i ) & ( for j being Nat st len q < j & j < n holds
b1 . j = 0 ) )
by A5, A6, A16; verum