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;
A1: 0 in card X by ORDINAL3:10;
A2: rng f = card X by Th6;
dom f = X by Th6;
then consider y being set such that
A3: y in X and
A4: 0 = f . y by A1, A2, FUNCT_1:def 5;
reconsider y = y as Element of X by A3;
reconsider g = (f +* y,(f . x)) +* x,0 as Enumeration of X by A4, Th8;
take g ; :: thesis: g . x = 0
dom f = X by Th6;
then dom (f +* y,(f . x)) = X by FUNCT_7:32;
hence g . x = 0 by FUNCT_7:33; :: thesis: verum