let L be non empty right_complementable distributive add-associative right_zeroed domRing-like doubleLoopStr ; :: thesis: for p, q being Polynomial of L holds

( not p *' q = 0_. L or p = 0_. L or q = 0_. L )

let p, q be Polynomial of L; :: thesis: ( not p *' q = 0_. L or p = 0_. L or q = 0_. L )

assume that

A1: p *' q = 0_. L and

A2: p <> 0_. L and

A3: q <> 0_. L ; :: thesis: contradiction

consider lp1 being Nat such that

A4: len p = lp1 + 1 by A2, NAT_1:6, POLYNOM4:5;

len p <> 0 by A2, POLYNOM4:5;

then A5: 0 + 1 <= len p by NAT_1:13;

consider lq1 being Nat such that

A6: len q = lq1 + 1 by A3, NAT_1:6, POLYNOM4:5;

reconsider lp1 = lp1, lq1 = lq1 as Element of NAT by ORDINAL1:def 12;

A7: p . lp1 <> 0. L by A4, ALGSEQ_1:10;

A8: q . lq1 <> 0. L by A6, ALGSEQ_1:10;

set lpq = lp1 + lq1;

consider r being FinSequence of L such that

A9: len r = (lp1 + lq1) + 1 and

A10: (p *' q) . (lp1 + lq1) = Sum r and

A11: for k being Element of NAT st k in dom r holds

r . k = (p . (k -' 1)) * (q . (((lp1 + lq1) + 1) -' k)) by POLYNOM3:def 9;

A12: ((lp1 + lq1) + 1) -' (len p) = (lq1 + (lp1 + 1)) -' (len p)

.= lq1 by A4, NAT_D:34 ;

len p <= (lp1 + 1) + lq1 by A4, NAT_1:12;

then A13: len p in dom r by A9, A5, FINSEQ_3:25;

.= (p . ((len p) -' 1)) * (q . (((lp1 + lq1) + 1) -' (len p))) by A11, A13

.= (p . lp1) * (q . lq1) by A4, A12, NAT_D:34 ;

then Sum r <> 0. L by A7, A8, VECTSP_2:def 1;

hence contradiction by A1, A10, FUNCOP_1:7; :: thesis: verum

( not p *' q = 0_. L or p = 0_. L or q = 0_. L )

let p, q be Polynomial of L; :: thesis: ( not p *' q = 0_. L or p = 0_. L or q = 0_. L )

assume that

A1: p *' q = 0_. L and

A2: p <> 0_. L and

A3: q <> 0_. L ; :: thesis: contradiction

consider lp1 being Nat such that

A4: len p = lp1 + 1 by A2, NAT_1:6, POLYNOM4:5;

len p <> 0 by A2, POLYNOM4:5;

then A5: 0 + 1 <= len p by NAT_1:13;

consider lq1 being Nat such that

A6: len q = lq1 + 1 by A3, NAT_1:6, POLYNOM4:5;

reconsider lp1 = lp1, lq1 = lq1 as Element of NAT by ORDINAL1:def 12;

A7: p . lp1 <> 0. L by A4, ALGSEQ_1:10;

A8: q . lq1 <> 0. L by A6, ALGSEQ_1:10;

set lpq = lp1 + lq1;

consider r being FinSequence of L such that

A9: len r = (lp1 + lq1) + 1 and

A10: (p *' q) . (lp1 + lq1) = Sum r and

A11: for k being Element of NAT st k in dom r holds

r . k = (p . (k -' 1)) * (q . (((lp1 + lq1) + 1) -' k)) by POLYNOM3:def 9;

A12: ((lp1 + lq1) + 1) -' (len p) = (lq1 + (lp1 + 1)) -' (len p)

.= lq1 by A4, NAT_D:34 ;

len p <= (lp1 + 1) + lq1 by A4, NAT_1:12;

then A13: len p in dom r by A9, A5, FINSEQ_3:25;

now :: thesis: for k being Nat st k in dom r & k <> len p holds

r . k = 0. L

then Sum r =
r . (len p)
by A13, MATRIX_3:12
r . k = 0. L

let k be Nat; :: thesis: ( k in dom r & k <> len p implies r . b_{1} = 0. L )

assume that

A14: k in dom r and

A15: k <> len p ; :: thesis: r . b_{1} = 0. L

reconsider k1 = k as Element of NAT by ORDINAL1:def 12;

A16: r . k1 = (p . (k1 -' 1)) * (q . (((lp1 + lq1) + 1) -' k1)) by A11, A14;

end;assume that

A14: k in dom r and

A15: k <> len p ; :: thesis: r . b

reconsider k1 = k as Element of NAT by ORDINAL1:def 12;

A16: r . k1 = (p . (k1 -' 1)) * (q . (((lp1 + lq1) + 1) -' k1)) by A11, A14;

per cases
( k < len p or k > len p )
by A15, XXREAL_0:1;

end;

suppose
k < len p
; :: thesis: r . b_{1} = 0. L

then consider d being Element of NAT such that

A17: len p = k1 + d and

A18: 1 <= d by FINSEQ_4:84;

A19: len q <= lq1 + d by A6, A18, XREAL_1:6;

((lp1 + lq1) + 1) -' k = ((lq1 + d) + k) -' k by A4, A17

.= lq1 + d by NAT_D:34 ;

hence r . k = (p . (k -' 1)) * (0. L) by A16, A19, ALGSEQ_1:8

.= 0. L ;

:: thesis: verum

end;A17: len p = k1 + d and

A18: 1 <= d by FINSEQ_4:84;

A19: len q <= lq1 + d by A6, A18, XREAL_1:6;

((lp1 + lq1) + 1) -' k = ((lq1 + d) + k) -' k by A4, A17

.= lq1 + d by NAT_D:34 ;

hence r . k = (p . (k -' 1)) * (0. L) by A16, A19, ALGSEQ_1:8

.= 0. L ;

:: thesis: verum

.= (p . ((len p) -' 1)) * (q . (((lp1 + lq1) + 1) -' (len p))) by A11, A13

.= (p . lp1) * (q . lq1) by A4, A12, NAT_D:34 ;

then Sum r <> 0. L by A7, A8, VECTSP_2:def 1;

hence contradiction by A1, A10, FUNCOP_1:7; :: thesis: verum