let t be expression of C; :: thesis: ex f being valuation of C st f unifies t,t
set f = the valuation of C;
take the valuation of C ; :: thesis: the valuation of C unifies t,t
thus t at the valuation of C = t at the valuation of C ; :: according to ABCMIZ_A:def 24 :: thesis: verum