let L be non degenerated right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed 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 AS1: 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 AS2: 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 A1: ( 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 A2: p = Product f ; :: thesis: p <> 0_. L
f = <*> the carrier of (Polynom-Ring L) by A1;
then p = 1_ (Polynom-Ring L) by A2, 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 IA: S₁[ 0 ] ;

IS: 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 IV: 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 A1: ( 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 A2: p = Product f ; :: thesis: p <> 0_. L
f <> {} by A1;
then consider g being FinSequence, u being set such that
A6: f = g ^ <*u*> by FINSEQ_1:46;
reconsider g = g as FinSequence of (Polynom-Ring L) by A6, FINSEQ_1:36;
A2c: dom f = Seg (n + 1) by A1, FINSEQ_1:def 3;
1 <= n + 1 by NAT_1:11;
then A2a: n + 1 in dom f by A2c;
A2c: n + 1 = (len g) + (len <*u*>) by A1, A6, FINSEQ_1:22
.= (len g) + 1 by FINSEQ_1:40 ;
then f . (n + 1) = u by A6, FINSEQ_1:42;
then consider z being Element of L such that
U: u = rpoly (1,z) by A1, A2a;
reconsider u = u as Element of (Polynom-Ring L) by U, POLYNOM3:def 10;
reconsider q = Product g as Polynomial of L by POLYNOM3:def 10;
A4: Product f = (Product g) * u by A6, GROUP_4:6;
A3: u <> 0. (Polynom-Ring L) by U, 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 G: i in dom g ; :: thesis: ex z being Element of L st g . i = rpoly (1,z)
then H: g . i = f . i by A6, FINSEQ_1:def 7;
dom g c= dom f by A6, FINSEQ_1:26;
hence ex z being Element of L st g . i = rpoly (1,z) by G, H, A1; :: thesis: verum

end;

then q <> 0_. L by IV, A2c;
then q <> 0. (Polynom-Ring L) by POLYNOM3:def 10;
then p <> 0. (Polynom-Ring L) by A2, A3, A4, VECTSP_2:def 1;
hence p <> 0_. L by POLYNOM3:def 10; :: thesis: verum

end;

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

end;

I: for n being Nat holds S₁[n] from NAT_1:sch 2(IA, IS);
len f is Nat ;
hence p <> 0_. L by AS1, AS2, I; :: thesis: verum