defpred S₂[ FinSequence] means for p, q, s being FinSequence st p ^ q = $1 ^ s & len p <= len $1 holds
ex t being FinSequence st p ^ t = $1;
A1: S₂[ {} ]

proof

let p, q, s be FinSequence; :: thesis: ( p ^ q = {} ^ s & len p <= len {} implies ex t being FinSequence st p ^ t = {} )
assume B2: ( p ^ q = {} ^ s & len p <= len {} ) ; :: thesis: ex t being FinSequence st p ^ t = {}
take {} ; :: thesis: p ^ {} = {}
thus p ^ {} = p by Th47
.= {} by B2 ; :: thesis: verum

end;

A3: for r being FinSequence
for x being set st S₂[r] holds
S₂[r ^ <*x*>]

proof

let r be FinSequence; :: 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 FinSequence st p ^ q = r ^ s & len p <= len r holds
ex t being FinSequence st p ^ t = r ; :: thesis: S₂[r ^ <*x*>]
let p, q, s be FinSequence; :: thesis: ( p ^ q = (r ^ <*x*>) ^ s & len p <= len (r ^ <*x*>) implies ex t being FinSequence st p ^ t = r ^ <*x*> )
assume A5: ( p ^ q = (r ^ <*x*>) ^ s & len p <= len (r ^ <*x*>) ) ; :: thesis: ex t being FinSequence st p ^ t = r ^ <*x*>

A6: now

assume len p = len (r ^ <*x*>) ; :: thesis: ex t being FinSequence st p ^ t = r ^ <*x*>
then A7: dom p = Seg (len (r ^ <*x*>)) by Def3
.= dom (r ^ <*x*>) by Def3 ;
A8: 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 A9: k in dom p ; :: thesis: p . k = (r ^ <*x*>) . k
hence p . k = ((r ^ <*x*>) ^ s) . k by A5, Def7
.= (r ^ <*x*>) . k by A7, A9, Def7 ;
:: thesis: verum

end;

p ^ {} = p by Th47
.= r ^ <*x*> by A7, A8, Th17 ;
hence ex t being FinSequence st p ^ t = r ^ <*x*> ; :: thesis: verum

end;

now

assume len p <> len (r ^ <*x*>) ; :: thesis: ex t being FinSequence st p ^ t = r ^ <*x*>
then len p <> (len r) + (len <*x*>) by Th35;
then A10: len p <> (len r) + 1 by Th56;
len p <= (len r) + (len <*x*>) by A5, Th35;
then B11: len p <= (len r) + 1 by Th56;
p ^ q = r ^ (<*x*> ^ s) by A5, Th45;
then consider t being FinSequence such that
A12: p ^ t = r by A4, B11, A10, NAT_1:8;
p ^ (t ^ <*x*>) = r ^ <*x*> by A12, Th45;
hence ex t being FinSequence st p ^ t = r ^ <*x*> ; :: thesis: verum

end;

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

end;

for r being FinSequence holds S₂[r] from FINSEQ_1:sch 3(A1, A3);
hence for p, q, r, s being FinSequence st p ^ q = r ^ s & len p <= len r holds
ex t being FinSequence st p ^ t = r ; :: thesis: verum