let n, k, m be Nat; :: thesis: for f, g being FinSequence st ( len f = n or len g = m ) & f ^ g in doms (k,(n + m)) holds
( f in doms (k,n) & g in doms (k,m) )
let f, g be FinSequence; :: thesis: ( ( len f = n or len g = m ) & f ^ g in doms (k,(n + m)) implies ( f in doms (k,n) & g in doms (k,m) ) )
set fg = f ^ g;
assume A1: ( ( len f = n or len g = m ) & f ^ g in doms (k,(n + m)) ) ; :: thesis: ( f in doms (k,n) & g in doms (k,m) )
then consider s being Element of (Seg k) * such that
A2: ( f ^ g = s & len s = n + m ) ;
reconsider s = s as FinSequence of Seg k ;
A3: len (f ^ g) = (len f) + (len g) by FINSEQ_1:22;
( rng f c= rng s & rng g c= rng s & rng s c= Seg k ) by A2, FINSEQ_1:30, FINSEQ_1:29;
then ( rng f c= Seg k & rng g c= Seg k ) ;
then ( f is FinSequence of Seg k & g is FinSequence of Seg k ) by FINSEQ_1:def 4;
then ( f in (Seg k) * & g in (Seg k) * ) by FINSEQ_1:def 11;
hence ( f in doms (k,n) & g in doms (k,m) ) by A3, A1, A2; :: thesis: verum