let F be Field; :: thesis: for G being non empty FinSequence of the carrier of (Polynom-Ring F) holds
( Product G = 0_. F iff ex i being Element of dom G st G . i = 0_. F )
let G be non empty FinSequence of the carrier of (Polynom-Ring F); :: thesis: ( Product G = 0_. F iff ex i being Element of dom G st G . i = 0_. F )

A: now :: thesis: ( ex i being Element of dom G st G . i = 0_. F implies Product G = 0_. F )

assume ex i being Element of dom G st G . i = 0_. F ; :: thesis: Product G = 0_. F
then consider i being Element of dom G such that
B: G . i = 0_. F ;
reconsider p = Product <*(G . i)*> as Polynomial of F by POLYNOM3:def 10;
dom G = Seg (len G) by FINSEQ_1:def 3;
then ( 1 <= i & i <= len G ) by FINSEQ_1:1;
then G = ((G | (i -' 1)) ^ <*(G . i)*>) ^ (G /^ i) by FINSEQ_5:84;
then D: Product G = (Product ((G | (i -' 1)) ^ <*(G . i)*>)) * (Product (G /^ i)) by GROUP_4:5
.= ((Product (G | (i -' 1))) * (Product <*(G . i)*>)) * (Product (G /^ i)) by GROUP_4:5
.= ((Product <*(G . i)*>) * (Product (G | (i -' 1)))) * (Product (G /^ i)) by GROUP_1:def 12
.= (Product <*(G . i)*>) * ((Product (G | (i -' 1))) * (Product (G /^ i))) by GROUP_1:def 3 ;
reconsider r1 = Product (G | (i -' 1)), r2 = Product (G /^ i) as Polynomial of F by POLYNOM3:def 10;
F: p = 0_. F by B, GROUP_4:9;
r1 *' r2 = (Product (G | (i -' 1))) * (Product (G /^ i)) by POLYNOM3:def 10;
hence Product G = (0_. F) *' (r1 *' r2) by F, D, POLYNOM3:def 10
.= 0_. F ;
:: thesis: verum

end;

defpred S₁[ Nat] means for G being non empty FinSequence of the carrier of (Polynom-Ring F) st len G = $1 & ( for i being Element of dom G holds G . i <> 0_. F ) holds
Product G <> 0_. F;
C: S₁[1]

proof

now :: thesis: for G being non empty FinSequence of the carrier of (Polynom-Ring F) st len G = 1 & ( for i being Element of dom G holds G . i <> 0_. F ) holds
Product G <> 0_. F

let G be non empty FinSequence of the carrier of (Polynom-Ring F); :: thesis: ( len G = 1 & ( for i being Element of dom G holds G . i <> 0_. F ) implies Product G <> 0_. F )
assume C1: ( len G = 1 & ( for i being Element of dom G holds G . i <> 0_. F ) ) ; :: thesis: Product G <> 0_. F
then C2: G = <*(G . 1)*> by FINSEQ_1:40;
then C3: dom G = Seg 1 by FINSEQ_1:38;
then C4: 1 in dom G by FINSEQ_1:3;
G = <*(G /. 1)*> by C2, C3, PARTFUN1:def 6, FINSEQ_1:3;
then Product G = G /. 1 by GROUP_4:9
.= G . 1 by C3, PARTFUN1:def 6, FINSEQ_1:3 ;
hence Product G <> 0_. F by C1, C4; :: thesis: verum

end;

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

end;

D: now :: thesis: for k being Nat st 1 <= k & S₁[k] holds
S₁[k + 1]

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

now :: thesis: for G being non empty FinSequence of the carrier of (Polynom-Ring F) st len G = k + 1 & ( for i being Element of dom G holds G . i <> 0_. F ) holds
Product G <> 0_. F

let G be non empty FinSequence of the carrier of (Polynom-Ring F); :: thesis: ( len G = k + 1 & ( for i being Element of dom G holds G . i <> 0_. F ) implies Product G <> 0_. F )
assume D3: ( len G = k + 1 & ( for i being Element of dom G holds G . i <> 0_. F ) ) ; :: thesis: Product G <> 0_. F
consider G1 being FinSequence, y being object such that
B2: G = G1 ^ <*y*> by FINSEQ_1:46;
H: rng G c= the carrier of (Polynom-Ring F) by FINSEQ_1:def 4;
rng G1 c= rng G by B2, FINSEQ_1:29;
then reconsider G1 = G1 as FinSequence of the carrier of (Polynom-Ring F) by XBOOLE_1:1, H, FINSEQ_1:def 4;
len <*y*> = 1 by FINSEQ_1:40;
then C4: dom G = Seg ((len G1) + 1) by B2, FINSEQ_1:def 7;
B12: 1 <= (len G1) + 1 by NAT_1:11;
then B21: (len G1) + 1 in dom G by C4, FINSEQ_1:1;
dom <*y*> = Seg 1 by FINSEQ_1:38;
then B11: 1 in dom <*y*> by FINSEQ_1:3;
B20: y = <*y*> . 1
.= G . ((len G1) + 1) by B11, B2, FINSEQ_1:def 7 ;
then B13: y in rng G by B12, C4, FINSEQ_1:1, FUNCT_1:3;
rng G c= the carrier of (Polynom-Ring F) by FINSEQ_1:def 4;
then reconsider y = y as Element of the carrier of (Polynom-Ring F) by B13;
B3: Product G = (Product G1) * y by B2, GROUP_4:6;
B4: len G = (len G1) + (len <*y*>) by B2, FINSEQ_1:22
.= (len G1) + 1 by FINSEQ_1:39 ;

now :: thesis: not Product G = 0_. F

assume Product G = 0_. F ; :: thesis: contradiction
then Product G = 0. (Polynom-Ring F) by POLYNOM3:def 10;

per cases then ( y = 0. (Polynom-Ring F) or Product G1 = 0. (Polynom-Ring F) ) by B3, VECTSP_2:def 1;

suppose y = 0. (Polynom-Ring F) ; :: thesis: contradiction

then y = 0_. F by POLYNOM3:def 10;
hence contradiction by D3, B20, B21; :: thesis: verum

end;

suppose D6: Product G1 = 0. (Polynom-Ring F) ; :: thesis: contradiction

D7: Product (<*> the carrier of (Polynom-Ring F)) = 1_ (Polynom-Ring F) by GROUP_4:8;
then D9: not G1 is empty by D6;
then D8: dom G1 <> {} ;
Product G1 = 0_. F by D6, POLYNOM3:def 10;
then consider i being Element of dom G1 such that
D4: G1 . i = 0_. F by D3, D2, B4, D7;
dom G1 c= dom G by B2, FINSEQ_1:26;
then D5: ( i in dom G & i in dom G1 ) by D8;
G1 . i = G . i by D9, B2, FINSEQ_1:def 7;
hence contradiction by D3, D4, D5; :: thesis: verum

end;

end;

end;

hence Product G <> 0_. F ; :: thesis: verum

end;

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

end;

I: for k being Nat st k >= 1 holds
S₁[k] from NAT_1:sch 8(C, D);

now :: thesis: ( Product G = 0_. F implies ex i being Element of dom G st G . i = 0_. F )

assume B: Product G = 0_. F ; :: thesis: ex i being Element of dom G st G . i = 0_. F
consider n being Nat such that
H: n = len G ;
n >= 1 by H, NAT_1:14;
hence ex i being Element of dom G st G . i = 0_. F by B, I, H; :: thesis: verum

end;

hence ( Product G = 0_. F iff ex i being Element of dom G st G . i = 0_. F ) by A; :: thesis: verum