deffunc H₁( object ) -> set = (Den (o,A)) . (a +* (i,$1));
ex f being Function st
( dom f = the Sorts of A . ((the_arity_of o) /. i) & ( for x being object st x in the Sorts of A . ((the_arity_of o) /. i) holds
f . x = H₁(x) ) ) from FUNCT_1:sch 3();
hence ex b₁ being Function st
( dom b₁ = the Sorts of A . ((the_arity_of o) /. i) & ( for x being object st x in the Sorts of A . ((the_arity_of o) /. i) holds
b₁ . x = (Den (o,A)) . (a +* (i,x)) ) ) ; :: thesis: verum