let n be Ordinal; :: thesis: for T being connected admissible TermOrder of n
for L being non trivial right_complementable add-associative right_zeroed addLoopStr
for p being Polynomial of n,L st HT p,T = EmptyBag n holds
Red p,T = 0_ n,L
let T be connected admissible TermOrder of n; :: thesis: for L being non trivial right_complementable add-associative right_zeroed addLoopStr
for p being Polynomial of n,L st HT p,T = EmptyBag n holds
Red p,T = 0_ n,L
let L be non trivial right_complementable add-associative right_zeroed addLoopStr ; :: thesis: for p being Polynomial of n,L st HT p,T = EmptyBag n holds
Red p,T = 0_ n,L
let p be Polynomial of n,L; :: thesis: ( HT p,T = EmptyBag n implies Red p,T = 0_ n,L )
set red = Red p,T;
set e = 0_ n,L;
assume A1: HT p,T = EmptyBag n ; :: thesis: Red p,T = 0_ n,L

A2: now

let b be bag of n; :: thesis: ( b <> EmptyBag n implies p . b = 0. L )
A3: [(EmptyBag n),b] in T by BAGORDER:def 7;
assume b <> EmptyBag n ; :: thesis: p . b = 0. L
hence p . b = 0. L by A1, A3, Lm13; :: thesis: verum

end;

A4: now

let b be set ; :: thesis: ( b in dom (Red p,T) implies (Red p,T) . b = (0_ n,L) . b )
assume b in dom (Red p,T) ; :: thesis: (Red p,T) . b = (0_ n,L) . b
then reconsider b9 = b as Element of Bags n ;
A5: (Red p,T) . b9 = (p - (HM p,T)) . b9 by TERMORD:def 9
.= (p + (- (HM p,T))) . b9 by POLYNOM1:def 23
.= (p . b9) + ((- (HM p,T)) . b9) by POLYNOM1:def 21
.= (p . b9) + (- ((HM p,T) . b9)) by POLYNOM1:def 22 ;

now

per cases ( b9 = EmptyBag n or b9 <> EmptyBag n ) ;

case b9 = EmptyBag n ; :: thesis: (Red p,T) . b9 = (0_ n,L) . b9

hence (Red p,T) . b9 = (p . (HT p,T)) + (- (p . (HT p,T))) by A1, A5, TERMORD:18
.= 0. L by RLVECT_1:16
.= (0_ n,L) . b9 by POLYNOM1:81 ;
:: thesis: verum

end;

case A6: b9 <> EmptyBag n ; :: thesis: (Red p,T) . b9 = (0_ n,L) . b9

hence (Red p,T) . b9 = (0. L) + (- ((HM p,T) . b9)) by A2, A5
.= (0. L) + (- (0. L)) by A1, A6, TERMORD:19
.= 0. L by RLVECT_1:16
.= (0_ n,L) . b9 by POLYNOM1:81 ;
:: thesis: verum

end;

end;

end;

hence (Red p,T) . b = (0_ n,L) . b ; :: thesis: verum

end;

dom (Red p,T) = Bags n by FUNCT_2:def 1
.= dom (0_ n,L) by FUNCT_2:def 1 ;
hence Red p,T = 0_ n,L by A4, FUNCT_1:9; :: thesis: verum