let L be non empty non degenerated right_complementable well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr ; :: thesis: for r being Element of L

for p, q being Polynomial of L st p = <%r,(1. L)%> *' q & p . ((len p) -' 1) = 1. L holds

q . ((len q) -' 1) = 1. L

let x be Element of L; :: thesis: for p, q being Polynomial of L st p = <%x,(1. L)%> *' q & p . ((len p) -' 1) = 1. L holds

q . ((len q) -' 1) = 1. L

let p, q be Polynomial of L; :: thesis: ( p = <%x,(1. L)%> *' q & p . ((len p) -' 1) = 1. L implies q . ((len q) -' 1) = 1. L )

assume that

A1: p = <%x,(1. L)%> *' q and

A2: p . ((len p) -' 1) = 1. L ; :: thesis: q . ((len q) -' 1) = 1. L

set lp1 = (len p) -' 1;

then len p = (len q) + 1 by A1, Th35;

then A4: (len p) -' 1 = len q by NAT_D:34;

then consider lp2 being Nat such that

A5: (len p) -' 1 = lp2 + 1 by A3, NAT_1:6, POLYNOM4:5;

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

A6: q . ((len p) -' 1) = 0. L by A4, ALGSEQ_1:8;

(<%x,(1. L)%> *' q) . ((len p) -' 1) = (x * (q . ((len p) -' 1))) + ((1. L) * (q . lp2)) by A5, Th34

.= (0. L) + ((1. L) * (q . lp2)) by A6

.= (1. L) * (q . lp2) by RLVECT_1:4

.= q . lp2 ;

hence q . ((len q) -' 1) = 1. L by A1, A2, A4, A5, NAT_D:34; :: thesis: verum

for p, q being Polynomial of L st p = <%r,(1. L)%> *' q & p . ((len p) -' 1) = 1. L holds

q . ((len q) -' 1) = 1. L

let x be Element of L; :: thesis: for p, q being Polynomial of L st p = <%x,(1. L)%> *' q & p . ((len p) -' 1) = 1. L holds

q . ((len q) -' 1) = 1. L

let p, q be Polynomial of L; :: thesis: ( p = <%x,(1. L)%> *' q & p . ((len p) -' 1) = 1. L implies q . ((len q) -' 1) = 1. L )

assume that

A1: p = <%x,(1. L)%> *' q and

A2: p . ((len p) -' 1) = 1. L ; :: thesis: q . ((len q) -' 1) = 1. L

set lp1 = (len p) -' 1;

A3: now :: thesis: not q = 0_. L

then
q is non-zero
;assume
q = 0_. L
; :: thesis: contradiction

then p = 0_. L by A1, POLYNOM3:34;

hence contradiction by A2, FUNCOP_1:7; :: thesis: verum

end;then p = 0_. L by A1, POLYNOM3:34;

hence contradiction by A2, FUNCOP_1:7; :: thesis: verum

then len p = (len q) + 1 by A1, Th35;

then A4: (len p) -' 1 = len q by NAT_D:34;

then consider lp2 being Nat such that

A5: (len p) -' 1 = lp2 + 1 by A3, NAT_1:6, POLYNOM4:5;

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

A6: q . ((len p) -' 1) = 0. L by A4, ALGSEQ_1:8;

(<%x,(1. L)%> *' q) . ((len p) -' 1) = (x * (q . ((len p) -' 1))) + ((1. L) * (q . lp2)) by A5, Th34

.= (0. L) + ((1. L) * (q . lp2)) by A6

.= (1. L) * (q . lp2) by RLVECT_1:4

.= q . lp2 ;

hence q . ((len q) -' 1) = 1. L by A1, A2, A4, A5, NAT_D:34; :: thesis: verum