set cV = the carrier of V;
let F1, F2 be Function of (BOOL the carrier of V), the carrier of V; :: thesis: ( ( for A being non empty finite Subset of V holds F1 . A = (1 / (card A)) * (Sum A) ) & ( for A being Subset of V st A is infinite holds
F1 . A = 0. V ) & ( for A being non empty finite Subset of V holds F2 . A = (1 / (card A)) * (Sum A) ) & ( for A being Subset of V st A is infinite holds
F2 . A = 0. V ) implies F1 = F2 )
assume that
A5: for A being non empty finite Subset of V holds F1 . A = (1 / (card A)) * (Sum A) and
A6: for A being Subset of V st A is infinite holds
F1 . A = 0. V and
A7: for A being non empty finite Subset of V holds F2 . A = (1 / (card A)) * (Sum A) and
A8: for A being Subset of V st A is infinite holds
F2 . A = 0. V ; :: thesis: F1 = F2
for x being object st x in BOOL the carrier of V holds
F1 . x = F2 . x
proof
let x be object ; :: thesis: ( x in BOOL the carrier of V implies F1 . x = F2 . x )
assume x in BOOL the carrier of V ; :: thesis: F1 . x = F2 . x
then reconsider A = x as non empty Subset of V by ZFMISC_1:56;
per cases ( A is finite or A is infinite ) ;
suppose A is finite ; :: thesis: F1 . x = F2 . x
then reconsider A1 = A as non empty finite Subset of V ;
thus F1 . x = (1 / (card A1)) * (Sum A1) by A5
.= F2 . x by A7 ; :: thesis: verum
end;
suppose A9: A is infinite ; :: thesis: F1 . x = F2 . x
hence F1 . x = 0. V by A6
.= F2 . x by A8, A9 ;
:: thesis: verum
end;
end;
end;
hence F1 = F2 by FUNCT_2:12; :: thesis: verum