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

proof

let i be Nat; :: thesis: ( i in dom f implies f . i in dom (F . i) )
assume i in dom f ; :: thesis: f . i in dom (F . i)
then ( i in dom (f ^ g) & f . i = (f ^ g) . i & F . i = (F ^ G) . i ) by A3, TARSKI:def 3, FINSEQ_1:26, FINSEQ_1:def 7;
hence f . i in dom (F . i) by A1, Th47; :: thesis: verum

end;

hence f in doms F by A2, A1, Th47; :: thesis: g in doms G
for i being Nat st i in dom g holds
g . i in dom (G . i)

proof

let i be Nat; :: thesis: ( i in dom g implies g . i in dom (G . i) )
assume A4: i in dom g ; :: thesis: g . i in dom (G . i)
then A5: (len f) + i in dom (f ^ g) by FINSEQ_1:28;
( g . i = (f ^ g) . ((len f) + i) & G . i = (F ^ G) . ((len F) + i) ) by A4, A3, FINSEQ_1:def 7;
hence g . i in dom (G . i) by A5, A1, A2, Th47; :: thesis: verum

end;

hence g in doms G by A2, A1, Th47; :: thesis: verum