let S be non empty set ; :: thesis: for F being non empty FinSequence of S holds F is random_variable of Trivial-SigmaField (Seg (len F)), Trivial-SigmaField S

let F be non empty FinSequence of S; :: thesis: F is random_variable of Trivial-SigmaField (Seg (len F)), Trivial-SigmaField S

reconsider n = len F as non empty Element of NAT ;

A1: dom F = Seg n by FINSEQ_1:def 3;

rng F c= S ;

hence F is random_variable of Trivial-SigmaField (Seg (len F)), Trivial-SigmaField S by Th15, A1, FUNCT_2:2; :: thesis: verum

let F be non empty FinSequence of S; :: thesis: F is random_variable of Trivial-SigmaField (Seg (len F)), Trivial-SigmaField S

reconsider n = len F as non empty Element of NAT ;

A1: dom F = Seg n by FINSEQ_1:def 3;

rng F c= S ;

hence F is random_variable of Trivial-SigmaField (Seg (len F)), Trivial-SigmaField S by Th15, A1, FUNCT_2:2; :: thesis: verum