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;

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

hence
eq (t1,t2) is INT-Expression of A,f
by A6, A5, FUNCT_1:2; :: thesis: verum(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;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