let n be Nat; :: thesis: for D being non empty set
for x being Tuple of n,D holds x in Funcs ((Seg n),D)
let D be non empty set ; :: thesis: for x being Tuple of n,D holds x in Funcs ((Seg n),D)
let x be Tuple of n,D; :: thesis: x in Funcs ((Seg n),D)
x in n -tuples_on D by FINSEQ_2:131;
hence x in Funcs ((Seg n),D) by FINSEQ_2:93; :: thesis: verum