now

let n be Nat; :: thesis: (Complement ASeq) . n in Sigma
reconsider n1 = n as Element of NAT by ORDINAL1:def 13;
(Complement ASeq) . n1 = (ASeq . n1) ` by PROB_1:def 4;
then (Complement ASeq) . n1 is Event of Sigma by PROB_1:50;
hence (Complement ASeq) . n in Sigma ; :: thesis: verum

end;

then rng (Complement ASeq) c= Sigma by NAT_1:53;
hence Complement ASeq is SetSequence of by RELAT_1:def 19; :: thesis: verum