for D being non empty set holds { d where d is Element of D : P₁[d] } is Subset of D from DOMAIN_1:sch 1();
hence { d where d is Element of F₁() : P₁[d] } is Subset of F₁() ; :: thesis: verum