let F be Field; :: thesis: for i being Element of NAT
for m being Ordinal st m in card (nonConstantPolys F) holds
(Poly (m,(anpoly ((1. F),1)))) *' (Poly (m,(anpoly ((1. F),i)))) = Poly (m,(anpoly ((1. F),(i + 1))))
let i be Element of NAT ; :: thesis: for m being Ordinal st m in card (nonConstantPolys F) holds
(Poly (m,(anpoly ((1. F),1)))) *' (Poly (m,(anpoly ((1. F),i)))) = Poly (m,(anpoly ((1. F),(i + 1))))
let m be Ordinal; :: thesis: ( m in card (nonConstantPolys F) implies (Poly (m,(anpoly ((1. F),1)))) *' (Poly (m,(anpoly ((1. F),i)))) = Poly (m,(anpoly ((1. F),(i + 1)))) )
set n = card (nonConstantPolys F);
set f = power (Polynom-Ring ((card (nonConstantPolys F)),F));
assume AS: m in card (nonConstantPolys F) ; :: thesis: (Poly (m,(anpoly ((1. F),1)))) *' (Poly (m,(anpoly ((1. F),i)))) = Poly (m,(anpoly ((1. F),(i + 1))))
for o being object st o in {m} holds
o in card (nonConstantPolys F) by AS, TARSKI:def 1;
then reconsider S = {m} as finite Subset of (card (nonConstantPolys F)) by TARSKI:def 3;
set p1 = Poly (m,(anpoly ((1. F),1)));
set p2 = Poly (m,(anpoly ((1. F),i)));
set q = Poly (m,(anpoly ((1. F),(i + 1))));

per cases ( i = 0 or i <> 0 ) ;

suppose U: i = 0 ; :: thesis: (Poly (m,(anpoly ((1. F),1)))) *' (Poly (m,(anpoly ((1. F),i)))) = Poly (m,(anpoly ((1. F),(i + 1))))

then anpoly ((1. F),i) = (1. F) | F by FIELD_1:7;
then Poly (m,(anpoly ((1. F),i))) = (1. F) | ((card (nonConstantPolys F)),F) by AS, XYZbb
.= 1_ ((card (nonConstantPolys F)),F) by POLYNOM7:20 ;
hence (Poly (m,(anpoly ((1. F),1)))) *' (Poly (m,(anpoly ((1. F),i)))) = Poly (m,(anpoly ((1. F),(i + 1)))) by U, POLYNOM1:29; :: thesis: verum

end;

suppose U: i <> 0 ; :: thesis: (Poly (m,(anpoly ((1. F),1)))) *' (Poly (m,(anpoly ((1. F),i)))) = Poly (m,(anpoly ((1. F),(i + 1))))

now :: thesis: for b being Element of Bags (card (nonConstantPolys F)) holds (Poly (m,(anpoly ((1. F),(i + 1))))) . b = ((Poly (m,(anpoly ((1. F),1)))) *' (Poly (m,(anpoly ((1. F),i))))) . b

let b be Element of Bags (card (nonConstantPolys F)); :: thesis: (Poly (m,(anpoly ((1. F),(i + 1))))) . b₁ = ((Poly (m,(anpoly ((1. F),1)))) *' (Poly (m,(anpoly ((1. F),i))))) . b₁
consider s being FinSequence of the carrier of F such that
A: ( ((Poly (m,(anpoly ((1. F),1)))) *' (Poly (m,(anpoly ((1. F),i))))) . b = Sum s & len s = len (decomp b) & ( for k being Element of NAT st k in dom s holds
ex b1, b2 being bag of card (nonConstantPolys F) st
( (decomp b) /. k = <*b1,b2*> & s /. k = ((Poly (m,(anpoly ((1. F),1)))) . b1) * ((Poly (m,(anpoly ((1. F),i)))) . b2) ) ) ) by POLYNOM1:def 10;
A1: dom s = Seg (len (decomp b)) by A, FINSEQ_1:def 3
.= dom (decomp b) by FINSEQ_1:def 3 ;
A2: m in {m} by TARSKI:def 1;

per cases ( support b = {} or support b = {m} or ( support b <> {} & support b <> {m} ) ) ;

suppose support b = {} ; :: thesis: (Poly (m,(anpoly ((1. F),(i + 1))))) . b₁ = ((Poly (m,(anpoly ((1. F),1)))) *' (Poly (m,(anpoly ((1. F),i))))) . b₁

then B: b = EmptyBag (card (nonConstantPolys F)) by PRE_POLY:81;
C: Sum s = 0. F

proof

divisors b = <*(EmptyBag (card (nonConstantPolys F)))*> by B, PRE_POLY:67;
then C1: dom (decomp b) = dom <*(EmptyBag (card (nonConstantPolys F)))*> by PRE_POLY:def 17;
dom <*(EmptyBag (card (nonConstantPolys F)))*> = Seg 1 by FINSEQ_1:38;
then C2: 1 in dom (decomp b) by C1;
C3: dom s = Seg (len (decomp b)) by A, FINSEQ_1:def 3
.= dom (decomp b) by FINSEQ_1:def 3 ;
then consider b1, b2 being bag of card (nonConstantPolys F) such that
C5: ( (decomp b) /. 1 = <*b1,b2*> & s /. 1 = ((Poly (m,(anpoly ((1. F),1)))) . b1) * ((Poly (m,(anpoly ((1. F),i)))) . b2) ) by A, C2;
b1 = (divisors b) /. 1 by C5, C2, PRE_POLY:70
.= EmptyBag (card (nonConstantPolys F)) by PRE_POLY:65 ;
then (Poly (m,(anpoly ((1. F),1)))) . b1 = (anpoly ((1. F),1)) . 0 by defPg
.= 0. F by POLYDIFF:25 ;
then C6: 0. F = s . 1 by C3, C2, C5, PARTFUN1:def 6;
dom (decomp b) = Seg 1 by C1, FINSEQ_1:38;
then 1 = len s by A, FINSEQ_1:def 3;
then s = <*(s . 1)*> by FINSEQ_1:40;
hence Sum s = 0. F by C6, RLVECT_1:44; :: thesis: verum

end;

thus (Poly (m,(anpoly ((1. F),(i + 1))))) . b = (anpoly ((1. F),(i + 1))) . 0 by B, defPg
.= ((Poly (m,(anpoly ((1. F),1)))) *' (Poly (m,(anpoly ((1. F),i))))) . b by A, C, POLYDIFF:25 ; :: thesis: verum

end;

suppose B: support b = {m} ; :: thesis: ((Poly (m,(anpoly ((1. F),1)))) *' (Poly (m,(anpoly ((1. F),i))))) . b₁ = (Poly (m,(anpoly ((1. F),(i + 1))))) . b₁

then C: (Poly (m,(anpoly ((1. F),(i + 1))))) . b = (anpoly ((1. F),(i + 1))) . (b . m) by defPg;

per cases ( b . m = i + 1 or b . m <> i + 1 ) ;

suppose C1: b . m = i + 1 ; :: thesis: ((Poly (m,(anpoly ((1. F),1)))) *' (Poly (m,(anpoly ((1. F),i))))) . b₁ = (Poly (m,(anpoly ((1. F),(i + 1))))) . b₁

then W: (Poly (m,(anpoly ((1. F),(i + 1))))) . b = 1. F by C, POLYDIFF:24;
C2: len (divisors b) = (i + 1) + 1 by B, C1, Th13f;
2 <= i + 2 by NAT_1:11;
then 2 in Seg (len (divisors b)) by C2;
then C3: 2 in dom (divisors b) by FINSEQ_1:def 3;
2 - 1 > 0 ;
then 2 -' 1 = 1 by XREAL_0:def 2;
then C4: (S,1) -bag = (divisors b) . 2 by C3, B, Th13f
.= (divisors b) /. 2 by C3, PARTFUN1:def 6 ;
set b3 = (S,1) -bag ;
2 in dom (decomp b) by C3, PRE_POLY:def 17;
then C6: (decomp b) /. 2 = <*((S,1) -bag),(b -' ((S,1) -bag))*> by C4, PRE_POLY:def 17;
C20: 2 in dom s by A1, C3, PRE_POLY:def 17;
V: s /. 2 = 1. F

proof

consider b1, b2 being bag of card (nonConstantPolys F) such that
C7: ( (decomp b) /. 2 = <*b1,b2*> & s /. 2 = ((Poly (m,(anpoly ((1. F),1)))) . b1) * ((Poly (m,(anpoly ((1. F),i)))) . b2) ) by A, C20;
C8: (S,1) -bag = <*b1,b2*> . 1 by C7, C6, FINSEQ_1:44
.= b1 ;
C9: b -' ((S,1) -bag) = <*b1,b2*> . 2 by C7, C6, FINSEQ_1:44
.= b2 ;
C12: b -' ((S,1) -bag) = (S,i) -bag

proof

now :: thesis: for o being object st o in card (nonConstantPolys F) holds
(b -' ((S,1) -bag)) . o = ((S,i) -bag) . o

let o be object ; :: thesis: ( o in card (nonConstantPolys F) implies (b -' ((S,1) -bag)) . b₁ = ((S,i) -bag) . b₁ )
assume o in card (nonConstantPolys F) ; :: thesis: (b -' ((S,1) -bag)) . b₁ = ((S,i) -bag) . b₁

per cases ( o = m or o <> m ) ;

suppose D2: o = m ; :: thesis: (b -' ((S,1) -bag)) . b₁ = ((S,i) -bag) . b₁

hence (b -' ((S,1) -bag)) . o = (b . m) -' (((S,1) -bag) . m) by PRE_POLY:def 6
.= (b . m) -' 1 by A2, UPROOTS:7
.= (b . m) - 1 by C1, XREAL_0:def 2
.= ((S,i) -bag) . o by A2, C1, D2, UPROOTS:7 ;
:: thesis: verum

end;

suppose o <> m ; :: thesis: (b -' ((S,1) -bag)) . b₁ = ((S,i) -bag) . b₁

then D3: not o in {m} by TARSKI:def 1;
thus (b -' ((S,1) -bag)) . o = (b . o) -' (((S,1) -bag) . o) by PRE_POLY:def 6
.= 0 -' (((S,1) -bag) . o) by D3, B, PRE_POLY:def 7
.= 0 by NAT_2:8
.= ((S,i) -bag) . o by D3, UPROOTS:6 ; :: thesis: verum

end;

end;

end;

hence b -' ((S,1) -bag) = (S,i) -bag by PBOOLE:def 10; :: thesis: verum

end;

then support (b -' ((S,1) -bag)) = {m} by U, UPROOTS:8;
then C10: (Poly (m,(anpoly ((1. F),i)))) . (b -' ((S,1) -bag)) = (anpoly ((1. F),i)) . (((S,i) -bag) . m) by C12, defPg
.= (anpoly ((1. F),i)) . i by A2, UPROOTS:7
.= 1. F by POLYDIFF:24 ;
support ((S,1) -bag) = {m} by UPROOTS:8;
then (Poly (m,(anpoly ((1. F),1)))) . ((S,1) -bag) = (anpoly ((1. F),1)) . (((S,1) -bag) . m) by defPg
.= (anpoly ((1. F),1)) . 1 by A2, UPROOTS:7
.= 1. F by POLYDIFF:24 ;
hence s /. 2 = 1. F by C10, C9, C8, C7; :: thesis: verum

end;

now :: thesis: for k being Element of NAT st k in dom s & k <> 2 holds
s /. k = 0. F

let k be Element of NAT ; :: thesis: ( k in dom s & k <> 2 implies s /. b₁ = 0. F )
assume C11: ( k in dom s & k <> 2 ) ; :: thesis: s /. b₁ = 0. F
then consider b1, b2 being bag of card (nonConstantPolys F) such that
C7: ( (decomp b) /. k = <*b1,b2*> & s /. k = ((Poly (m,(anpoly ((1. F),1)))) . b1) * ((Poly (m,(anpoly ((1. F),i)))) . b2) ) by A;
C10: k in dom (divisors b) by C11, A1, PRE_POLY:def 17;
then k in Seg (len (divisors b)) by FINSEQ_1:def 3;
then 1 <= k by FINSEQ_1:1;
then C17: k -' 1 = k - 1 by XREAL_0:def 2;
C9: b1 = (divisors b) /. k by C11, A1, C7, PRE_POLY:70;
then C16: b1 = (divisors b) . k by C10, PARTFUN1:def 6;

per cases ( k -' 1 = 0 or k -' 1 <> 0 ) ;

suppose k -' 1 = 0 ; :: thesis: s /. b₁ = 0. F

then b1 = EmptyBag (card (nonConstantPolys F)) by C17, C9, PRE_POLY:65;
then (Poly (m,(anpoly ((1. F),1)))) . b1 = (anpoly ((1. F),1)) . 0 by defPg
.= 0. F by POLYDIFF:25 ;
hence s /. k = 0. F by C7; :: thesis: verum

end;

suppose C13: k -' 1 <> 0 ; :: thesis: s /. b₁ = 0. F

C15: b1 = (S,(k -' 1)) -bag by B, C16, C10, Th13f;
then C12: support b1 = {m} by C13, UPROOTS:8;

C14: now :: thesis: not b1 . m = 1

assume b1 . m = 1 ; :: thesis: contradiction
then k -' 1 = 1 by C15, A2, UPROOTS:7;
hence contradiction by C17, C11; :: thesis: verum

end;

(Poly (m,(anpoly ((1. F),1)))) . b1 = (anpoly ((1. F),1)) . (b1 . m) by C12, defPg
.= 0. F by C14, POLYDIFF:25 ;
hence s /. k = 0. F by C7; :: thesis: verum

end;

end;

end;

hence ((Poly (m,(anpoly ((1. F),1)))) *' (Poly (m,(anpoly ((1. F),i))))) . b = (Poly (m,(anpoly ((1. F),(i + 1))))) . b by V, W, C20, A, POLYNOM2:3; :: thesis: verum

end;

suppose U: b . m <> i + 1 ; :: thesis: ((Poly (m,(anpoly ((1. F),1)))) *' (Poly (m,(anpoly ((1. F),i))))) . b₁ = (Poly (m,(anpoly ((1. F),(i + 1))))) . b₁

then W: (Poly (m,(anpoly ((1. F),(i + 1))))) . b = 0. F by C, POLYDIFF:25;
C3: 1 in dom s

proof

1 <= len (decomp b) by NAT_1:14;
then 1 in Seg (len (decomp b)) ;
hence 1 in dom s by A1, FINSEQ_1:def 3; :: thesis: verum

end;

C2: now :: thesis: for k being Element of NAT st k in dom s holds
s /. k = 0. F

let k be Element of NAT ; :: thesis: ( k in dom s implies s /. b₁ = 0. F )
assume C11: k in dom s ; :: thesis: s /. b₁ = 0. F
then consider b1, b2 being bag of card (nonConstantPolys F) such that
C3: ( (decomp b) /. k = <*b1,b2*> & s /. k = ((Poly (m,(anpoly ((1. F),1)))) . b1) * ((Poly (m,(anpoly ((1. F),i)))) . b2) ) by A;
C10: k in dom (divisors b) by C11, A1, PRE_POLY:def 17;
then k in Seg (len (divisors b)) by FINSEQ_1:def 3;
then 1 <= k by FINSEQ_1:1;
then C17: k -' 1 = k - 1 by XREAL_0:def 2;
C9: b1 = (divisors b) /. k by C11, A1, C3, PRE_POLY:70;
then C16: b1 = (divisors b) . k by C10, PARTFUN1:def 6;

per cases ( k -' 1 = 0 or k -' 1 <> 0 ) ;

suppose k -' 1 = 0 ; :: thesis: s /. b₁ = 0. F

then b1 = EmptyBag (card (nonConstantPolys F)) by C17, C9, PRE_POLY:65;
then (Poly (m,(anpoly ((1. F),1)))) . b1 = (anpoly ((1. F),1)) . 0 by defPg
.= 0. F by POLYDIFF:25 ;
hence s /. k = 0. F by C3; :: thesis: verum

end;

suppose C13: k -' 1 <> 0 ; :: thesis: s /. b₁ = 0. F

C15: b1 = (S,(k -' 1)) -bag by B, C16, C10, Th13f;
then C12: support b1 = {m} by C13, UPROOTS:8;
C13: b1 . m = k -' 1 by C15, A2, UPROOTS:7;

per cases ( b1 . m <> 1 or b1 . m = 1 ) ;

suppose C14: b1 . m <> 1 ; :: thesis: s /. b₁ = 0. F

(Poly (m,(anpoly ((1. F),1)))) . b1 = (anpoly ((1. F),1)) . (b1 . m) by C12, defPg
.= 0. F by C14, POLYDIFF:25 ;
hence s /. k = 0. F by C3; :: thesis: verum

end;

suppose C14: b1 . m = 1 ; :: thesis: s /. b₁ = 0. F

then CC: b1 = (S,1) -bag by C15, A2, UPROOTS:7;
C2: len (divisors b) = (b . m) + 1 by B, Th13f;
C32: b . m <> 0 by A2, B, PRE_POLY:def 7;
(b . m) + 1 >= 1 + 1 by C32, NAT_1:14, XREAL_1:6;
then 2 in Seg (len (divisors b)) by C2;
then C30: 2 in dom (divisors b) by FINSEQ_1:def 3;
2 - 1 > 0 ;
then 2 -' 1 = 1 by XREAL_0:def 2;
then C4: (S,1) -bag = (divisors b) . 2 by C30, B, Th13f
.= (divisors b) /. 2 by C30, PARTFUN1:def 6 ;
2 in dom (decomp b) by C30, PRE_POLY:def 17;
then C6: (decomp b) /. 2 = <*b1,(b -' b1)*> by C13, C14, B, C16, C10, Th13f, C4, PRE_POLY:def 17;
C90: b -' b1 = <*b1,b2*> . 2 by C13, C17, C14, C3, C6, FINSEQ_1:44
.= b2 ;
reconsider j = (b . m) - 1 as Element of NAT by C32, INT_1:3;

per cases ( (b . m) - 1 = 0 or (b . m) - 1 <> 0 ) ;

suppose C34: (b . m) - 1 = 0 ; :: thesis: s /. b₁ = 0. F

now :: thesis: for o being object st o in card (nonConstantPolys F) holds
b . o = b1 . o

let o be object ; :: thesis: ( o in card (nonConstantPolys F) implies b . b₁ = b1 . b₁ )
assume o in card (nonConstantPolys F) ; :: thesis: b . b₁ = b1 . b₁

per cases ( o = m or o <> m ) ;

suppose o = m ; :: thesis: b . b₁ = b1 . b₁

hence b . o = b1 . o by C14, C34; :: thesis: verum

end;

suppose H: o <> m ; :: thesis: b . b₁ = b1 . b₁

support b1 = {m} by CC, UPROOTS:8;
then I: not o in support b1 by H, TARSKI:def 1;
not o in support b by H, B, TARSKI:def 1;
hence b . o = 0 by PRE_POLY:def 7
.= b1 . o by I, PRE_POLY:def 7 ;
:: thesis: verum

end;

end;

end;

then b1 = b by PBOOLE:def 10;
then C35: EmptyBag (card (nonConstantPolys F)) = b2 by C90, PRE_POLY:56;
C36: i <> 0 by U, C34;
(Poly (m,(anpoly ((1. F),i)))) . b2 = (anpoly ((1. F),i)) . 0 by C35, defPg
.= 0. F by C36, POLYDIFF:25 ;
hence s /. k = 0. F by C3; :: thesis: verum

end;

suppose C34: (b . m) - 1 <> 0 ; :: thesis: s /. b₁ = 0. F

C12: b -' b1 = (S,j) -bag

proof

now :: thesis: for o being object st o in card (nonConstantPolys F) holds
(b -' b1) . o = ((S,j) -bag) . o

let o be object ; :: thesis: ( o in card (nonConstantPolys F) implies (b -' b1) . b₁ = ((S,j) -bag) . b₁ )
assume o in card (nonConstantPolys F) ; :: thesis: (b -' b1) . b₁ = ((S,j) -bag) . b₁

per cases ( o = m or o <> m ) ;

suppose D2: o = m ; :: thesis: (b -' b1) . b₁ = ((S,j) -bag) . b₁

hence (b -' b1) . o = (b . m) -' 1 by C14, PRE_POLY:def 6
.= (b . m) - 1 by C32, XREAL_0:def 2
.= ((S,j) -bag) . o by A2, D2, UPROOTS:7 ;
:: thesis: verum

end;

suppose o <> m ; :: thesis: (b -' b1) . b₁ = ((S,j) -bag) . b₁

then D3: not o in {m} by TARSKI:def 1;
thus (b -' b1) . o = (b . o) -' (b1 . o) by PRE_POLY:def 6
.= 0 -' (b1 . o) by D3, B, PRE_POLY:def 7
.= 0 by NAT_2:8
.= ((S,j) -bag) . o by D3, UPROOTS:6 ; :: thesis: verum

end;

end;

end;

hence b -' b1 = (S,j) -bag by PBOOLE:def 10; :: thesis: verum

end;

then C36: support (b -' b1) = {m} by C34, UPROOTS:8;
b2 . m = (b . m) - 1 by C12, C90, A2, UPROOTS:7;
then C35: b2 . m <> i by U;
(Poly (m,(anpoly ((1. F),i)))) . b2 = (anpoly ((1. F),i)) . (b2 . m) by C36, C90, defPg
.= 0. F by C35, POLYDIFF:25 ;
hence s /. k = 0. F by C3; :: thesis: verum

end;

end;

end;

end;

end;

end;

end;

then for k being Element of NAT st k in dom s & k <> 1 holds
s /. k = 0. F ;
hence ((Poly (m,(anpoly ((1. F),1)))) *' (Poly (m,(anpoly ((1. F),i))))) . b = s /. 1 by A, C3, POLYNOM2:3
.= (Poly (m,(anpoly ((1. F),(i + 1))))) . b by C2, C3, W ;
:: thesis: verum

end;

end;

end;

suppose U1: ( support b <> {} & support b <> {m} ) ; :: thesis: ((Poly (m,(anpoly ((1. F),1)))) *' (Poly (m,(anpoly ((1. F),i))))) . b₁ = (Poly (m,(anpoly ((1. F),(i + 1))))) . b₁

then W: (Poly (m,(anpoly ((1. F),(i + 1))))) . b = 0. F by defPg;
C3: 1 in dom s

proof

1 <= len (decomp b) by NAT_1:14;
then 1 in Seg (len (decomp b)) ;
hence 1 in dom s by A1, FINSEQ_1:def 3; :: thesis: verum

end;

C2: now :: thesis: for k being Element of NAT st k in dom s holds
s /. k = 0. F

let k be Element of NAT ; :: thesis: ( k in dom s implies s /. b₁ = 0. F )
assume C11: k in dom s ; :: thesis: s /. b₁ = 0. F
then consider b1, b2 being bag of card (nonConstantPolys F) such that
C3: ( (decomp b) /. k = <*b1,b2*> & s /. k = ((Poly (m,(anpoly ((1. F),1)))) . b1) * ((Poly (m,(anpoly ((1. F),i)))) . b2) ) by A;
consider a1, a2 being bag of card (nonConstantPolys F) such that
C4: ( (decomp b) /. k = <*a1,a2*> & b = a1 + a2 ) by C11, A1, PRE_POLY:68;
C5: a1 = <*b1,b2*> . 1 by C3, C4, FINSEQ_1:44
.= b1 ;
C6: a2 = <*b1,b2*> . 2 by C3, C4, FINSEQ_1:44
.= b2 ;

per cases ( support b1 = {} or support b1 <> {} ) ;

suppose support b1 = {} ; :: thesis: s /. b₁ = 0. F

then b1 = EmptyBag (card (nonConstantPolys F)) by PRE_POLY:81;
then (Poly (m,(anpoly ((1. F),1)))) . b1 = (anpoly ((1. F),1)) . 0 by defPg
.= 0. F by POLYDIFF:25 ;
hence s /. k = 0. F by C3; :: thesis: verum

end;

suppose D1: support b1 <> {} ; :: thesis: s /. b₁ = 0. F

per cases ( support b2 = {} or support b2 <> {} ) ;

suppose support b2 = {} ; :: thesis: s /. b₁ = 0. F

then b2 = EmptyBag (card (nonConstantPolys F)) by PRE_POLY:81;
then (Poly (m,(anpoly ((1. F),i)))) . b2 = (anpoly ((1. F),i)) . 0 by defPg
.= 0. F by U, POLYDIFF:25 ;
hence s /. k = 0. F by C3; :: thesis: verum

end;

suppose D2: support b2 <> {} ; :: thesis: s /. b₁ = 0. F

now :: thesis: ( support b1 = {m} implies not support b2 = {m} )

assume ( support b1 = {m} & support b2 = {m} ) ; :: thesis: contradiction
then support b = {m} \/ {m} by C4, C5, C6, PRE_POLY:38;
hence contradiction by U1; :: thesis: verum

end;

per cases then ( support b1 <> {m} or support b2 <> {m} ) ;

suppose support b1 <> {m} ; :: thesis: s /. b₁ = 0. F

then (Poly (m,(anpoly ((1. F),1)))) . b1 = 0. F by D1, defPg;
hence s /. k = 0. F by C3; :: thesis: verum

end;

suppose support b2 <> {m} ; :: thesis: s /. b₁ = 0. F

then (Poly (m,(anpoly ((1. F),i)))) . b2 = 0. F by D2, defPg;
hence s /. k = 0. F by C3; :: thesis: verum

end;

end;

end;

end;

end;

end;

end;

then for k being Element of NAT st k in dom s & k <> 1 holds
s /. k = 0. F ;
hence ((Poly (m,(anpoly ((1. F),1)))) *' (Poly (m,(anpoly ((1. F),i))))) . b = s /. 1 by A, C3, POLYNOM2:3
.= (Poly (m,(anpoly ((1. F),(i + 1))))) . b by C2, C3, W ;
:: thesis: verum

end;

end;

end;

hence (Poly (m,(anpoly ((1. F),1)))) *' (Poly (m,(anpoly ((1. F),i)))) = Poly (m,(anpoly ((1. F),(i + 1)))) ; :: thesis: verum

end;

end;