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₁[ Nat] means len (<%x,(1. L)%> `^ $1) = $1 + 1;
set r = <%x,(1. L)%>;
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]
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;

<%x,(1. L)%> `^ 0 = 1_. L by POLYNOM5:15;
then A3: S₁[ 0 ] by POLYNOM4:4;
thus for i being Nat holds S₁[i] from NAT_1:sch 2(A3, A1); :: thesis: verum