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)

(probability (G,(Trivial-Probability V))) . y = (card (G " y)) / (card V) ; :: thesis: verum

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)

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

(probability (G,(Trivial-Probability V))) . y = (card (G " y)) / (card V) ; :: thesis: verum