now

let n be Nat; :: thesis: ( n in dom (Complement F) implies (Complement F) . n in S )
assume n in dom (Complement F) ; :: thesis: (Complement F) . n in S
then (Complement F) . n = (F . n) ` by Def8;
then (Complement F) . n is Event of S by PROB_1:50;
hence (Complement F) . n in S ; :: thesis: verum

end;

hence Complement F is FinSequence of S by Def10; :: thesis: verum