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 :: thesis: for b being bag of n st b <> EmptyBag n holds
p . b = 0. L

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

end;

A4: now :: thesis: for b being object st b in dom (Red (p,T)) holds
(Red (p,T)) . b = (0_ (n,L)) . b

let b be object ; :: 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 7
.= (p . b9) + ((- (HM (p,T))) . b9) by POLYNOM1:15
.= (p . b9) + (- ((HM (p,T)) . b9)) by POLYNOM1:17 ;

now :: thesis: ( ( b9 = EmptyBag n & (Red (p,T)) . b9 = (0_ (n,L)) . b9 ) or ( b9 <> EmptyBag n & (Red (p,T)) . b9 = (0_ (n,L)) . b9 ) )

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:5
.= (0_ (n,L)) . b9 by POLYNOM1:22 ;
:: 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:5
.= (0_ (n,L)) . b9 by POLYNOM1:22 ;
:: 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:2; :: thesis: verum