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

let a be set ; :: 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:9; :: thesis: verum