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