let L be non degenerated comRing; 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; 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; for i being Nat holds len ((<%x,(1. L)%> `^ i) *' q) = i + (len q)
set r = <%x,(1. L)%>;
defpred S1[ Nat] means len ((<%x,(1. L)%> `^ $1) *' q) = $1 + (len q);
A1:
for i being Nat st S1[i] holds
S1[i + 1]
proof
let i be
Nat;
( S1[i] implies S1[i + 1] )
assume A2:
S1[
i]
;
S1[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)
;
verum
end;
len ((<%x,(1. L)%> `^ 0) *' q) =
len ((1_. L) *' q)
by POLYNOM5:15
.=
0 + (len q)
by POLYNOM3:35
;
then A4:
S1[ 0 ]
;
thus
for i being Nat holds S1[i]
from NAT_1:sch 2(A4, A1); verum