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