let L be non degenerated comRing; :: thesis: for x being Element of L

for i being Nat holds len (<%x,(1. L)%> `^ i) = i + 1

let x be Element of L; :: thesis: for i being Nat holds len (<%x,(1. L)%> `^ i) = i + 1

defpred S_{1}[ Nat] means len (<%x,(1. L)%> `^ $1) = $1 + 1;

set r = <%x,(1. L)%>;

A1: for i being Nat st S_{1}[i] holds

S_{1}[i + 1]

then A3: S_{1}[ 0 ]
by POLYNOM4:4;

thus for i being Nat holds S_{1}[i]
from NAT_1:sch 2(A3, A1); :: thesis: verum

for i being Nat holds len (<%x,(1. L)%> `^ i) = i + 1

let x be Element of L; :: thesis: for i being Nat holds len (<%x,(1. L)%> `^ i) = i + 1

defpred S

set r = <%x,(1. L)%>;

A1: for i being Nat st S

S

proof

<%x,(1. L)%> `^ 0 = 1_. L
by POLYNOM5:15;
let i be Nat; :: thesis: ( S_{1}[i] implies S_{1}[i + 1] )

assume A2: S_{1}[i]
; :: thesis: S_{1}[i + 1]

reconsider ri = <%x,(1. L)%> `^ i as non-zero Polynomial of L by A2, Th14;

thus len (<%x,(1. L)%> `^ (i + 1)) = len ((<%x,(1. L)%> `^ 1) *' ri) by Th27

.= len (<%x,(1. L)%> *' ri) by POLYNOM5:16

.= (i + 1) + 1 by A2, Th35 ; :: thesis: verum

end;assume A2: S

reconsider ri = <%x,(1. L)%> `^ i as non-zero Polynomial of L by A2, Th14;

thus len (<%x,(1. L)%> `^ (i + 1)) = len ((<%x,(1. L)%> `^ 1) *' ri) by Th27

.= len (<%x,(1. L)%> *' ri) by POLYNOM5:16

.= (i + 1) + 1 by A2, Th35 ; :: thesis: verum

then A3: S

thus for i being Nat holds S