defpred S₁[ 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₁[x,y] )

proof

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₁[x,y] ) )
assume x in BOOL the carrier of V ; :: thesis: ex y being object st
( y in the carrier of V & S₁[x,y] )
then reconsider A = x as Subset of V ;

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

suppose A is finite ; :: thesis: ex y being object st
( y in the carrier of V & S₁[x,y] )

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₁[x,(1 / (card A1)) * (Sum A1)] )
thus ( (1 / (card A1)) * (Sum A1) in the carrier of V & S₁[x,(1 / (card A1)) * (Sum A1)] ) ; :: thesis: verum

end;

suppose A2: A is infinite ; :: thesis: ex y being object st
( y in the carrier of V & S₁[x,y] )

take 0. V ; :: thesis: ( 0. V in the carrier of V & S₁[x, 0. V] )
thus ( 0. V in the carrier of V & S₁[x, 0. V] ) by A2; :: thesis: verum

end;

end;

end;

consider f being Function of (BOOL the carrier of V), the carrier of V such that
A3: for x being object st x in BOOL the carrier of V holds
S₁[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 ) )

hereby :: thesis: for A being Subset of V st A is infinite holds
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;

let A be Subset of V; :: thesis: ( A is infinite implies 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