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 that
p ^ q = {} ^ s and
A2: len p <= len {} ; :: thesis: ex t being FinSequence st p ^ t = {}
take {} ; :: thesis: p ^ {} = {}
thus p ^ {} = p by Th34
.= {} by A2 ; :: thesis: verum

end;

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

proof

let r be FinSequence; :: thesis: for x being object st S₂[r] holds
S₂[r ^ <*x*>]
let x be object ; :: 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 that
A5: p ^ q = (r ^ <*x*>) ^ s and
A6: len p <= len (r ^ <*x*>) ; :: thesis: ex t being FinSequence st p ^ t = r ^ <*x*>

A7: now :: thesis: ( len p = len (r ^ <*x*>) implies ex t being FinSequence st p ^ t = r ^ <*x*> )

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

end;

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

end;

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

assume len p <> len (r ^ <*x*>) ; :: thesis: ex t being FinSequence st p ^ t = r ^ <*x*>
then len p <> (len r) + (len <*x*>) by Th22;
then A11: len p <> (len r) + 1 by Th39;
len p <= (len r) + (len <*x*>) by A6, Th22;
then A12: len p <= (len r) + 1 by Th39;
p ^ q = r ^ (<*x*> ^ s) by A5, Th32;
then consider t being FinSequence such that
A13: p ^ t = r by A4, A11, A12, NAT_1:8;
p ^ (t ^ <*x*>) = r ^ <*x*> by A13, Th32;
hence ex t being FinSequence st p ^ t = r ^ <*x*> ; :: thesis: verum

end;

hence ex t being FinSequence st p ^ t = r ^ <*x*> by A7; :: 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