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 q being non-zero Polynomial of L holds len (<%r,(1. L)%> *' q) = (len q) + 1
let r be Element of L; :: thesis: for q being non-zero Polynomial of L holds len (<%r,(1. L)%> *' q) = (len q) + 1
let q be non-zero Polynomial of L; :: thesis: len (<%r,(1. L)%> *' q) = (len q) + 1
set p = <%r,(1. L)%>;
A1: (<%r,(1. L)%> . ((len <%r,(1. L)%>) -' 1)) * (q . ((len q) -' 1)) = (<%r,(1. L)%> . ((1 + 1) -' 1)) * (q . ((len q) -' 1)) by POLYNOM5:40
.= (<%r,(1. L)%> . 1) * (q . ((len q) -' 1)) by NAT_D:34
.= (1. L) * (q . ((len q) -' 1)) by POLYNOM5:38
.= q . ((len q) -' 1) ;
( len <%r,(1. L)%> = 2 & len q > 0 ) by Th14, POLYNOM5:40;
hence len (<%r,(1. L)%> *' q) = ((len q) + (1 + 1)) - 1 by A1, Th15, POLYNOM4:10
.= (len q) + 1 ;
:: thesis: verum