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 )

proof

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;

hence dom (P * FSeq) = dom FSeq by TARSKI:2; :: thesis: verum