let n be Ordinal; :: thesis: for T being connected TermOrder of n
for L being non trivial right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr
for f, g, p being Polynomial of n,L st f reduces_to g,p,T holds
( f <> 0_ (n,L) & p <> 0_ (n,L) )
let T be connected TermOrder of n; :: thesis: for L being non trivial right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr
for f, g, p being Polynomial of n,L st f reduces_to g,p,T holds
( f <> 0_ (n,L) & p <> 0_ (n,L) )
let L be non trivial right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr ; :: thesis: for f, g, p being Polynomial of n,L st f reduces_to g,p,T holds
( f <> 0_ (n,L) & p <> 0_ (n,L) )
let f, g, p be Polynomial of n,L; :: thesis: ( f reduces_to g,p,T implies ( f <> 0_ (n,L) & p <> 0_ (n,L) ) )
assume f reduces_to g,p,T ; :: thesis: ( f <> 0_ (n,L) & p <> 0_ (n,L) )
then ex b being bag of n st f reduces_to g,p,b,T ;
hence ( f <> 0_ (n,L) & p <> 0_ (n,L) ) ; :: thesis: verum