reconsider l1 = leq (t1,t2), l2 = leq (t2,t1) as INT-Expression of A,f ;
A5: dom (l1 (#) l2) = Funcs (X,INT) by FUNCT_2:def 1;
A6: dom (eq (t1,t2)) = Funcs (X,INT) by FUNCT_2:def 1;

now :: thesis: for a being object st a in Funcs (X,INT) holds
(eq (t1,t2)) . a = (l1 (#) l2) . a

let a be object ; :: thesis: ( a in Funcs (X,INT) implies (eq (t1,t2)) . a = (l1 (#) l2) . a )
assume a in Funcs (X,INT) ; :: thesis: (eq (t1,t2)) . a = (l1 (#) l2) . a
then reconsider s = a as Element of Funcs (X,INT) ;
A7: ( t1 . s = t2 . s or t1 . s < t2 . s or t2 . s < t1 . s ) by XXREAL_0:1;
A8: l2 . s = IFGT ((t2 . s),(t1 . s),0,1) by Def31;
A9: (l1 (#) l2) . s = (l1 . s) * (l2 . s) by A5, VALUED_1:def 4;
A10: l1 . s = IFGT ((t1 . s),(t2 . s),0,1) by Def31;
(eq (t1,t2)) . s = IFEQ ((t1 . s),(t2 . s),1,0) by A6, Def7;
then ( ( (eq (t1,t2)) . s = 1 & l1 . s = 1 & l2 . s = 1 ) or ( (eq (t1,t2)) . s = 0 & l1 . s = 0 & l2 . s = 1 ) or ( (eq (t1,t2)) . s = 0 & l1 . s = 1 & l2 . s = 0 ) ) by A8, A10, A7, FUNCOP_1:def 8, XXREAL_0:def 11;
hence (eq (t1,t2)) . a = (l1 (#) l2) . a by A9; :: thesis: verum

end;

hence eq (t1,t2) is INT-Expression of A,f by A6, A5, FUNCT_1:2; :: thesis: verum