let n be Ordinal; for T being connected TermOrder of n
for L being non trivial right_complementable Abelian add-associative right_zeroed doubleLoopStr
for p being non-zero Polynomial of n,L holds
( Up (p,T,1) = HM (p,T) & Low (p,T,1) = Red (p,T) )
let T be connected TermOrder of n; for L being non trivial right_complementable Abelian add-associative right_zeroed doubleLoopStr
for p being non-zero Polynomial of n,L holds
( Up (p,T,1) = HM (p,T) & Low (p,T,1) = Red (p,T) )
let L be non trivial right_complementable Abelian add-associative right_zeroed doubleLoopStr ; for p being non-zero Polynomial of n,L holds
( Up (p,T,1) = HM (p,T) & Low (p,T,1) = Red (p,T) )
let p be non-zero Polynomial of n,L; ( Up (p,T,1) = HM (p,T) & Low (p,T,1) = Red (p,T) )
set u = Up (p,T,1);
set l = Low (p,T,1);
then
Support (Up (p,T,1)) = Upper_Support (p,T,1)
by Lm3;
then
card (Support (Up (p,T,1))) = 1
by A1, Def2;
then consider x being object such that
A2:
Support (Up (p,T,1)) = {x}
by CARD_2:42;
HT (p,T) in {x}
by A1, A2, Th30;
then A3:
Support (Up (p,T,1)) = {(HT (p,T))}
by A2, TARSKI:def 1;
HM (p,T) <> 0_ (n,L)
by POLYNOM7:def 1;
then
Support (HM (p,T)) <> {}
by POLYNOM7:1;
then A4:
Support (Up (p,T,1)) = Support (HM (p,T))
by A3, TERMORD:21;
A5:
now for x being object st x in dom (HM (p,T)) holds
(HM (p,T)) . x = (Up (p,T,1)) . xlet x be
object ;
( x in dom (HM (p,T)) implies (HM (p,T)) . x = (Up (p,T,1)) . x )assume
x in dom (HM (p,T))
;
(HM (p,T)) . x = (Up (p,T,1)) . xthen reconsider x9 =
x as
Element of
Bags n ;
hence
(HM (p,T)) . x = (Up (p,T,1)) . x
;
verum end;
dom (HM (p,T)) =
Bags n
by FUNCT_2:def 1
.=
dom (Up (p,T,1))
by FUNCT_2:def 1
;
hence
HM (p,T) = Up (p,T,1)
by A5, FUNCT_1:2; Low (p,T,1) = Red (p,T)
then A8:
(HM (p,T)) + (Low (p,T,1)) = p
by A1, Th33;
thus Red (p,T) =
p - (HM (p,T))
by TERMORD:def 9
.=
((Low (p,T,1)) + (HM (p,T))) + (- (HM (p,T)))
by A8, POLYNOM1:def 7
.=
(Low (p,T,1)) + ((HM (p,T)) + (- (HM (p,T))))
by POLYNOM1:21
.=
(Low (p,T,1)) + (0_ (n,L))
by POLYRED:3
.=
Low (p,T,1)
by POLYRED:2
; verum