theorem :: ABCMIZ_1:143

for C being initialized ConstructorSignature
for f, g being one-to-one irrelevant valuation of C st ( for x, y being variable st x in dom f & f . x = y -term C holds
( y in dom g & g . y = x -term C ) ) holds
for e being expression of C st variables_in e c= dom f holds
(e at f) at g = e