let t be expression of C; :: thesis: ex f being valuation of C st t = t at f
consider f being empty valuation of C;
take f ; :: thesis: t = t at f
thus t at f = t by ABCMIZ_1:139; :: thesis: verum