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

then
rng (Complement ASeq) c= Sigma
by NAT_1:52;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;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

hence Complement ASeq is Sigma -valued by RELAT_1:def 19; :: thesis: verum