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 being Polynomial of n,L holds f is_irreducible_wrt 0_ n,L,T
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 being Polynomial of n,L holds f is_irreducible_wrt 0_ n,L,T
let L be non trivial right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr ; :: thesis: for f being Polynomial of n,L holds f is_irreducible_wrt 0_ n,L,T
let f be Polynomial of n,L; :: thesis: f is_irreducible_wrt 0_ n,L,T
assume f is_reducible_wrt 0_ n,L,T ; :: thesis: contradiction
then consider g being Polynomial of n,L such that
A1: f reduces_to g, 0_ n,L,T by POLYRED:def 8;
consider b being bag of such that
A2: f reduces_to g, 0_ n,L,b,T by A1, POLYRED:def 6;
thus contradiction by A2, POLYRED:def 5; :: thesis: verum