let L be non empty right_complementable commutative left-distributive well-unital add-associative right_zeroed 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:18;
k1 + 1 = k ;
then A2: k1 <= k by INT_1:19;
k1 <> k ;
then A3: k1 < k by A2, XXREAL_0:1;

A4: now

A5: 1 - 1 >= 0 ;
let i9 be set ; :: 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 11;
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 8
.= ((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 Lm11
.= (- (((power L) . z,0 ) * z)) * ((qpoly k,z) . ((i + 1) -' 1)) by A6, GROUP_1:def 8
.= (- ((1_ L) * z)) * ((qpoly k,z) . ((i + 1) -' 1)) by GROUP_1:def 8
.= (- z) * ((qpoly k,z) . ((i + 1) -' 1)) by VECTSP_1:def 19
.= (- z) * ((qpoly k,z) . i) by NAT_D:34 ;

A13: now

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

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:10;
hence contradiction by A17, FINSEQ_1:3; :: thesis: verum

end;

end;

end;

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

end;

A20: now

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:26;
A25: g1 = <*(g1 . 1)*> by A22, FINSEQ_1:57
.= <*(fp . 1)*> by A22, A24, FINSEQ_1:85
.= <*(fp /. 1)*> by A11, PARTFUN1:def 8 ;
assume i <> 0 ; :: thesis: ((rpoly 1,z) *' (qpoly k,z)) . i = (fp /. 1) + (fp /. 2)
then A26: i + 1 > 0 + 1 by XREAL_1:10;
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

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:3;
len fp = 1 + (len g2) by A22, A24, FINSEQ_1:35;
then i + 1 <= len fp by A35, XREAL_1:8;
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:3;
then A37: fp . (i + 1) = 0. L by A13, A36, A32;
1 <= i by A34, FINSEQ_1:3;
then g2 . i = fp . (i + 1) by A22, A24, A35, FINSEQ_1:86;
hence g2 /. i = 0. L by A30, A37, PARTFUN1:def 8; :: thesis: verum

end;

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

end;

A38: 2 - 1 >= 0 ;

A39: now

assume i <> 0 ; :: thesis: fp /. 2 = (qpoly k,z) . (i -' 1)
then A40: i + 1 > 0 + 1 by XREAL_1:10;
then i >= 1 by NAT_1:13;
then reconsider i1 = i - 1 as Element of NAT by INT_1:18;
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 Lm11
.= (qpoly k,z) . ((i + 1) -' 2) by VECTSP_1:def 19
.= (qpoly k,z) . i1 by A10, XREAL_0:def 2 ;
thus fp /. 2 = fp . 2 by A41, PARTFUN1:def 8
.= (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:57
.= <*(fp /. 1)*> by A11, PARTFUN1:def 8 ;
hence ((rpoly 1,z) *' (qpoly k,z)) . i9 = (- z) * ((qpoly k,z) . 0 ) by A8, A12, A44, RLVECT_1:61
.= (- z) * ((power L) . z,k1) by A45, A46, Def4
.= - (z * ((power L) . z,k1)) by VECTSP_1:41
.= - ((power L) . z,k) by A46, GROUP_1:def 8
.= (rpoly k,z) . i9 by A1, A44, Lm11 ;
:: 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:8;
then i >= 1 by NAT_1:13;
then i - 1 >= 1 - 1 by XREAL_1:11;
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:11;
then reconsider ki = k - i as Element of NAT by INT_1:16;
ki > i - i by A43, XREAL_1:11;
then ki + 1 > 0 + 1 by XREAL_1:8;
then ki >= 1 by NAT_1:13;
then reconsider ki1 = (k - i) - 1 as Element of NAT by INT_1:18;
A49: k - 1 < k - 0 by XREAL_1:12;
i - 1 < k - 1 by A43, XREAL_1:11;
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:41
.= (- ((power L) . z,ki)) + ((power L) . z,ki) by A51, GROUP_1:def 8
.= 0. L by RLVECT_1:16
.= (rpoly k,z) . i9 by A43, A47, Lm12 ; :: 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:11;
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 by VECTSP_1:36 ;
hence ((rpoly 1,z) *' (qpoly k,z)) . i9 = (qpoly k,z) . k1 by A39, A20, A52, A53, ALGSTR_1:def 5
.= (power L) . z,0 by A3, A54, Def4
.= 1_ L by GROUP_1:def 8
.= (rpoly k,z) . i9 by A1, A52, Lm11 ;
:: 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:8;
then i >= 1 by NAT_1:13;
then i - 1 >= 1 - 1 by XREAL_1:11;
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:11;
fp /. 1 = (- z) * (0. L) by A12, A55, Def4
.= 0. L by VECTSP_1:36 ;
hence ((rpoly 1,z) *' (qpoly k,z)) . i9 = (qpoly k,z) . (i -' 1) by A39, A20, A55, ALGSTR_1:def 5
.= 0. L by A56, A57, Def4
.= (rpoly k,z) . i9 by A55, Lm12 ;
:: 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:9; :: thesis: verum