let Omega be non empty set ; :: thesis: for Sigma being SigmaField of Omega

for P being Probability of Sigma

for FSeq being FinSequence of Sigma holds dom (P * FSeq) = dom FSeq

let Sigma be SigmaField of Omega; :: thesis: for P being Probability of Sigma

for FSeq being FinSequence of Sigma holds dom (P * FSeq) = dom FSeq

let P be Probability of Sigma; :: thesis: for FSeq being FinSequence of Sigma holds dom (P * FSeq) = dom FSeq

let FSeq be FinSequence of Sigma; :: thesis: dom (P * FSeq) = dom FSeq

for x being object holds

( x in dom (P * FSeq) iff x in dom FSeq )

for P being Probability of Sigma

for FSeq being FinSequence of Sigma holds dom (P * FSeq) = dom FSeq

let Sigma be SigmaField of Omega; :: thesis: for P being Probability of Sigma

for FSeq being FinSequence of Sigma holds dom (P * FSeq) = dom FSeq

let P be Probability of Sigma; :: thesis: for FSeq being FinSequence of Sigma holds dom (P * FSeq) = dom FSeq

let FSeq be FinSequence of Sigma; :: thesis: dom (P * FSeq) = dom FSeq

for x being object holds

( x in dom (P * FSeq) iff x in dom FSeq )

proof

hence
dom (P * FSeq) = dom FSeq
by TARSKI:2; :: thesis: verum
let x be object ; :: thesis: ( x in dom (P * FSeq) iff x in dom FSeq )

thus ( x in dom (P * FSeq) implies x in dom FSeq ) by FUNCT_1:11; :: thesis: ( x in dom FSeq implies x in dom (P * FSeq) )

assume A1: x in dom FSeq ; :: thesis: x in dom (P * FSeq)

then reconsider k = x as Element of NAT ;

FSeq . k in Sigma ;

then FSeq . k in dom P by FUNCT_2:def 1;

hence x in dom (P * FSeq) by A1, FUNCT_1:11; :: thesis: verum

end;thus ( x in dom (P * FSeq) implies x in dom FSeq ) by FUNCT_1:11; :: thesis: ( x in dom FSeq implies x in dom (P * FSeq) )

assume A1: x in dom FSeq ; :: thesis: x in dom (P * FSeq)

then reconsider k = x as Element of NAT ;

FSeq . k in Sigma ;

then FSeq . k in dom P by FUNCT_2:def 1;

hence x in dom (P * FSeq) by A1, FUNCT_1:11; :: thesis: verum