let ti be INT-Expression of A,f; ( ti = eq (t1,t2) iff for s being Element of Funcs (X,INT) holds ti . s = IFEQ ((t1 . s),(t2 . s),1,0) )
A1:
dom t1 = Funcs (X,INT)
by FUNCT_2:def 1;
A2:
dom t2 = Funcs (X,INT)
by FUNCT_2:def 1;
A3:
dom (eq (t1,t2)) = (dom t1) /\ (dom t2)
by Def7;
hence
( ti = eq (t1,t2) implies for s being Element of Funcs (X,INT) holds ti . s = IFEQ ((t1 . s),(t2 . s),1,0) )
by A1, A2, Def7; ( ( for s being Element of Funcs (X,INT) holds ti . s = IFEQ ((t1 . s),(t2 . s),1,0) ) implies ti = eq (t1,t2) )
A4:
dom ti = Funcs (X,INT)
by FUNCT_2:def 1;
assume
for s being Element of Funcs (X,INT) holds ti . s = IFEQ ((t1 . s),(t2 . s),1,0)
; ti = eq (t1,t2)
then
for s being object st s in Funcs (X,INT) holds
ti . s = IFEQ ((t1 . s),(t2 . s),1,0)
;
hence
ti = eq (t1,t2)
by A3, A1, A2, A4, Def7; verum