let IT1, IT2 be TermOrder of n; :: thesis: ( ( for p, q being bag of holds
( [p,q] in IT1 iff ( ( 0 ,(i + 1) -cut p <> 0 ,(i + 1) -cut q & [(0 ,(i + 1) -cut p),(0 ,(i + 1) -cut q)] in o1 ) or ( 0 ,(i + 1) -cut p = 0 ,(i + 1) -cut q & [((i + 1),n -cut p),((i + 1),n -cut q)] in o2 ) ) ) ) & ( for p, q being bag of holds
( [p,q] in IT2 iff ( ( 0 ,(i + 1) -cut p <> 0 ,(i + 1) -cut q & [(0 ,(i + 1) -cut p),(0 ,(i + 1) -cut q)] in o1 ) or ( 0 ,(i + 1) -cut p = 0 ,(i + 1) -cut q & [((i + 1),n -cut p),((i + 1),n -cut q)] in o2 ) ) ) ) implies IT1 = IT2 )
assume that
A32:
for p, q being bag of holds
( [p,q] in IT1 iff ( ( 0 ,(i + 1) -cut p <> 0 ,(i + 1) -cut q & [(0 ,(i + 1) -cut p),(0 ,(i + 1) -cut q)] in o1 ) or ( 0 ,(i + 1) -cut p = 0 ,(i + 1) -cut q & [((i + 1),n -cut p),((i + 1),n -cut q)] in o2 ) ) )
and
A33:
for p, q being bag of holds
( [p,q] in IT2 iff ( ( 0 ,(i + 1) -cut p <> 0 ,(i + 1) -cut q & [(0 ,(i + 1) -cut p),(0 ,(i + 1) -cut q)] in o1 ) or ( 0 ,(i + 1) -cut p = 0 ,(i + 1) -cut q & [((i + 1),n -cut p),((i + 1),n -cut q)] in o2 ) ) )
; :: thesis: IT1 = IT2
now let a,
b be
set ;
:: thesis: ( ( [a,b] in IT1 implies [a,b] in IT2 ) & ( [a,b] in IT2 implies [a,b] in IT1 ) )hereby :: thesis: ( [a,b] in IT2 implies [a,b] in IT1 )
assume A34:
[a,b] in IT1
;
:: thesis: [a,b] in IT2then
(
a in dom IT1 &
b in rng IT1 )
by RELAT_1:20;
then reconsider p =
a,
q =
b as
bag of
by POLYNOM1:def 14;
( (
0 ,
(i + 1) -cut p <> 0 ,
(i + 1) -cut q &
[(0 ,(i + 1) -cut p),(0 ,(i + 1) -cut q)] in o1 ) or (
0 ,
(i + 1) -cut p = 0 ,
(i + 1) -cut q &
[((i + 1),n -cut p),((i + 1),n -cut q)] in o2 ) )
by A32, A34;
hence
[a,b] in IT2
by A33;
:: thesis: verum
end; assume A35:
[a,b] in IT2
;
:: thesis: [a,b] in IT1then
(
a in dom IT2 &
b in rng IT2 )
by RELAT_1:20;
then reconsider p =
a,
q =
b as
bag of
by POLYNOM1:def 14;
( (
0 ,
(i + 1) -cut p <> 0 ,
(i + 1) -cut q &
[(0 ,(i + 1) -cut p),(0 ,(i + 1) -cut q)] in o1 ) or (
0 ,
(i + 1) -cut p = 0 ,
(i + 1) -cut q &
[((i + 1),n -cut p),((i + 1),n -cut q)] in o2 ) )
by A33, A35;
hence
[a,b] in IT1
by A32;
:: thesis: verum end;
hence
IT1 = IT2
by RELAT_1:def 2; :: thesis: verum