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;
A3: now :: thesis: not q = 0_. L
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 q is non-zero ;
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