let n be Nat; :: thesis: for F being FinSequence-yielding FinSequence
for f being FinSequence st f in doms F holds
f | n in doms (F | n)
let F be FinSequence-yielding FinSequence; :: thesis: for f being FinSequence st f in doms F holds
f | n in doms (F | n)
let f be FinSequence; :: thesis: ( f in doms F implies f | n in doms (F | n) )
assume A1: f in doms F ; :: thesis: f | n in doms (F | n)
then A2: len f = len F by Th47;

per cases ( n > len f or n <= len f ) ;

suppose n > len f ; :: thesis: f | n in doms (F | n)

then ( f | n = f & F | n = F ) by A2, FINSEQ_1:58;
hence f | n in doms (F | n) by A1; :: thesis: verum

end;

suppose n <= len f ; :: thesis: f | n in doms (F | n)

then A3: ( len (f | n) = n & len (F | n) = n ) by A2, FINSEQ_1:59;
then A4: dom (f | n) = dom (F | n) by FINSEQ_3:30;
for i being Nat st i in dom (f | n) holds
(f | n) . i in dom ((F | n) . i)

proof

let i be Nat; :: thesis: ( i in dom (f | n) implies (f | n) . i in dom ((F | n) . i) )
assume i in dom (f | n) ; :: thesis: (f | n) . i in dom ((F | n) . i)
then ( (f | n) . i = f . i & (F | n) . i = F . i & i in dom f ) by A4, FUNCT_1:47, RELAT_1:57;
hence (f | n) . i in dom ((F | n) . i) by A1, Th47; :: thesis: verum

end;

hence f | n in doms (F | n) by A3, Th47; :: thesis: verum

end;

end;