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 for a being object st a in Funcs (X,INT) holds
(eq (t1,t2)) . a = (l1 (#) l2) . alet a be
object ;
( a in Funcs (X,INT) implies (eq (t1,t2)) . a = (l1 (#) l2) . a )assume
a in Funcs (
X,
INT)
;
(eq (t1,t2)) . a = (l1 (#) l2) . athen 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;
verum end;
hence
eq (t1,t2) is INT-Expression of A,f
by A6, A5, FUNCT_1:2; verum