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