deffunc H₁( object ) -> object = [$1,(1. R)];
A1: for o1 being object st o1 in the carrier of R holds
H₁(o1) in Frac S by Lm16;
ex f being Function of R,(Frac S) st
for o2 being object st o2 in the carrier of R holds
f . o2 = H₁(o2) from FUNCT_2:sch 2(A1);
hence ex b₁ being Function of R,(Frac S) st
for o being object st o in the carrier of R holds
b₁ . o = [o,(1. R)] ; :: thesis: verum