:: deftheorem Def66 defines at ABCMIZ_1:def 66 :
for C being initialized ConstructorSignature
for f, g, b₄ being valuation of C holds
( b₄ = f at g iff ( dom b₄ = (dom f) \/ (dom g) & ( for x being variable st x in dom b₄ holds
b₄ . x = ((x -term C) at f) at g ) ) );