let j, k be Nat; :: thesis: for D being non empty set

for p being FinSequence of D st len p = (j + 1) + k holds

ex q, r being FinSequence of D ex c being Element of D st

( len q = j & len r = k & p = (q ^ <*c*>) ^ r )

let D be non empty set ; :: thesis: for p being FinSequence of D st len p = (j + 1) + k holds

ex q, r being FinSequence of D ex c being Element of D st

( len q = j & len r = k & p = (q ^ <*c*>) ^ r )

let p be FinSequence of D; :: thesis: ( len p = (j + 1) + k implies ex q, r being FinSequence of D ex c being Element of D st

( len q = j & len r = k & p = (q ^ <*c*>) ^ r ) )

assume len p = (j + 1) + k ; :: thesis: ex q, r being FinSequence of D ex c being Element of D st

( len q = j & len r = k & p = (q ^ <*c*>) ^ r )

then consider q9, r being FinSequence of D such that

A1: len q9 = j + 1 and

A2: ( len r = k & p = q9 ^ r ) by FINSEQ_2:23;

consider q being FinSequence of D, c being Element of D such that

A3: q9 = q ^ <*c*> by A1, FINSEQ_2:19;

take q ; :: thesis: ex r being FinSequence of D ex c being Element of D st

( len q = j & len r = k & p = (q ^ <*c*>) ^ r )

take r ; :: thesis: ex c being Element of D st

( len q = j & len r = k & p = (q ^ <*c*>) ^ r )

take c ; :: thesis: ( len q = j & len r = k & p = (q ^ <*c*>) ^ r )

len q9 = (len q) + 1 by A3, FINSEQ_2:16;

hence ( len q = j & len r = k & p = (q ^ <*c*>) ^ r ) by A1, A2, A3; :: thesis: verum

for p being FinSequence of D st len p = (j + 1) + k holds

ex q, r being FinSequence of D ex c being Element of D st

( len q = j & len r = k & p = (q ^ <*c*>) ^ r )

let D be non empty set ; :: thesis: for p being FinSequence of D st len p = (j + 1) + k holds

ex q, r being FinSequence of D ex c being Element of D st

( len q = j & len r = k & p = (q ^ <*c*>) ^ r )

let p be FinSequence of D; :: thesis: ( len p = (j + 1) + k implies ex q, r being FinSequence of D ex c being Element of D st

( len q = j & len r = k & p = (q ^ <*c*>) ^ r ) )

assume len p = (j + 1) + k ; :: thesis: ex q, r being FinSequence of D ex c being Element of D st

( len q = j & len r = k & p = (q ^ <*c*>) ^ r )

then consider q9, r being FinSequence of D such that

A1: len q9 = j + 1 and

A2: ( len r = k & p = q9 ^ r ) by FINSEQ_2:23;

consider q being FinSequence of D, c being Element of D such that

A3: q9 = q ^ <*c*> by A1, FINSEQ_2:19;

take q ; :: thesis: ex r being FinSequence of D ex c being Element of D st

( len q = j & len r = k & p = (q ^ <*c*>) ^ r )

take r ; :: thesis: ex c being Element of D st

( len q = j & len r = k & p = (q ^ <*c*>) ^ r )

take c ; :: thesis: ( len q = j & len r = k & p = (q ^ <*c*>) ^ r )

len q9 = (len q) + 1 by A3, FINSEQ_2:16;

hence ( len q = j & len r = k & p = (q ^ <*c*>) ^ r ) by A1, A2, A3; :: thesis: verum