let n be Ordinal; :: thesis: for T being connected TermOrder of n
for L being non trivial right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed 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 associative commutative well-unital distributive add-associative right_zeroed 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 associative commutative well-unital distributive add-associative right_zeroed 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 consider b being bag of such that
A1: f reduces_to g,p,b,T by Def6;
thus ( f <> 0_ n,L & p <> 0_ n,L ) by A1, Def5; :: thesis: verum