now :: thesis: for n being Nat holds (Complement ASeq) . n in Sigma

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

end;

then rng (Complement ASeq) c= Sigma by NAT_1:52;
hence Complement ASeq is Sigma -valued by RELAT_1:def 19; :: thesis: verum