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: ( not x in proj1 p or p . x is set )
assume A1: x in dom p ; :: thesis: p . x is set
then reconsider i = x as Element of NAT ;
p . i is Element of n -tuples_on D by A1, FINSEQ_2:13;
hence p . x is set ; :: thesis: verum