let n, k, m be Nat; :: thesis: for f, g being FinSequence st f in doms (k,n) & g in doms (k,m) holds
f ^ g in doms (k,(n + m))
let f, g be FinSequence; :: thesis: ( f in doms (k,n) & g in doms (k,m) implies f ^ g in doms (k,(n + m)) )
assume A1: ( f in doms (k,n) & g in doms (k,m) ) ; :: thesis: f ^ g in doms (k,(n + m))
then consider p1 being Element of (Seg k) * such that
A2: ( p1 = f & len p1 = n ) ;
consider s1 being Element of (Seg k) * such that
A3: ( s1 = g & len s1 = m ) by A1;
A4: len (f ^ g) = n + m by A2, A3, FINSEQ_1:22;
A5: rng (f ^ g) = (rng f) \/ (rng g) by FINSEQ_1:31;
( rng s1 c= Seg k & rng p1 c= Seg k ) ;
then f ^ g is FinSequence of Seg k by FINSEQ_1:def 4, A5, A2, A3, XBOOLE_1:8;
then f ^ g is Element of (Seg k) * by FINSEQ_1:def 11;
hence f ^ g in doms (k,(n + m)) by A4; :: thesis: verum