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