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