consider f being Element of X;
reconsider f = f as Function ;
f . i in pi X,i by CARD_3:def 6;
hence not pi X,i is empty ; :: thesis: verum