defpred S₁[ set ] means verum;
deffunc H₁( Element of NAT ) -> Element of NAT = 2 * $1;
{ H₁(k) where k is Element of NAT : S₁[k] } is Subset of NAT from DOMAIN_1:sch 8();
hence { (2 * k) where k is Element of NAT : verum } is Subset of NAT ; :: thesis: verum