len q in NAT ;
then reconsider x = len q as Element of D by A2;
0 in NAT ;
then reconsider r = 0 as Element of D by A2;
reconsider q5 = ((n -' (len q)) -' 1) --> r as XFinSequence of D by Th4;
<%x%> ^ (FS2XFS q) <> {} by Th33;
then reconsider p0 = (<%x%> ^ (FS2XFS q)) ^ q5 as non empty XFinSequence of D by Th33;
0 in 1 by NAT_1:45;
then A3: 0 in dom <%x%> by Def5;
A4: len <%x%> = 1 by Def5;
0 in (len <%x%>) + (len (FS2XFS q)) by NAT_1:45;
then 0 in len (<%x%> ^ (FS2XFS q)) by Th20;
then A5: p0 . 0 = (<%x%> ^ (FS2XFS q)) . 0 by Def4
.= <%x%> . 0 by A3, Def4
.= x by Def5 ;
A6: for i being Nat st 1 <= i & i <= len q holds
p0 . i = q . i

proof

let i be Nat; :: thesis: ( 1 <= i & i <= len q implies p0 . i = q . i )
assume that
A7: 1 <= i and
A8: i <= len q ; :: thesis: p0 . i = q . i
i - 1 >= 0 by A7, XREAL_1:50;
then A9: i -' 1 = i - 1 by XREAL_0:def 2;
i < i + 1 by NAT_1:13;
then i - 1 < (i + 1) - 1 by XREAL_1:11;
then A10: i -' 1 < len q by A8, A9, XXREAL_0:2;
then i -' 1 in len q by NAT_1:45;
then A11: i -' 1 in len (FS2XFS q) by Def1;
i < 1 + (len q) by A8, NAT_1:13;
then i < (len <%x%>) + (len (FS2XFS q)) by A4, Def1;
then i in (len <%x%>) + (len (FS2XFS q)) by NAT_1:45;
then i in len (<%x%> ^ (FS2XFS q)) by Th20;
then p0 . i = (<%x%> ^ (FS2XFS q)) . (1 + (i -' 1)) by A9, Def4
.= (FS2XFS q) . (i -' 1) by A4, A11, Def4
.= q . ((i -' 1) + 1) by A10, Def1
.= q . i by A9 ;
hence p0 . i = q . i ; :: thesis: verum

end;

A12: n - (len q) > 0 by A1, XREAL_1:52;
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:50;
A15: len q5 = (n -' (len q)) -' 1 by FUNCOP_1:19;
A16: for j being Nat st len q < j & j < n holds
p0 . j = 0

proof

let j be Nat; :: thesis: ( len q < j & j < n implies p0 . j = 0 )
assume that
A17: len q < j and
A18: j < n ; :: thesis: p0 . j = 0
A19: len (<%x%> ^ (FS2XFS q)) = (len <%x%>) + (len (FS2XFS q)) by Th20
.= 1 + (len q) by A4, Def1 ;
len q < n by A17, A18, XXREAL_0:2;
then A20: n - (len q) > 0 by XREAL_1:52;
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:50;
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 j - (1 + (len q)) >= 0 by XREAL_1:50;
then A23: j -' (1 + (len q)) = j - (1 + (len q)) by XREAL_0:def 2;
j - ((len q) + 1) < n - ((len q) + 1) by A18, XREAL_1:11;
then A24: j -' (len (<%x%> ^ (FS2XFS q))) in (n -' (len q)) -' 1 by A19, A23, A22, NAT_1:45;
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, Def4
.= 0 by A24, FUNCOP_1:13 ;
hence p0 . j = 0 ; :: thesis: verum

end;

len p0 = (len (<%x%> ^ (FS2XFS q))) + (len q5) by Th20
.= ((len <%x%>) + (len (FS2XFS q))) + (len q5) by Th20
.= (1 + (len (FS2XFS q))) + (len q5) by Th36
.= (1 + (len q)) + (len q5) by Def1
.= (1 + (len q)) + ((n -' (len q)) -' 1) by FUNCOP_1:19
.= (n - ((len q) + 1)) + ((len q) + 1) by A13, A14, XREAL_0:def 2
.= n ;
hence ex b₁ being non empty XFinSequence of D st
( len q = b₁ . 0 & len b₁ = n & ( for i being Nat st 1 <= i & i <= len q holds
b₁ . i = q . i ) & ( for j being Nat st len q < j & j < n holds
b₁ . j = 0 ) ) by A5, A6, A16; :: thesis: verum