let i, j be Nat; :: thesis: for D being non empty set
for r being FinSequence of D 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 FinSequence of D 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 FinSequence of D; :: 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 Th25;
( p is FinSequence of D & q is FinSequence of D ) by A2, FINSEQ_1:50;
hence ex p, q being FinSequence of D st
( len p = i & len q = j & r = p ^ q ) by A1, A2; :: thesis: verum