let X be set ; :: thesis: for A being Subset of X ex F being sequence of (bool X) st rng F = {A}
let A be Subset of X; :: thesis: ex F being sequence of (bool X) st rng F = {A}
take NAT --> A ; :: thesis: rng (NAT --> A) = {A}
thus rng (NAT --> A) = {A} by FUNCOP_1:8; :: thesis: verum