let i, j be Nat; :: thesis: for D being non empty set
for r being b₁ -valued FinSequence st len r = i + j holds
ex p, q being b₁ -valued FinSequence 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 D -valued FinSequence 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 D -valued FinSequence st
( len p = i & len q = j & r = p ^ q ) )
assume A1: len r = i + j ; :: thesis: ex p, q being D -valued FinSequence st
( len p = i & len q = j & r = p ^ q )
reconsider r1 = r as FinSequence of D by NEWTON02:103;
ex p1, q1 being FinSequence of D st
( len p1 = i & len q1 = j & r1 = p1 ^ q1 ) by A1, FINSEQ_2:23;
hence ex p, q being D -valued FinSequence st
( len p = i & len q = j & r = p ^ q ) ; :: thesis: verum