deffunc H₁( Element of V) -> Element of the carrier of V = r * $1;
defpred S₁[ set ] means $1 in M;
{ H₁(v) where v is Element of V : S₁[v] } is Subset of V from DOMAIN_1:sch 8();
hence { (r * v) where v is Element of V : v in M } is Subset of V ; :: thesis: verum