consider F1 being FinSequence of bool X such that
A1: for k being Nat st k in dom F1 holds
F1 . k = X by Th52;
take F1 ; :: thesis: for k being Nat st k in dom F1 holds
F1 . k in Si
for k being Nat st k in dom F1 holds
F1 . k in Si

proof

let k be Nat; :: thesis: ( k in dom F1 implies F1 . k in Si )
assume k in dom F1 ; :: thesis: F1 . k in Si
then F1 . k = X by A1;
hence F1 . k in Si by PROB_1:43; :: thesis: verum

end;

hence for k being Nat st k in dom F1 holds
F1 . k in Si ; :: thesis: verum