let L be non empty right_complementable left-distributive well-unital add-associative right_zeroed commutative doubleLoopStr ; :: thesis: for z being Element of L
for k being Element of NAT st k > 1 holds
(rpoly (1,z)) *' (qpoly (k,z)) = rpoly (k,z)
let z be Element of L; :: thesis: for k being Element of NAT st k > 1 holds
(rpoly (1,z)) *' (qpoly (k,z)) = rpoly (k,z)
let k be Element of NAT ; :: thesis: ( k > 1 implies (rpoly (1,z)) *' (qpoly (k,z)) = rpoly (k,z) )
set p = (rpoly (1,z)) *' (qpoly (k,z));
set u = rpoly (k,z);
assume A1: k > 1 ; :: thesis: (rpoly (1,z)) *' (qpoly (k,z)) = rpoly (k,z)
then reconsider k1 = k - 1 as Element of NAT by INT_1:5;
k1 + 1 = k ;
then A2: k1 <= k by INT_1:6;
k1 <> k ;
then A3: k1 < k by A2, XXREAL_0:1;

A4: now :: thesis: for i9 being object st i9 in dom ((rpoly (1,z)) *' (qpoly (k,z))) holds
((rpoly (1,z)) *' (qpoly (k,z))) . i9 = (rpoly (k,z)) . i9

A5: 1 - 1 >= 0 ;
let i9 be object ; :: thesis: ( i9 in dom ((rpoly (1,z)) *' (qpoly (k,z))) implies ((rpoly (1,z)) *' (qpoly (k,z))) . b₁ = (rpoly (k,z)) . b₁ )
A6: 0 + 1 = 1 ;
assume i9 in dom ((rpoly (1,z)) *' (qpoly (k,z))) ; :: thesis: ((rpoly (1,z)) *' (qpoly (k,z))) . b₁ = (rpoly (k,z)) . b₁
then reconsider i = i9 as Element of NAT ;
consider fp being FinSequence of L such that
A7: len fp = i + 1 and
A8: ((rpoly (1,z)) *' (qpoly (k,z))) . i = Sum fp and
A9: for j being Element of NAT st j in dom fp holds
fp . j = ((rpoly (1,z)) . (j -' 1)) * ((qpoly (k,z)) . ((i + 1) -' j)) by POLYNOM3:def 9;
A10: (i + 1) - 2 = i - 1 ;
len fp >= 1 by A7, NAT_1:11;
then 1 in Seg (len fp) ;
then A11: 1 in dom fp by FINSEQ_1:def 3;
then A12: fp /. 1 = fp . 1 by PARTFUN1:def 6
.= ((rpoly (1,z)) . (1 -' 1)) * ((qpoly (k,z)) . ((i + 1) -' 1)) by A9, A11
.= ((rpoly (1,z)) . 0) * ((qpoly (k,z)) . ((i + 1) -' 1)) by A5, XREAL_0:def 2
.= (- ((power L) . (z,1))) * ((qpoly (k,z)) . ((i + 1) -' 1)) by Lm10
.= (- (((power L) . (z,0)) * z)) * ((qpoly (k,z)) . ((i + 1) -' 1)) by A6, GROUP_1:def 7
.= (- ((1_ L) * z)) * ((qpoly (k,z)) . ((i + 1) -' 1)) by GROUP_1:def 7
.= (- z) * ((qpoly (k,z)) . ((i + 1) -' 1))
.= (- z) * ((qpoly (k,z)) . i) by NAT_D:34 ;

A13: now :: thesis: for j being Element of NAT st j in dom fp & j <> 1 & j <> 2 holds
fp . j = 0. L

let j be Element of NAT ; :: thesis: ( j in dom fp & j <> 1 & j <> 2 implies fp . j = 0. L )
assume that
A14: j in dom fp and
A15: j <> 1 and
A16: j <> 2 ; :: thesis: fp . j = 0. L
A17: j in Seg (len fp) by A14, FINSEQ_1:def 3;

now :: thesis: ( not j -' 1 = 0 & not j -' 1 = 1 )

assume A18: ( j -' 1 = 0 or j -' 1 = 1 ) ; :: thesis: contradiction

per cases ( j - 1 >= 0 or j - 1 < 0 ) ;

suppose j - 1 >= 0 ; :: thesis: contradiction

then j -' 1 = j - 1 by XREAL_0:def 2;
hence contradiction by A15, A16, A18; :: thesis: verum

end;

suppose j - 1 < 0 ; :: thesis: contradiction

then (j - 1) + 1 < 0 + 1 by XREAL_1:8;
hence contradiction by A17, FINSEQ_1:1; :: thesis: verum

end;

end;

end;

then A19: (rpoly (1,z)) . (j -' 1) = 0. L by Lm11;
fp . j = ((rpoly (1,z)) . (j -' 1)) * ((qpoly (k,z)) . ((i + 1) -' j)) by A9, A14;
hence fp . j = 0. L by A19; :: thesis: verum

end;

A20: now :: thesis: ( i <> 0 implies ((rpoly (1,z)) *' (qpoly (k,z))) . i = (fp /. 1) + (fp /. 2) )

A21: 1 + 1 = 2 ;
consider g1, g2 being FinSequence of L such that
A22: len g1 = 1 and
A23: len g2 = i and
A24: fp = g1 ^ g2 by A7, FINSEQ_2:23;
A25: g1 = <*(g1 . 1)*> by A22, FINSEQ_1:40
.= <*(fp . 1)*> by A22, A24, FINSEQ_1:64
.= <*(fp /. 1)*> by A11, PARTFUN1:def 6 ;
assume i <> 0 ; :: thesis: ((rpoly (1,z)) *' (qpoly (k,z))) . i = (fp /. 1) + (fp /. 2)
then A26: i + 1 > 0 + 1 by XREAL_1:8;
then A27: i >= 1 by NAT_1:13;
then 1 in Seg (len g2) by A23;
then A28: 1 in dom g2 by FINSEQ_1:def 3;
1 + 1 <= len fp by A7, A26, NAT_1:13;
then 2 in Seg (len fp) ;
then A29: 2 in dom fp by FINSEQ_1:def 3;

now :: thesis: for i being Element of NAT st i in dom g2 & i <> 1 holds
g2 /. i = 0. L

let i be Element of NAT ; :: thesis: ( i in dom g2 & i <> 1 implies g2 /. i = 0. L )
assume that
A30: i in dom g2 and
A31: i <> 1 ; :: thesis: g2 /. i = 0. L
A32: i + 1 <> 2 by A31;
A33: 1 <= i + 1 by NAT_1:11;
A34: i in Seg (len g2) by A30, FINSEQ_1:def 3;
then A35: i <= len g2 by FINSEQ_1:1;
len fp = 1 + (len g2) by A22, A24, FINSEQ_1:22;
then i + 1 <= len fp by A35, XREAL_1:6;
then i + 1 in Seg (len fp) by A33;
then A36: i + 1 in dom fp by FINSEQ_1:def 3;
i + 1 <> 0 + 1 by A34, FINSEQ_1:1;
then A37: fp . (i + 1) = 0. L by A13, A36, A32;
1 <= i by A34, FINSEQ_1:1;
then g2 . i = fp . (i + 1) by A22, A24, A35, FINSEQ_1:65;
hence g2 /. i = 0. L by A30, A37, PARTFUN1:def 6; :: thesis: verum

end;

then Sum g2 = g2 /. 1 by A28, POLYNOM2:3
.= g2 . 1 by A28, PARTFUN1:def 6
.= fp . 2 by A27, A22, A23, A24, A21, FINSEQ_1:65
.= fp /. 2 by A29, PARTFUN1:def 6 ;
hence ((rpoly (1,z)) *' (qpoly (k,z))) . i = (Sum g1) + (fp /. 2) by A8, A24, RLVECT_1:41
.= (fp /. 1) + (fp /. 2) by A25, RLVECT_1:44 ;
:: thesis: verum

end;

A38: 2 - 1 >= 0 ;

A39: now :: thesis: ( i <> 0 implies fp /. 2 = (qpoly (k,z)) . (i -' 1) )

assume i <> 0 ; :: thesis: fp /. 2 = (qpoly (k,z)) . (i -' 1)
then A40: i + 1 > 0 + 1 by XREAL_1:8;
then i >= 1 by NAT_1:13;
then reconsider i1 = i - 1 as Element of NAT by INT_1:5;
len fp >= 1 + 1 by A7, A40, NAT_1:13;
then 2 in Seg (len fp) ;
then A41: 2 in dom fp by FINSEQ_1:def 3;
then A42: fp . 2 = ((rpoly (1,z)) . (2 -' 1)) * ((qpoly (k,z)) . ((i + 1) -' 2)) by A9
.= ((rpoly (1,z)) . 1) * ((qpoly (k,z)) . ((i + 1) -' 2)) by A38, XREAL_0:def 2
.= (1_ L) * ((qpoly (k,z)) . ((i + 1) -' 2)) by Lm10
.= (qpoly (k,z)) . ((i + 1) -' 2)
.= (qpoly (k,z)) . i1 by A10, XREAL_0:def 2 ;
thus fp /. 2 = fp . 2 by A41, PARTFUN1:def 6
.= (qpoly (k,z)) . (i -' 1) by A42, XREAL_0:def 2 ; :: thesis: verum

end;

per cases ( i < k or i = k or i > k ) by XXREAL_0:1;

suppose A43: i < k ; :: thesis: ((rpoly (1,z)) *' (qpoly (k,z))) . b₁ = (rpoly (k,z)) . b₁

per cases ( i = 0 or i > 0 ) ;

suppose A44: i = 0 ; :: thesis: ((rpoly (1,z)) *' (qpoly (k,z))) . b₁ = (rpoly (k,z)) . b₁

A45: (k - 0) - 1 = k1 ;
A46: k1 + 1 = k ;
fp = <*(fp . 1)*> by A7, A44, FINSEQ_1:40
.= <*(fp /. 1)*> by A11, PARTFUN1:def 6 ;
hence ((rpoly (1,z)) *' (qpoly (k,z))) . i9 = (- z) * ((qpoly (k,z)) . 0) by A8, A12, A44, RLVECT_1:44
.= (- z) * ((power L) . (z,k1)) by A45, A46, Def4
.= - (z * ((power L) . (z,k1))) by VECTSP_1:9
.= - ((power L) . (z,k)) by A46, GROUP_1:def 7
.= (rpoly (k,z)) . i9 by A1, A44, Lm10 ;
:: thesis: verum

end;

suppose A47: i > 0 ; :: thesis: ((rpoly (1,z)) *' (qpoly (k,z))) . b₁ = (rpoly (k,z)) . b₁

then i + 1 > 0 + 1 by XREAL_1:6;
then i >= 1 by NAT_1:13;
then i - 1 >= 1 - 1 by XREAL_1:9;
then i -' 1 = i - 1 by XREAL_0:def 2;
then A48: (k - (i -' 1)) - 1 = k - i ;
k - i > i - i by A43, XREAL_1:9;
then reconsider ki = k - i as Element of NAT by INT_1:3;
ki > i - i by A43, XREAL_1:9;
then ki + 1 > 0 + 1 by XREAL_1:6;
then ki >= 1 by NAT_1:13;
then reconsider ki1 = (k - i) - 1 as Element of NAT by INT_1:5;
A49: k - 1 < k - 0 by XREAL_1:10;
i - 1 < k - 1 by A43, XREAL_1:9;
then A50: i - 1 < k by A49, XXREAL_0:2;
A51: ki1 + 1 = ki ;
thus ((rpoly (1,z)) *' (qpoly (k,z))) . i9 = ((- z) * ((power L) . (z,ki1))) + ((qpoly (k,z)) . (i -' 1)) by A12, A39, A20, A43, A47, Def4
.= ((- z) * ((power L) . (z,ki1))) + ((power L) . (z,ki)) by A48, A50, Def4
.= (- (z * ((power L) . (z,ki1)))) + ((power L) . (z,ki)) by VECTSP_1:9
.= (- ((power L) . (z,ki))) + ((power L) . (z,ki)) by A51, GROUP_1:def 7
.= 0. L by RLVECT_1:5
.= (rpoly (k,z)) . i9 by A43, A47, Lm11 ; :: thesis: verum

end;

end;

end;

suppose A52: i = k ; :: thesis: ((rpoly (1,z)) *' (qpoly (k,z))) . b₁ = (rpoly (k,z)) . b₁

then i - 1 >= 1 - 1 by A1, XREAL_1:9;
then A53: i -' 1 = i - 1 by XREAL_0:def 2;
A54: (k - k1) - 1 = 0 ;
fp /. 1 = (- z) * (0. L) by A12, A52, Def4
.= 0. L ;
hence ((rpoly (1,z)) *' (qpoly (k,z))) . i9 = (qpoly (k,z)) . k1 by A39, A20, A52, A53, ALGSTR_1:def 2
.= (power L) . (z,0) by A3, A54, Def4
.= 1_ L by GROUP_1:def 7
.= (rpoly (k,z)) . i9 by A1, A52, Lm10 ;
:: thesis: verum

end;

suppose A55: i > k ; :: thesis: ((rpoly (1,z)) *' (qpoly (k,z))) . b₁ = (rpoly (k,z)) . b₁

then i + 1 > 0 + 1 by XREAL_1:6;
then i >= 1 by NAT_1:13;
then i - 1 >= 1 - 1 by XREAL_1:9;
then A56: i -' 1 = i - 1 by XREAL_0:def 2;
i >= k + 1 by A55, NAT_1:13;
then A57: i - 1 >= (k + 1) - 1 by XREAL_1:9;
fp /. 1 = (- z) * (0. L) by A12, A55, Def4
.= 0. L ;
hence ((rpoly (1,z)) *' (qpoly (k,z))) . i9 = (qpoly (k,z)) . (i -' 1) by A39, A20, A55, ALGSTR_1:def 2
.= 0. L by A56, A57, Def4
.= (rpoly (k,z)) . i9 by A55, Lm11 ;
:: thesis: verum

end;

end;

end;

dom ((rpoly (1,z)) *' (qpoly (k,z))) = NAT by FUNCT_2:def 1
.= dom (rpoly (k,z)) by FUNCT_2:def 1 ;
hence (rpoly (1,z)) *' (qpoly (k,z)) = rpoly (k,z) by A4, FUNCT_1:2; :: thesis: verum