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 S<sub>1</sub>[ Nat] means len ((<%x,(1. L)%> `^ $1) *' q) = $1 + (len q);
A1: for i being Nat st S₁[i] holds
S₁[i + 1]

proof

let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume A2: S₁[i] ; :: thesis: S₁[i + 1]
len q > 0 by Th14;
then A3: (<%x,(1. L)%> `^ i) *' q is non-zero by A2, Th14;
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: S₁[ 0 ] ;
thus for i being Nat holds S₁[i] from NAT_1:sch 2(A4, A1); :: thesis: verum