let MySigmaField, MySet be 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
let A1 be SetSequence of MySet; ( 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}} )
; for k1, k2 being Nat holds (A1 . k1) /\ (A1 . k2) in MySigmaField
let k1, k2 be Nat; (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;
verum
end;
hence
(A1 . k1) /\ (A1 . k2) in MySigmaField
; verum