defpred S₁[ XFinSequence] means for p, q, s being XFinSequence st p ^ q = $1 ^ s & len p <= len $1 holds
ex t being XFinSequence st p ^ t = $1;
A1: for r being XFinSequence
for x being object st S₁[r] holds
S₁[r ^ <%x%>]

proof

let r be XFinSequence; :: thesis: for x being object st S₁[r] holds
S₁[r ^ <%x%>]
let x be object ; :: thesis: ( S₁[r] implies S₁[r ^ <%x%>] )
assume A2: for p, q, s being XFinSequence st p ^ q = r ^ s & len p <= len r holds
ex t being XFinSequence st p ^ t = r ; :: thesis: S₁[r ^ <%x%>]
let p, q, s be XFinSequence; :: thesis: ( p ^ q = (r ^ <%x%>) ^ s & len p <= len (r ^ <%x%>) implies ex t being XFinSequence st p ^ t = r ^ <%x%> )
assume that
A3: p ^ q = (r ^ <%x%>) ^ s and
A4: len p <= len (r ^ <%x%>) ; :: thesis: ex t being XFinSequence st p ^ t = r ^ <%x%>

A5: now :: thesis: ( len p <> len (r ^ <%x%>) implies ex t being XFinSequence st p ^ t = r ^ <%x%> )

assume len p <> len (r ^ <%x%>) ; :: thesis: ex t being XFinSequence st p ^ t = r ^ <%x%>
then len p <> (len r) + (len <%x%>) by Def3;
then A6: len p <> (len r) + 1 by Th30;
len p <= (len r) + (len <%x%>) by A4, Def3;
then A7: len p <= (len r) + 1 by Th30;
p ^ q = r ^ (<%x%> ^ s) by A3, Th25;
then consider t being XFinSequence such that
A8: p ^ t = r by A2, A6, A7, NAT_1:8;
p ^ (t ^ <%x%>) = r ^ <%x%> by A8, Th25;
hence ex t being XFinSequence st p ^ t = r ^ <%x%> ; :: thesis: verum

end;

now :: thesis: ( len p = len (r ^ <%x%>) implies ex t being XFinSequence st p ^ t = r ^ <%x%> )

assume A9: len p = len (r ^ <%x%>) ; :: thesis: ex t being XFinSequence st p ^ t = r ^ <%x%>
A10: for k being Nat st k in dom p holds
p . k = (r ^ <%x%>) . k

proof

let k be Nat; :: thesis: ( k in dom p implies p . k = (r ^ <%x%>) . k )
assume A11: k in dom p ; :: thesis: p . k = (r ^ <%x%>) . k
hence p . k = ((r ^ <%x%>) ^ s) . k by A3, Def3
.= (r ^ <%x%>) . k by A9, A11, Def3 ;
:: thesis: verum

end;

p ^ {} = r ^ <%x%> by A9, A10;
hence ex t being XFinSequence st p ^ t = r ^ <%x%> ; :: thesis: verum

end;

hence ex t being XFinSequence st p ^ t = r ^ <%x%> by A5; :: thesis: verum

end;

A12: S₁[ {} ]

proof

let p, q, s be XFinSequence; :: thesis: ( p ^ q = {} ^ s & len p <= len {} implies ex t being XFinSequence st p ^ t = {} )
assume that
p ^ q = {} ^ s and
A13: len p <= len {} ; :: thesis: ex t being XFinSequence st p ^ t = {}
take {} ; :: thesis: p ^ {} = {}
thus p ^ {} = {} by A13; :: thesis: verum

end;

for r being XFinSequence holds S₁[r] from AFINSQ_1:sch 3(A12, A1);
hence for p, q, r, s being XFinSequence st p ^ q = r ^ s & len p <= len r holds
ex t being XFinSequence st p ^ t = r ; :: thesis: verum