let f be Function of X,(n -tuples_on D); :: thesis: f is FinSequence-yielding
let x be set ; :: according to MATRLIN:def 1 :: thesis: ( not x in dom f or f . x is set )
assume x in dom f ; :: thesis: f . x is set
then reconsider fx = f . x as Element of n -tuples_on D by FUNCT_2:7;
fx = f . x ;
hence f . x is set ; :: thesis: verum