reconsider Y = X as non empty Subset of (product (I --> L)) ;
consider f being Element of Y;
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