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 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 ; :: thesis: deg (rpoly (k,z)) = k

A2: now :: thesis: for m being Nat st m is_at_least_length_of rpoly (k,z) holds
1 <= m

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

now :: thesis: not m < 1

assume m < 1 ; :: thesis: contradiction
then 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; :: thesis: verum

end;

hence 1 <= m ; :: thesis: verum

end;

now :: thesis: for i being Nat st i >= 1 holds
(rpoly (k,z)) . i = 0. L

let i be Nat; :: thesis: ( i >= 1 implies (rpoly (k,z)) . i = 0. L )
A7: i in NAT by ORDINAL1:def 12;
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:11
.= 0. L by A7, FUNCOP_1:7 ;
:: thesis: 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; :: thesis: verum

end;

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

A9: now :: thesis: for m being Nat st m is_at_least_length_of rpoly (k,z) holds
k + 1 <= m

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 :: thesis: not m < k + 1

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

end;

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

end;

now :: thesis: for i being Nat st i >= k + 1 holds
(rpoly (k,z)) . i = 0. L

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 Lm11; :: thesis: verum

end;

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

end;

end;