let V, S be non empty finite set ; :: thesis: 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)
let G be random_variable of Trivial-SigmaField V, Trivial-SigmaField S; :: thesis: for y being set st y in Trivial-SigmaField S holds
(probability (G,(Trivial-Probability V))) . y = (card (G " y)) / (card V)

now :: thesis: for y being set st y in Trivial-SigmaField S holds
(probability (G,(Trivial-Probability V))) . y = (card (G " y)) / (card V)

let y be set ; :: thesis: ( y in Trivial-SigmaField S implies (probability (G,(Trivial-Probability V))) . y = (card (G " y)) / (card V) )
assume A1: y in Trivial-SigmaField S ; :: thesis: (probability (G,(Trivial-Probability V))) . y = (card (G " y)) / (card V)
thus (probability (G,(Trivial-Probability V))) . y = (Trivial-Probability V) . (G " y) by Th14, A1
.= prob (G " y) by RANDOM_1:def 1
.= (card (G " y)) / (card V) ; :: thesis: verum

end;

hence for y being set st y in Trivial-SigmaField S holds
(probability (G,(Trivial-Probability V))) . y = (card (G " y)) / (card V) ; :: thesis: verum