let L be domRing; :: thesis: for p being Polynomial of L st len p <> 0 holds
for n being Nat holds len (p `^ n) = ((n * (len p)) - n) + 1
let p be Polynomial of L; :: thesis: ( len p <> 0 implies for n being Nat holds len (p `^ n) = ((n * (len p)) - n) + 1 )
defpred S₁[ Nat] means len (p `^ $1) = (($1 * (len p)) - $1) + 1;
assume A1: len p <> 0 ; :: thesis: for n being Nat holds len (p `^ n) = ((n * (len p)) - n) + 1

A2: now :: thesis: for n being Nat st S₁[n] holds
S₁[n + 1]

len p >= 0 + 1 by A1, NAT_1:13;
then (len p) - 1 >= (0 + 1) - 1 ;
then A3: (len p) -' 1 = (len p) - 1 by XREAL_0:def 2;
A4: p . ((len p) -' 1) <> 0. L by A1, Lm2;
let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A5: S₁[n] ; :: thesis: S₁[n + 1]
(n * ((len p) -' 1)) + 1 >= 0 + 1 by XREAL_1:6;
then (p `^ n) . ((len (p `^ n)) -' 1) <> 0. L by A5, A3, Lm2;
then A6: ((p `^ n) . ((len (p `^ n)) -' 1)) * (p . ((len p) -' 1)) <> 0. L by A4, VECTSP_2:def 1;
len (p `^ (n + 1)) = len ((p `^ n) *' p) by Th19
.= ((((n * (len p)) - n) + 1) + (len p)) - 1 by A5, A6, POLYNOM4:10
.= (((n + 1) * (len p)) - (n + 1)) + 1 ;
hence S₁[n + 1] ; :: thesis: verum

end;

len (p `^ 0) = len (1_. L) by Th15
.= ((0 * (len p)) - 0) + 1 by POLYNOM4:4 ;
then A7: S₁[ 0 ] ;
thus for n being Nat holds S₁[n] from NAT_1:sch 2(A7, A2); :: thesis: verum