let n be Ordinal; :: thesis: for T being connected admissible TermOrder of n
for L being non trivial right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for f, g being non-zero Polynomial of n,L holds PolyRedRel {g},T reduces f *' g, 0_ n,L
let T be connected admissible TermOrder of n; :: thesis: for L being non trivial right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for f, g being non-zero Polynomial of n,L holds PolyRedRel {g},T reduces f *' g, 0_ n,L
let L be non trivial right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; :: thesis: for f, g being non-zero Polynomial of n,L holds PolyRedRel {g},T reduces f *' g, 0_ n,L
let f, g be non-zero Polynomial of n,L; :: thesis: PolyRedRel {g},T reduces f *' g, 0_ n,L
defpred S₁[ Element of NAT ] means for f being Polynomial of n,L st card (Support f) = $1 holds
PolyRedRel {g},T reduces f *' g, 0_ n,L;

now

let f be Polynomial of n,L; :: thesis: ( card (Support f) = 0 implies PolyRedRel {g},T reduces f *' g, 0_ n,L )
assume card (Support f) = 0 ; :: thesis: PolyRedRel {g},T reduces f *' g, 0_ n,L
then Support f, 0 are_equipotent by CARD_1:def 5;
then Support f = {} by CARD_1:46;
then f = 0_ n,L by POLYNOM7:1;
then f *' g = 0_ n,L by POLYRED:5;
hence PolyRedRel {g},T reduces f *' g, 0_ n,L by REWRITE1:13; :: thesis: verum

end;

then A1: S₁[ 0 ] ;

A2: now

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A3: S₁[k] ; :: thesis: S₁[k + 1]

now

let f be Polynomial of n,L; :: thesis: ( card (Support f) = k + 1 implies PolyRedRel {g},T reduces f *' g, 0_ n,L )
assume A4: card (Support f) = k + 1 ; :: thesis: PolyRedRel {g},T reduces f *' g, 0_ n,L

now

assume f = 0_ n,L ; :: thesis: contradiction
then Support f = {} by POLYNOM7:1;
hence contradiction by A4; :: thesis: verum

end;

then reconsider f1 = f as non-zero Polynomial of n,L by POLYNOM7:def 2;
set rf = Red f,T;
f1 <> 0_ n,L by POLYNOM7:def 2;
then Support f <> {} by POLYNOM7:1;
then HT f,T in Support f by TERMORD:def 6;
then for u being set st u in {(HT f,T)} holds
u in Support f by TARSKI:def 1;
then A5: {(HT f,T)} c= Support f by TARSKI:def 3;
Support (Red f,T) = (Support f) \ {(HT f,T)} by TERMORD:36;
then card (Support (Red f,T)) = (card (Support f)) - (card {(HT f,T)}) by A5, CARD_2:63
.= (k + 1) - 1 by A4, CARD_1:50
.= k + 0 ;
then A6: PolyRedRel {g},T reduces (Red f,T) *' g, 0_ n,L by A3;
f1 *' g reduces_to (Red f,T) *' g,{g},T by Th47;
then [(f1 *' g),((Red f,T) *' g)] in PolyRedRel {g},T by POLYRED:def 13;
then PolyRedRel {g},T reduces f *' g,(Red f,T) *' g by REWRITE1:16;
hence PolyRedRel {g},T reduces f *' g, 0_ n,L by A6, REWRITE1:17; :: thesis: verum

end;

hence S₁[k + 1] ; :: thesis: verum

end;

A7: for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A1, A2);
consider n being Element of NAT such that
A8: card (Support f) = n ;
thus PolyRedRel {g},T reduces f *' g, 0_ n,L by A7, A8; :: thesis: verum