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

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