:: deftheorem Def6 defines ^^^ FOMODEL2:def 6 :
for f being Function-yielding Function
for g, b₃ being Function holds
( b₃ = ^^^g,f__ iff ( dom b₃ = dom f & ( for x being set st x in dom f holds
b₃ . x = g * (f . x) ) ) );