defpred S₁[ set , set ] 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 not A is finite & A = $1 holds
$2 = 0. V ) );
set cV = the carrier of V;
A1: for x being set st x in BOOL the carrier of V holds
ex y being set st
( y in the carrier of V & S₁[x,y] )

proof

let x be set ; :: thesis: ( x in BOOL the carrier of V implies ex y being set st
( y in the carrier of V & S₁[x,y] ) )
assume x in BOOL the carrier of V ; :: thesis: ex y being set st
( y in the carrier of V & S₁[x,y] )
then reconsider A = x as Subset of V ;

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

suppose A is finite ; :: thesis: ex y being set 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: not A is finite ; :: thesis: ex y being set 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 set 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 not A is finite holds
f . A = 0. V ) )

hereby :: thesis: for A being Subset of V st not A is finite 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:64;
hence f . A = (1 / (card A)) * (Sum A) by A3; :: thesis: verum

end;

let A be Subset of V; :: thesis: ( not A is finite implies f . A = 0. V )
assume A4: not A is finite ; :: thesis: f . A = 0. V
then A in (bool the carrier of V) \ {{} } by ZFMISC_1:64;
hence f . A = 0. V by A3, A4; :: thesis: verum