for V, S being non empty finite set
for G being random_variable of Trivial-SigmaField V, Trivial-SigmaField S
for y being set st y in Trivial-SigmaField S holds
(probability (G,(Trivial-Probability V))) . y = (card (G " y)) / (card V)