let L be non empty non degenerated well-unital doubleLoopStr ; :: thesis: for z being Element of L
for k being Element of NAT holds deg (rpoly k,z) = k
let z be Element of L; :: thesis: for k being Element of NAT holds deg (rpoly k,z) = k
let k be Element of NAT ; :: thesis: deg (rpoly k,z) = k
set t = rpoly k,z;
set f = 0 ,k --> (- ((power L) . z,k)),(1_ L);
set a = - ((power L) . z,k);

per cases ( k = 0 or k <> 0 ) ;

suppose A1: k = 0 ; :: thesis: deg (rpoly k,z) = k

now

let i be Nat; :: thesis: ( i >= 1 implies (rpoly k,z) . i = 0. L )
A2: i in NAT by ORDINAL1:def 13;
assume i >= 1 ; :: thesis: (rpoly k,z) . i = 0. L
then not i in dom (0 ,k --> (- ((power L) . z,k)),(1_ L)) by A1, TARSKI:def 2;
hence (rpoly k,z) . i = (0_. L) . i by FUNCT_4:12
.= 0. L by A2, FUNCOP_1:13 ;
:: thesis: verum

end;

then A3: 1 is_at_least_length_of rpoly k,z by ALGSEQ_1:def 3;

now

let m be Nat; :: thesis: ( m is_at_least_length_of rpoly k,z implies 1 <= m )
assume A4: m is_at_least_length_of rpoly k,z ; :: thesis: 1 <= m

now

assume m < 1 ; :: thesis: contradiction
then A5: m = 0 by NAT_1:14;
A6: k in {k} by TARSKI:def 1;
then A7: k in dom ({k} --> (1_ L)) by FUNCOP_1:19;
dom (0 ,k --> (- ((power L) . z,k)),(1_ L)) = {0 ,k} by FUNCT_4:65;
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:14
.= ((0 .--> (- ((power L) . z,k))) +* (k .--> (1_ L))) . 0 by FUNCT_4:def 4
.= (0 .--> (1_ L)) . 0 by A1, A7, FUNCT_4:14
.= 1_ L by A1, A6, FUNCOP_1:13 ;
hence contradiction by A4, A5, ALGSEQ_1:def 3; :: thesis: verum

end;

hence 1 <= m ; :: thesis: verum

end;

then len (rpoly k,z) = 1 by A3, ALGSEQ_1:def 4;
hence deg (rpoly k,z) = k by A1; :: thesis: verum

end;

suppose A8: k <> 0 ; :: thesis: deg (rpoly k,z) = k

now

let i be Nat; :: thesis: ( i >= k + 1 implies (rpoly k,z) . i = 0. L )
assume i >= k + 1 ; :: thesis: (rpoly k,z) . i = 0. L
then i > k by NAT_1:13;
hence (rpoly k,z) . i = 0. L by Lm12; :: thesis: verum

end;

then A9: k + 1 is_at_least_length_of rpoly k,z by ALGSEQ_1:def 3;

now

let m be Nat; :: thesis: ( m is_at_least_length_of rpoly k,z implies k + 1 <= m )
assume A10: m is_at_least_length_of rpoly k,z ; :: thesis: k + 1 <= m

now

assume m < k + 1 ; :: thesis: contradiction
then A11: m <= k by NAT_1:13;
(rpoly k,z) . k = 1_ L by A8, Lm11;
hence contradiction by A10, A11, ALGSEQ_1:def 3; :: thesis: verum

end;

hence k + 1 <= m ; :: thesis: verum

end;

then len (rpoly k,z) = k + 1 by A9, ALGSEQ_1:def 4;
hence deg (rpoly k,z) = k ; :: thesis: verum

end;

end;