deffunc H₁( object ) -> Element of bool (Frac S) = Class ((EqRel S),((frac1 S) . $1));
A1: for o1 being object st o1 in the carrier of A holds
H₁(o1) in the carrier of (S ~ A) by Lm44;
ex g being Function of A,(S ~ A) st
for o2 being object st o2 in the carrier of A holds
g . o2 = H₁(o2) from FUNCT_2:sch 2(A1);
hence ex b₁ being Function of A,(S ~ A) st
for o being object st o in the carrier of A holds
b₁ . o = Class ((EqRel S),((frac1 S) . o)) ; :: thesis: verum