let i, j be natural Number ; :: thesis: for r being FinSequence st len r = i + j holds
ex p, q being FinSequence st
( len p = i & len q = j & r = p ^ q )
let r be FinSequence; :: thesis: ( len r = i + j implies ex p, q being FinSequence st
( len p = i & len q = j & r = p ^ q ) )
assume A1: len r = i + j ; :: thesis: ex p, q being FinSequence st
( len p = i & len q = j & r = p ^ q )
reconsider z = i as Element of NAT by ORDINAL1:def 12;
reconsider p = r | (Seg z) as FinSequence by FINSEQ_1:15;
consider q being FinSequence such that
A2: r = p ^ q by FINSEQ_1:80;
take p ; :: thesis: ex q being FinSequence st
( len p = i & len q = j & r = p ^ q )
take q ; :: thesis: ( len p = i & len q = j & r = p ^ q )
i <= len r by A1, NAT_1:11;
hence len p = i by FINSEQ_1:17; :: thesis: ( len q = j & r = p ^ q )
then len (p ^ q) = i + (len q) by FINSEQ_1:22;
hence len q = j by A1, A2; :: thesis: r = p ^ q
thus r = p ^ q by A2; :: thesis: verum