consider f being FinSequence of bool X such that
A1: for k being Nat st k in dom f holds
f . k = X by PROB_3:47;
take f ; :: thesis: for k being Nat st k in dom f holds
f . k in F

hereby :: thesis: verum

let k be Nat; :: thesis: ( k in dom f implies f . k in F )
assume k in dom f ; :: thesis: f . k in F
then f . k = X by A1;
hence f . k in F by PROB_1:5; :: thesis: verum

end;