defpred S_{1}[ object , object ] means ( ( for A being non empty finite Subset of V st A = $1 holds

$2 = (1 / (card A)) * (Sum A) ) & ( for A being Subset of V st A is infinite & A = $1 holds

$2 = 0. V ) );

set cV = the carrier of V;

A1: for x being object st x in BOOL the carrier of V holds

ex y being object st

( y in the carrier of V & S_{1}[x,y] )

A3: for x being object st x in BOOL the carrier of V holds

S_{1}[x,f . x]
from FUNCT_2:sch 1(A1);

take f ; :: thesis: ( ( for A being non empty finite Subset of V holds f . A = (1 / (card A)) * (Sum A) ) & ( for A being Subset of V st A is infinite holds

f . A = 0. V ) )

assume A4: A is infinite ; :: thesis: f . A = 0. V

then A in (bool the carrier of V) \ {{}} by ZFMISC_1:56;

hence f . A = 0. V by A3, A4; :: thesis: verum

$2 = (1 / (card A)) * (Sum A) ) & ( for A being Subset of V st A is infinite & A = $1 holds

$2 = 0. V ) );

set cV = the carrier of V;

A1: for x being object st x in BOOL the carrier of V holds

ex y being object st

( y in the carrier of V & S

proof

consider f being Function of (BOOL the carrier of V), the carrier of V such that
let x be object ; :: thesis: ( x in BOOL the carrier of V implies ex y being object st

( y in the carrier of V & S_{1}[x,y] ) )

assume x in BOOL the carrier of V ; :: thesis: ex y being object st

( y in the carrier of V & S_{1}[x,y] )

then reconsider A = x as Subset of V ;

end;( y in the carrier of V & S

assume x in BOOL the carrier of V ; :: thesis: ex y being object st

( y in the carrier of V & S

then reconsider A = x as Subset of V ;

per cases
( A is finite or A is infinite )
;

end;

suppose
A is finite
; :: thesis: ex y being object st

( y in the carrier of V & S_{1}[x,y] )

( y in the carrier of V & S

then reconsider A1 = A as finite Subset of V ;

take (1 / (card A1)) * (Sum A1) ; :: thesis: ( (1 / (card A1)) * (Sum A1) in the carrier of V & S_{1}[x,(1 / (card A1)) * (Sum A1)] )

thus ( (1 / (card A1)) * (Sum A1) in the carrier of V & S_{1}[x,(1 / (card A1)) * (Sum A1)] )
; :: thesis: verum

end;take (1 / (card A1)) * (Sum A1) ; :: thesis: ( (1 / (card A1)) * (Sum A1) in the carrier of V & S

thus ( (1 / (card A1)) * (Sum A1) in the carrier of V & S

A3: for x being object st x in BOOL the carrier of V holds

S

take f ; :: thesis: ( ( for A being non empty finite Subset of V holds f . A = (1 / (card A)) * (Sum A) ) & ( for A being Subset of V st A is infinite holds

f . A = 0. V ) )

hereby :: thesis: for A being Subset of V st A is infinite holds

f . A = 0. V

let A be Subset of V; :: thesis: ( A is infinite implies f . A = 0. V )f . A = 0. V

let A be non empty finite Subset of V; :: thesis: f . A = (1 / (card A)) * (Sum A)

A in BOOL the carrier of V by ZFMISC_1:56;

hence f . A = (1 / (card A)) * (Sum A) by A3; :: thesis: verum

end;A in BOOL the carrier of V by ZFMISC_1:56;

hence f . A = (1 / (card A)) * (Sum A) by A3; :: thesis: verum

assume A4: A is infinite ; :: thesis: f . A = 0. V

then A in (bool the carrier of V) \ {{}} by ZFMISC_1:56;

hence f . A = 0. V by A3, A4; :: thesis: verum