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: S₁[ {} ]

proof

let p, q, s be XFinSequence; :: thesis: ( p ^ q = {} ^ s & len p <= len {} implies ex t being XFinSequence st p ^ t = {} )
assume ( p ^ q = {} ^ s & len p <= len {} ) ; :: thesis: ex t being XFinSequence st p ^ t = {}
then A2: len p = 0 ;
take {} ; :: thesis: p ^ {} = {}
thus p ^ {} = p by Th32
.= {} by A2 ; :: thesis: verum

end;

A3: for r being XFinSequence
for x being set st S₁[r] holds
S₁[r ^ <%x%>]

proof

let r be XFinSequence; :: thesis: for x being set st S₁[r] holds
S₁[r ^ <%x%>]
let x be set ; :: thesis: ( S₁[r] implies S₁[r ^ <%x%>] )
assume A4: 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 A5: ( p ^ q = (r ^ <%x%>) ^ s & len p <= len (r ^ <%x%>) ) ; :: thesis: ex t being XFinSequence st p ^ t = r ^ <%x%>

A6: now

assume Z: len p = len (r ^ <%x%>) ; :: thesis: ex t being XFinSequence st p ^ t = r ^ <%x%>
A8: for k being Element of NAT st k in dom p holds
p . k = (r ^ <%x%>) . k

proof

let k be Element of NAT ; :: thesis: ( k in dom p implies p . k = (r ^ <%x%>) . k )
assume A9: k in dom p ; :: thesis: p . k = (r ^ <%x%>) . k
hence p . k = ((r ^ <%x%>) ^ s) . k by A5, Def4
.= (r ^ <%x%>) . k by Z, A9, Def4 ;
:: thesis: verum

end;

p ^ {} = p by Th32
.= r ^ <%x%> by Z, A8, Th10 ;
hence ex t being XFinSequence st p ^ t = r ^ <%x%> ; :: thesis: verum

end;

now

assume len p <> len (r ^ <%x%>) ; :: thesis: ex t being XFinSequence st p ^ t = r ^ <%x%>
then len p <> (len r) + (len <%x%>) by Def4;
then A10: len p <> (len r) + 1 by Th36;
len p <= (len r) + (len <%x%>) by A5, Def4;
then B11: len p <= (len r) + 1 by Th36;
p ^ q = r ^ (<%x%> ^ s) by A5, Th30;
then consider t being XFinSequence such that
A12: p ^ t = r by A4, B11, A10, NAT_1:8;
p ^ (t ^ <%x%>) = r ^ <%x%> by A12, Th30;
hence ex t being XFinSequence st p ^ t = r ^ <%x%> ; :: thesis: verum

end;

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

end;

for r being XFinSequence holds S₁[r] from AFINSQ_1:sch 3(A1, A3);
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