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