let X be non empty set ; :: thesis: for x being Element of X ex f being Enumeration of X st f . x = 0
let x be Element of X; :: thesis: ex f being Enumeration of X st f . x = 0
consider f being Enumeration of X;
( 0 in card X & dom f = X & rng f = card X ) by ThNum1, ORDINAL3:10;
then consider y being set such that
A1: ( y in X & 0 = f . y ) by FUNCT_1:def 5;
reconsider y = y as Element of X by A1;
reconsider g = (f +* y,(f . x)) +* x,0 as Enumeration of X by A1, ThNum6;
take g ; :: thesis: g . x = 0
dom f = X by ThNum1;
then dom (f +* y,(f . x)) = X by FUNCT_7:32;
hence g . x = 0 by FUNCT_7:33; :: thesis: verum