A3: now

let k be Nat; :: thesis:
assume A4: 1 <= k ; :: thesis:
thus ( S₁[k] implies S₁[k + 1] ) :: thesis:

assume A5: S₁[k] ; :: thesis:

let f, g be Polynomial of n,L; :: thesis:
assume PolyRedRel P,T reduces f,g ; :: thesis:
let p be RedSequence of PolyRedRel P,T; :: thesis:
assume A6: ( p . 1 = f & p . (len p) = g & len p = k + 1 ) ; :: thesis:
then A7: dom p = Seg (k + 1) by FINSEQ_1:def 3;
A8: k <= k + 1 by NAT_1:11;
then A9: k in dom p by A4, A7, FINSEQ_1:3;
k + 1 in dom p by A7, FINSEQ_1:6;
then A10: [(p . k),(p . (k + 1))] in PolyRedRel P,T by A9, REWRITE1:def 2;
set q = p | (Seg k);
reconsider q = p | (Seg k) as FinSequence by FINSEQ_1:19;
set h = q . (len q);
A11: len q = k by A6, A8, FINSEQ_1:21;
A12: dom q = Seg k by A6, A8, FINSEQ_1:21;
then k in dom q by A4, FINSEQ_1:3;
then A13: [(q . (len q)),g] in PolyRedRel P,T by A6, A10, A11, FUNCT_1:68;
then consider h', g' being set such that
A14: ( [(q . (len q)),g] = [h',g'] & h' in the carrier of (Polynom-Ring n,L) \ {(0_ n,L)} & g' in the carrier of (Polynom-Ring n,L) ) by RELSET_1:6;
A15: q . (len q) = [h',g'] `1 by A14, MCART_1:def 1
.= h' by MCART_1:def 1 ;
not h' in {(0_ n,L)} by A14, XBOOLE_0:def 5;
then h' <> 0_ n,L by TARSKI:def 1;
then reconsider h = q . (len q) as non-zero Polynomial of n,L by A14, A15, POLYNOM1:def 27, POLYNOM7:def 2;

let i be Element of NAT ; :: thesis:
assume A16: ( i in dom q & i + 1 in dom q ) ; :: thesis:
then A17: ( 1 <= i & i <= k & 1 <= i + 1 & i + 1 <= k ) by A12, FINSEQ_1:3;
then A18: ( i <= k + 1 & i + 1 <= k + 1 ) by A8, XXREAL_0:2;
then A19: i in dom p by A7, A17, FINSEQ_1:3;
i + 1 in dom p by A7, A17, A18, FINSEQ_1:3;
then A20: [(p . i),(p . (i + 1))] in PolyRedRel P,T by A19, REWRITE1:def 2;
p . i = q . i by A16, FUNCT_1:68;
hence [(q . i),(q . (i + 1))] in PolyRedRel P,T by A16, A20, FUNCT_1:68; :: thesis:

end;

then reconsider q = q as RedSequence of PolyRedRel P,T by A4, A11, REWRITE1:def 2;
1 in dom q by A4, A12, FINSEQ_1:3;
then A21: q . 1 = f by A6, FUNCT_1:68;
then PolyRedRel P,T reduces f,h by REWRITE1:def 3;
then A22: h <= f,T by A5, A11, A21;
h reduces_to g,P,T by A13, Def13;
then consider r being Polynomial of n,L such that
A23: ( r in P & h reduces_to g,r,T ) by Def7;
reconsider h = h as non-zero Polynomial of n,L ;
g < h,T by A23, Th43;
then g <= h,T by Def3;
hence g <= f,T by A22, Th27; :: thesis:

end;

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

end;

A24: for k being Nat st 1 <= k holds
S₁[k] from NAT_1:sch 8(A2, A3);
consider p being RedSequence of PolyRedRel P,T such that
A25: ( p . 1 = f & p . (len p) = g ) by A1, REWRITE1:def 3;
consider k being Nat such that
A26: len p = k ;
k > 0 by A26;
then 1 <= k by NAT_1:14;
hence A27: g <= f,T by A1, A24, A25, A26; :: thesis:

assume g <> 0_ n,L ; :: thesis:
then Support g <> {} by POLYNOM7:1;
then A28: HT g,T in Support g by TERMORD:def 6;
assume A29: not HT g,T <= HT f,T,T ; :: thesis:

per cases ;

case HT f,T = HT g,T ; :: thesis:

hence contradiction by A29, TERMORD:6; :: thesis:

end;

case A30: HT f,T <> HT g,T ; :: thesis:

A31: T is_connected_in field T by RELAT_2:def 14;
( HT f,T <= HT f,T,T & HT g,T <= HT g,T,T ) by TERMORD:6;
then ( [(HT f,T),(HT f,T)] in T & [(HT g,T),(HT g,T)] in T ) by TERMORD:def 2;
then ( HT f,T in field T & HT g,T in field T ) by RELAT_1:30;
then ( [(HT f,T),(HT g,T)] in T or [(HT g,T),(HT f,T)] in T ) by A30, A31, RELAT_2:def 6;
then HT f,T <= HT g,T,T by A29, TERMORD:def 2;
then A32: HT f,T < HT g,T,T by A30, TERMORD:def 3;
then f < g,T by Lm15;
then f <= g,T by Def3;
then Support f = Support g by A27, Th26;
then HT g,T <= HT f,T,T by A28, TERMORD:def 6;
hence contradiction by A32, TERMORD:5; :: thesis:

end;

hence contradiction ; :: thesis:

end;

hence ( g = 0_ n,L or HT g,T <= HT f,T,T ) ; :: thesis: