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