let i, j be natural Number ; :: thesis: for D being non empty set
for r being b₁ -valued FinSequence st len r = i + j holds
ex p, q being FinSequence of D st
( len p = i & len q = j & r = p ^ q )
let D be non empty set ; :: thesis: for r being D -valued FinSequence st len r = i + j holds
ex p, q being FinSequence of D st
( len p = i & len q = j & r = p ^ q )
let r be D -valued FinSequence; :: thesis: ( len r = i + j implies ex p, q being FinSequence of D st
( len p = i & len q = j & r = p ^ q ) )
assume len r = i + j ; :: thesis: ex p, q being FinSequence of D st
( len p = i & len q = j & r = p ^ q )
then consider p, q being FinSequence such that
A1: ( len p = i & len q = j ) and
A2: r = p ^ q by Th20;
( p is FinSequence of D & q is FinSequence of D ) by A2, FINSEQ_1:36;
hence ex p, q being FinSequence of D st
( len p = i & len q = j & r = p ^ q ) by A1, A2; :: thesis: verum