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