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:81 ;
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