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