let L be non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr ; :: thesis: for f being FinSequence of (Polynom-Ring L) st ( for i being Nat st i in dom f holds
ex z being Element of L st f . i = rpoly (1,z) ) holds
for p being Polynomial of L st p = Product f holds
p <> 0_. L
let f be FinSequence of (Polynom-Ring L); :: thesis: ( ( for i being Nat st i in dom f holds
ex z being Element of L st f . i = rpoly (1,z) ) implies for p being Polynomial of L st p = Product f holds
p <> 0_. L )
assume A1: for i being Nat st i in dom f holds
ex z being Element of L st f . i = rpoly (1,z) ; :: thesis: for p being Polynomial of L st p = Product f holds
p <> 0_. L
let p be Polynomial of L; :: thesis: ( p = Product f implies p <> 0_. L )
assume A2: p = Product f ; :: thesis: p <> 0_. L
defpred S₁[ Nat] means for f being FinSequence of (Polynom-Ring L) st len f = $1 & ( for i being Nat st i in dom f holds
ex z being Element of L st f . i = rpoly (1,z) ) holds
for p being Polynomial of L st p = Product f holds
p <> 0_. L;

now :: thesis: for f being FinSequence of (Polynom-Ring L) st len f = 0 & ( for i being Nat st i in dom f holds
ex z being Element of L st f . i = rpoly (1,z) ) holds
for p being Polynomial of L st p = Product f holds
p <> 0_. L

let f be FinSequence of (Polynom-Ring L); :: thesis: ( len f = 0 & ( for i being Nat st i in dom f holds
ex z being Element of L st f . i = rpoly (1,z) ) implies for p being Polynomial of L st p = Product f holds
p <> 0_. L )
assume A3: ( len f = 0 & ( for i being Nat st i in dom f holds
ex z being Element of L st f . i = rpoly (1,z) ) ) ; :: thesis: for p being Polynomial of L st p = Product f holds
p <> 0_. L
let p be Polynomial of L; :: thesis: ( p = Product f implies p <> 0_. L )
assume A4: p = Product f ; :: thesis: p <> 0_. L
f = <*> the carrier of (Polynom-Ring L) by A3;
then p = 1_ (Polynom-Ring L) by A4, GROUP_4:8
.= 1. (Polynom-Ring L) ;
then p <> 0. (Polynom-Ring L) ;
hence p <> 0_. L by POLYNOM3:def 10; :: thesis: verum

end;

then A5: S₁[ 0 ] ;

A6: now :: thesis: for n being Nat st S₁[n] holds
S₁[n + 1]

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

now :: thesis: for f being FinSequence of (Polynom-Ring L) st len f = n + 1 & ( for i being Nat st i in dom f holds
ex z being Element of L st f . i = rpoly (1,z) ) holds
for p being Polynomial of L st p = Product f holds
p <> 0_. L

let f be FinSequence of (Polynom-Ring L); :: thesis: ( len f = n + 1 & ( for i being Nat st i in dom f holds
ex z being Element of L st f . i = rpoly (1,z) ) implies for p being Polynomial of L st p = Product f holds
p <> 0_. L )
assume A8: ( len f = n + 1 & ( for i being Nat st i in dom f holds
ex z being Element of L st f . i = rpoly (1,z) ) ) ; :: thesis: for p being Polynomial of L st p = Product f holds
p <> 0_. L
let p be Polynomial of L; :: thesis: ( p = Product f implies p <> 0_. L )
assume A9: p = Product f ; :: thesis: p <> 0_. L
f <> {} by A8;
then consider g being FinSequence, u being object such that
A10: f = g ^ <*u*> by FINSEQ_1:46;
reconsider g = g as FinSequence of (Polynom-Ring L) by A10, FINSEQ_1:36;
A11: dom f = Seg (n + 1) by A8, FINSEQ_1:def 3;
1 <= n + 1 by NAT_1:11;
then A12: n + 1 in dom f by A11;
A13: n + 1 = (len g) + (len <*u*>) by A8, A10, FINSEQ_1:22
.= (len g) + 1 by FINSEQ_1:40 ;
then f . (n + 1) = u by A10, FINSEQ_1:42;
then consider z being Element of L such that
A14: u = rpoly (1,z) by A8, A12;
reconsider u = u as Element of (Polynom-Ring L) by A14, POLYNOM3:def 10;
reconsider q = Product g as Polynomial of L by POLYNOM3:def 10;
A15: Product f = (Product g) * u by A10, GROUP_4:6;
A16: u <> 0. (Polynom-Ring L) by A14, POLYNOM3:def 10;

now :: thesis: for i being Nat st i in dom g holds
ex z being Element of L st g . i = rpoly (1,z)

let i be Nat; :: thesis: ( i in dom g implies ex z being Element of L st g . i = rpoly (1,z) )
assume A17: i in dom g ; :: thesis: ex z being Element of L st g . i = rpoly (1,z)
then A18: g . i = f . i by A10, FINSEQ_1:def 7;
dom g c= dom f by A10, FINSEQ_1:26;
hence ex z being Element of L st g . i = rpoly (1,z) by A17, A18, A8; :: thesis: verum

end;

then q <> 0_. L by A7, A13;
then q <> 0. (Polynom-Ring L) by POLYNOM3:def 10;
then p <> 0. (Polynom-Ring L) by A9, A16, A15, VECTSP_2:def 1;
hence p <> 0_. L by POLYNOM3:def 10; :: thesis: verum

end;

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

end;

A19: for n being Nat holds S₁[n] from NAT_1:sch 2(A5, A6);
len f is Nat ;
hence p <> 0_. L by A1, A2, A19; :: thesis: verum