let F be Field; :: thesis: for a being non zero Element of F
for i being Nat
for m being Ordinal st m in card (nonConstantPolys F) holds
(Poly (m,(anpoly (a,0)))) *' (Poly (m,(anpoly ((1. F),i)))) = Poly (m,(anpoly (a,i)))
let a be non zero Element of F; :: thesis: for i being Nat
for m being Ordinal st m in card (nonConstantPolys F) holds
(Poly (m,(anpoly (a,0)))) *' (Poly (m,(anpoly ((1. F),i)))) = Poly (m,(anpoly (a,i)))
let i be Nat; :: thesis: for m being Ordinal st m in card (nonConstantPolys F) holds
(Poly (m,(anpoly (a,0)))) *' (Poly (m,(anpoly ((1. F),i)))) = Poly (m,(anpoly (a,i)))
let m be Ordinal; :: thesis: ( m in card (nonConstantPolys F) implies (Poly (m,(anpoly (a,0)))) *' (Poly (m,(anpoly ((1. F),i)))) = Poly (m,(anpoly (a,i))) )
set n = card (nonConstantPolys F);
assume AS: m in card (nonConstantPolys F) ; :: thesis: (Poly (m,(anpoly (a,0)))) *' (Poly (m,(anpoly ((1. F),i)))) = Poly (m,(anpoly (a,i)))
anpoly (a,0) = a | F by FIELD_1:7;
then C: Poly (m,(anpoly (a,0))) = a | ((card (nonConstantPolys F)),F) by AS, XYZbb;
then A: (Poly (m,(anpoly (a,0)))) *' (Poly (m,(anpoly ((1. F),i)))) = a * (Poly (m,(anpoly ((1. F),i)))) by POLYNOM7:27;
set q = a * (Poly (m,(anpoly ((1. F),i))));

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

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

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;
hence (Poly (m,(anpoly (a,0)))) *' (Poly (m,(anpoly ((1. F),i)))) = (a | ((card (nonConstantPolys F)),F)) *' (1_ ((card (nonConstantPolys F)),F)) by C, POLYNOM7:20
.= Poly (m,(anpoly (a,i))) by I, C, POLYNOM1:29 ;
:: thesis: verum

end;

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

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

let o be Element of Bags (card (nonConstantPolys F)); :: thesis: (Poly (m,(anpoly (a,i)))) . b₁ = (a * (Poly (m,(anpoly ((1. F),i))))) . b₁

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

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

then B: o = EmptyBag (card (nonConstantPolys F)) by PRE_POLY:81;
hence (Poly (m,(anpoly (a,i)))) . o = (anpoly (a,i)) . 0 by defPg
.= a * (0. F) by I, POLYDIFF:25
.= a * ((anpoly ((1. F),i)) . 0) by I, POLYDIFF:25
.= a * ((Poly (m,(anpoly ((1. F),i)))) . o) by B, defPg
.= (a * (Poly (m,(anpoly ((1. F),i))))) . o by POLYNOM7:def 9 ;
:: thesis: verum

end;

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

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

suppose I2: o . m = i ; :: thesis: (Poly (m,(anpoly (a,i)))) . b₁ = (a * (Poly (m,(anpoly ((1. F),i))))) . b₁

thus (Poly (m,(anpoly (a,i)))) . o = (anpoly (a,i)) . (o . m) by I1, defPg
.= a * (1. F) by I2, POLYDIFF:24
.= a * ((anpoly ((1. F),i)) . (o . m)) by I2, POLYDIFF:24
.= a * ((Poly (m,(anpoly ((1. F),i)))) . o) by I1, defPg
.= (a * (Poly (m,(anpoly ((1. F),i))))) . o by POLYNOM7:def 9 ; :: thesis: verum

end;

suppose I2: o . m <> i ; :: thesis: (Poly (m,(anpoly (a,i)))) . b₁ = (a * (Poly (m,(anpoly ((1. F),i))))) . b₁

thus (Poly (m,(anpoly (a,i)))) . o = (anpoly (a,i)) . (o . m) by I1, defPg
.= a * (0. F) by I2, POLYDIFF:25
.= a * ((anpoly ((1. F),i)) . (o . m)) by I2, POLYDIFF:25
.= a * ((Poly (m,(anpoly ((1. F),i)))) . o) by I1, defPg
.= (a * (Poly (m,(anpoly ((1. F),i))))) . o by POLYNOM7:def 9 ; :: thesis: verum

end;

end;

end;

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

hence (Poly (m,(anpoly (a,i)))) . o = a * (0. F) by defPg
.= a * ((Poly (m,(anpoly ((1. F),i)))) . o) by I2, defPg
.= (a * (Poly (m,(anpoly ((1. F),i))))) . o by POLYNOM7:def 9 ;
:: thesis: verum

end;

end;

end;

hence (Poly (m,(anpoly (a,0)))) *' (Poly (m,(anpoly ((1. F),i)))) = Poly (m,(anpoly (a,i))) by A; :: thesis: verum

end;

end;