let j, k be Element of 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 q', r being FinSequence of D such that
A1: ( len q' = j + 1 & len r = k & p = q' ^ r ) by FINSEQ_2:26;
consider q being FinSequence of D, c being Element of D such that
A2: q' = q ^ <*c*> by A1, FINSEQ_2:22;
A3: len q' = (len q) + 1 by A2, 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 )
thus ( len q = j & len r = k & p = (q ^ <*c*>) ^ r ) by A1, A2, A3; :: thesis: verum