let MySigmaField, MySet be set ; :: thesis: 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
let A1 be SetSequence of MySet; :: thesis: ( MySet = {1,2,3,4} & rng A1 c= MySigmaField & MySigmaField = {{},{1,2,3,4}} implies for k1, k2 being Nat holds (A1 . k1) /\ (A1 . k2) in MySigmaField )
assume A0: ( MySet = {1,2,3,4} & rng A1 c= MySigmaField & MySigmaField = {{},{1,2,3,4}} ) ; :: thesis: for k1, k2 being Nat holds (A1 . k1) /\ (A1 . k2) in MySigmaField
let k1, k2 be Nat; :: thesis: (A1 . k1) /\ (A1 . k2) in MySigmaField
D1: dom A1 = NAT by FUNCT_2:def 1;
then k1 in dom A1 by ORDINAL1:def 12;
then B1: A1 . k1 in MySigmaField by FUNCT_1:3, A0;
k2 in dom A1 by D1, ORDINAL1:def 12;
then B2: A1 . k2 in MySigmaField by FUNCT_1:3, A0;
(A1 . k1) /\ (A1 . k2) in MySigmaField

proof

( ( A1 . k1 = {} or A1 . k1 = {1,2,3,4} ) & ( A1 . k2 = {} or A1 . k2 = {1,2,3,4} ) ) by B2, B1, A0, TARSKI:def 2;
hence (A1 . k1) /\ (A1 . k2) in MySigmaField by A0, TARSKI:def 2; :: thesis: verum

end;

hence (A1 . k1) /\ (A1 . k2) in MySigmaField ; :: thesis: verum