let f be FinSequence of D * ; :: thesis: f is FinSequence-yielding
let x be set ; :: according to PRE_POLY:def 3 :: thesis: ( x in dom f implies f . x is FinSequence )
assume A1: x in dom f ; :: thesis: f . x is FinSequence
then reconsider x = x as Element of NAT ;
f . x in D * by A1, FINSEQ_2:11;
hence f . x is FinSequence ; :: thesis: verum