thus ( ( p = {} or q = {} ) implies ex r being FinSequence st r = p ^ q ) ; :: thesis: ( p = {} or q = {} or ex b₁ being FinSequence ex i being Nat ex r being FinSequence st
( len p = i + 1 & r = p | (Seg i) & b₁ = r ^ q ) )
assume that
A1: p <> {} and
q <> {} ; :: thesis: ex b₁ being FinSequence ex i being Nat ex r being FinSequence st
( len p = i + 1 & r = p | (Seg i) & b₁ = r ^ q )
len p >= 0 + 1 by A1, NAT_1:13;
then consider i being Nat such that
A2: len p = 1 + i by NAT_1:10;
reconsider i = i as Nat ;
reconsider r = p | (Seg i) as FinSequence by FINSEQ_1:15;
take r ^ q ; :: thesis: ex i being Nat ex r being FinSequence st
( len p = i + 1 & r = p | (Seg i) & r ^ q = r ^ q )
take i ; :: thesis: ex r being FinSequence st
( len p = i + 1 & r = p | (Seg i) & r ^ q = r ^ q )
take r ; :: thesis: ( len p = i + 1 & r = p | (Seg i) & r ^ q = r ^ q )
thus ( len p = i + 1 & r = p | (Seg i) & r ^ q = r ^ q ) by A2; :: thesis: verum