not X is empty ;
then consider x0 being object such that
A1: x0 in X ;
reconsider x0 = x0 as Element of X by A1;
A2: product ((Seg n) --> X) = n -tuples_on X by Th8;
set f = product (n |-> x0);
product (n |-> x0) in Product (n,X) by A2, Def2;
hence not Product (n,X) is empty ; :: thesis: verum