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 S1[ Nat] means len (<%x,(1. L)%> `^ $1) = $1 + 1;
set r = <%x,(1. L)%>;
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]
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: S1[ 0 ] by POLYNOM4:4;
thus for i being Nat holds S1[i] from NAT_1:sch 2(A3, A1); :: thesis: verum