:: deftheorem defines ^^^ FOMODEL0:def 4 :
for f being Function-yielding Function
for g, b₃ being Function holds
( b₃ = ^^^f,g__ iff ( dom b₃ = (dom f) /\ (dom g) & ( for x being set st x in dom b₃ holds
b₃ . x = (f . x) . (g . x) ) ) );