now

let n be Nat; :: thesis: (Complement S) . n in Si
reconsider n1 = n as Element of NAT by ORDINAL1:def 13;
A1: (Complement S) . n = (S . n1) ` by PROB_1:def 4;
( S . n in rng S & rng S c= Si ) by NAT_1:52, RELAT_1:def 19;
then (Complement S) . n is Event of Si by A1, PROB_1:50;
hence (Complement S) . n in Si ; :: thesis: verum

end;

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