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