let n be Ordinal; :: thesis: for T being connected admissible TermOrder of n
for L being non trivial right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative 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 well-unital distributive Abelian add-associative right_zeroed associative commutative 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 well-unital distributive Abelian add-associative right_zeroed associative commutative 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₁[ Nat] means for f being Polynomial of n,L st card (Support f) = $1 holds
PolyRedRel ({g},T) reduces f *' g, 0_ (n,L);
A1: ex n being Element of NAT st card (Support f) = n ;

A2: now :: thesis: for k being Nat st S₁[k] holds
S₁[k + 1]

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

now :: thesis: for f being Polynomial of n,L st card (Support f) = k + 1 holds
PolyRedRel ({g},T) reduces f *' g, 0_ (n,L)

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

now :: thesis: not f = 0_ (n,L)

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 1;
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 A5: PolyRedRel ({g},T) reduces f *' g,(Red (f,T)) *' g by REWRITE1:15;
f1 <> 0_ (n,L) by POLYNOM7:def 1;
then Support f <> {} by POLYNOM7:1;
then HT (f,T) in Support f by TERMORD:def 6;
then for u being object st u in {(HT (f,T))} holds
u in Support f by TARSKI:def 1;
then A6: {(HT (f,T))} c= Support f ;
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 A6, CARD_2:44
.= (k + 1) - 1 by A4, CARD_1:30
.= k + 0 ;
then PolyRedRel ({g},T) reduces (Red (f,T)) *' g, 0_ (n,L) by A3;
hence PolyRedRel ({g},T) reduces f *' g, 0_ (n,L) by A5, REWRITE1:16; :: thesis: verum

end;

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

end;

now :: thesis: for f being Polynomial of n,L st card (Support f) = 0 holds
PolyRedRel ({g},T) reduces f *' g, 0_ (n,L)

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 = {} ;
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:12; :: thesis: verum

end;

then A7: S₁[ 0 ] ;
for k being Nat holds S₁[k] from NAT_1:sch 2(A7, A2);
hence PolyRedRel ({g},T) reduces f *' g, 0_ (n,L) by A1; :: thesis: verum