theorem :: FINANCE3:22

for MySigmaField, MySet being set
for A1 being SetSequence of MySet st MySet = {1,2,3,4} & rng A1 c= MySigmaField & MySigmaField = {{},{1,2,3,4}} holds
for k1, k2 being Nat holds (A1 . k1) /\ (A1 . k2) in MySigmaField