let n be Ordinal; :: thesis: for T being connected TermOrder of n
for L being non trivial right_complementable add-associative right_zeroed addLoopStr holds Red ((0_ (n,L)),T) = 0_ (n,L)
let T be connected TermOrder of n; :: thesis: for L being non trivial right_complementable add-associative right_zeroed addLoopStr holds Red ((0_ (n,L)),T) = 0_ (n,L)
let L be non trivial right_complementable add-associative right_zeroed addLoopStr ; :: thesis: Red ((0_ (n,L)),T) = 0_ (n,L)
set e = 0_ (n,L);
set h = HM ((0_ (n,L)),T);
HC ((HM ((0_ (n,L)),T)),T) = HC ((0_ (n,L)),T) by TERMORD:27
.= (0_ (n,L)) . (HT ((0_ (n,L)),T)) by TERMORD:def 7
.= 0. L by POLYNOM1:22 ;
then HM ((0_ (n,L)),T) = 0_ (n,L) by TERMORD:17;
hence Red ((0_ (n,L)),T) = (0_ (n,L)) - (0_ (n,L)) by TERMORD:def 9
.= 0_ (n,L) by POLYRED:4 ;
:: thesis: verum