let L be non degenerated comRing; :: thesis: for x being Element of L
for q being non-zero Polynomial of L
for i being Nat holds len ((<%x,(1. L)%> `^ i) *' q) = i + (len q)

let x be Element of L; :: thesis: for q being non-zero Polynomial of L
for i being Nat holds len ((<%x,(1. L)%> `^ i) *' q) = i + (len q)

let q be non-zero Polynomial of L; :: thesis: for i being Nat holds len ((<%x,(1. L)%> `^ i) *' q) = i + (len q)
set r = <%x,(1. L)%>;
defpred S1[ Nat] means len ((<%x,(1. L)%> `^ \$1) *' q) = \$1 + (len q);
A1: for i being Nat st S1[i] holds
S1[i + 1]
proof
let i be Nat; :: thesis: ( S1[i] implies S1[i + 1] )
assume A2: S1[i] ; :: thesis: S1[i + 1]
len q > 0 by Th14;
then A3: (<%x,(1. L)%> `^ i) *' q is non-zero by ;
thus len ((<%x,(1. L)%> `^ (i + 1)) *' q) = len (((<%x,(1. L)%> `^ 1) *' (<%x,(1. L)%> `^ i)) *' q) by Th27
.= len ((<%x,(1. L)%> *' (<%x,(1. L)%> `^ i)) *' q) by POLYNOM5:16
.= len (<%x,(1. L)%> *' ((<%x,(1. L)%> `^ i) *' q)) by POLYNOM3:33
.= (i + (len q)) + 1 by A2, A3, Th35
.= (i + 1) + (len q) ; :: thesis: verum
end;
len ((<%x,(1. L)%> `^ 0) *' q) = len ((1_. L) *' q) by POLYNOM5:15
.= 0 + (len q) by POLYNOM3:35 ;
then A4: S1[ 0 ] ;
thus for i being Nat holds S1[i] from NAT_1:sch 2(A4, A1); :: thesis: verum