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 )
assume A1: HT p,T = EmptyBag n ; :: thesis: Red p,T = 0_ n,L

A2: now

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

end;

set red = Red p,T;
set e = 0_ n,L;
A4: dom (Red p,T) = Bags n by FUNCT_2:def 1
.= dom (0_ n,L) by FUNCT_2:def 1 ;

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 b' = b as Element of Bags n ;
A5: (Red p,T) . b' = (p - (HM p,T)) . b' by TERMORD:def 9
.= (p + (- (HM p,T))) . b' by POLYNOM1:def 23
.= (p . b') + ((- (HM p,T)) . b') by POLYNOM1:def 21
.= (p . b') + (- ((HM p,T) . b')) by POLYNOM1:def 22 ;

now

per cases ( b' = EmptyBag n or b' <> EmptyBag n ) ;

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

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

end;

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

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

end;

end;

end;

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

end;

hence Red p,T = 0_ n,L by A4, FUNCT_1:9; :: thesis: verum