let n be Ordinal; for T being connected TermOrder of n
for L being non trivial ZeroStr
for p being non-zero Polynomial of n,L holds PosetMax (Support (p,T)) = HT (p,T)
let T be connected TermOrder of n; for L being non trivial ZeroStr
for p being non-zero Polynomial of n,L holds PosetMax (Support (p,T)) = HT (p,T)
let L be non trivial ZeroStr ; for p being non-zero Polynomial of n,L holds PosetMax (Support (p,T)) = HT (p,T)
let p be non-zero Polynomial of n,L; PosetMax (Support (p,T)) = HT (p,T)
set htp = HT (p,T);
set R = RelStr(# (Bags n),T #);
set sp = Support (p,T);
p <> 0_ (n,L)
by POLYNOM7:def 1;
then
Support p <> {}
by POLYNOM7:1;
then A1:
HT (p,T) in Support p
by TERMORD:def 6;
now for y being set holds
( not y in Support (p,T) or not y <> HT (p,T) or not [(HT (p,T)),y] in the InternalRel of RelStr(# (Bags n),T #) )assume
ex
y being
set st
(
y in Support (
p,
T) &
y <> HT (
p,
T) &
[(HT (p,T)),y] in the
InternalRel of
RelStr(#
(Bags n),
T #) )
;
contradictionthen consider y being
set such that A2:
y in Support (
p,
T)
and A3:
y <> HT (
p,
T)
and A4:
[(HT (p,T)),y] in the
InternalRel of
RelStr(#
(Bags n),
T #)
;
y is
Element of
Bags n
by A2;
then reconsider y9 =
y as
bag of
n ;
(
y9 <= HT (
p,
T),
T &
HT (
p,
T)
<= y9,
T )
by A2, A4, TERMORD:def 2, TERMORD:def 6;
hence
contradiction
by A3, TERMORD:7;
verum end;
then
HT (p,T) is_maximal_wrt Support (p,T), the InternalRel of RelStr(# (Bags n),T #)
by A1, WAYBEL_4:def 23;
hence
PosetMax (Support (p,T)) = HT (p,T)
by A1, BAGORDER:def 13; verum