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

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