let L be non empty non degenerated well-unital doubleLoopStr ; for z being Element of L
for k being Element of NAT holds deg (rpoly (k,z)) = k
let z be Element of L; for k being Element of NAT holds deg (rpoly (k,z)) = k
let k be Element of NAT ; deg (rpoly (k,z)) = k
set t = rpoly (k,z);
set a = - ((power L) . (z,k));
set f = (0,k) --> ((- ((power L) . (z,k))),(1_ L));
per cases
( k = 0 or k <> 0 )
;
suppose A1:
k = 0
;
deg (rpoly (k,z)) = kA2:
now for m being Nat st m is_at_least_length_of rpoly (k,z) holds
1 <= mlet m be
Nat;
( m is_at_least_length_of rpoly (k,z) implies 1 <= m )assume A3:
m is_at_least_length_of rpoly (
k,
z)
;
1 <= mnow not m < 1assume
m < 1
;
contradictionthen A4:
m = 0
by NAT_1:14;
A5:
k in {k}
by TARSKI:def 1;
then A6:
k in dom ({k} --> (1_ L))
;
dom ((0,k) --> ((- ((power L) . (z,k))),(1_ L))) = {0,k}
by FUNCT_4:62;
then
0 in dom ((0,k) --> ((- ((power L) . (z,k))),(1_ L)))
by TARSKI:def 2;
then (rpoly (k,z)) . 0 =
((0,k) --> ((- ((power L) . (z,k))),(1_ L))) . 0
by FUNCT_4:13
.=
((0 .--> (- ((power L) . (z,k)))) +* (k .--> (1_ L))) . 0
by FUNCT_4:def 4
.=
(0 .--> (1_ L)) . 0
by A1, A6, FUNCT_4:13
.=
1_ L
by A1, A5, FUNCOP_1:7
;
hence
contradiction
by A3, A4, ALGSEQ_1:def 2;
verum end; hence
1
<= m
;
verum end; then
1
is_at_least_length_of rpoly (
k,
z)
by ALGSEQ_1:def 2;
then
len (rpoly (k,z)) = 1
by A2, ALGSEQ_1:def 3;
hence
deg (rpoly (k,z)) = k
by A1;
verum end; end;