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

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

hence
F1 = F2
by FUNCT_2:12; :: thesis: verum
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;

end;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;