let F, G be FinSequence-yielding FinSequence; :: thesis: for f, g being FinSequence st f in doms F & g in doms G holds
f ^ g in doms (F ^ G)
let f, g be FinSequence; :: thesis: ( f in doms F & g in doms G implies f ^ g in doms (F ^ G) )
set fg = f ^ g;
set FG = F ^ G;
assume A1: ( f in doms F & g in doms G ) ; :: thesis: f ^ g in doms (F ^ G)
A2: ( len (f ^ g) = (len f) + (len g) & len (F ^ G) = (len F) + (len G) ) by FINSEQ_1:22;
A3: ( len f = len F & len g = len G ) by A1, Th47;
for i being Nat st i in dom (f ^ g) holds
(f ^ g) . i in dom ((F ^ G) . i)

proof

let i be Nat; :: thesis: ( i in dom (f ^ g) implies (f ^ g) . i in dom ((F ^ G) . i) )
assume A4: i in dom (f ^ g) ; :: thesis: (f ^ g) . i in dom ((F ^ G) . i)

per cases ( i in dom f or ex j being Nat st
( j in dom g & i = (len f) + j ) ) by A4, FINSEQ_1:25;

suppose A5: i in dom f ; :: thesis: (f ^ g) . i in dom ((F ^ G) . i)

then i in dom F by A3, FINSEQ_3:29;
then ( f . i = (f ^ g) . i & F . i = (F ^ G) . i ) by A5, FINSEQ_1:def 7;
hence (f ^ g) . i in dom ((F ^ G) . i) by A1, Th47, A5; :: thesis: verum

end;

suppose ex j being Nat st
( j in dom g & i = (len f) + j ) ; :: thesis: (f ^ g) . i in dom ((F ^ G) . i)

then consider j being Nat such that
A6: ( j in dom g & i = (len f) + j ) ;
j in dom G by A6, A3, FINSEQ_3:29;
then ( g . j = (f ^ g) . i & G . j = (F ^ G) . i ) by A6, A3, FINSEQ_1:def 7;
hence (f ^ g) . i in dom ((F ^ G) . i) by A1, Th47, A6; :: thesis: verum

end;

end;

end;

hence f ^ g in doms (F ^ G) by A2, A3, Th47; :: thesis: verum