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 )
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;
set p = (rpoly 1,z) *' (qpoly k,z);
set u = rpoly k,z;
A4: dom ((rpoly 1,z) *' (qpoly k,z)) = NAT by FUNCT_2:def 1
.= dom (rpoly k,z) by FUNCT_2:def 1 ;

now

let i' be set ; :: thesis: ( i' in dom ((rpoly 1,z) *' (qpoly k,z)) implies ((rpoly 1,z) *' (qpoly k,z)) . b₁ = (rpoly k,z) . b₁ )
assume i' in dom ((rpoly 1,z) *' (qpoly k,z)) ; :: thesis: ((rpoly 1,z) *' (qpoly k,z)) . b₁ = (rpoly k,z) . b₁
then reconsider i = i' as Element of NAT ;
consider fp being FinSequence of L such that
A5: ( len fp = i + 1 & ((rpoly 1,z) *' (qpoly k,z)) . i = Sum fp & ( 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;
A6: ( 0 + 1 = 1 & 1 - 1 >= 0 ) ;
A7: 2 - 1 >= 0 ;
len fp >= 1 by A5, NAT_1:11;
then 1 in Seg (len fp) ;
then A8: 1 in dom fp by FINSEQ_1:def 3;
then A9: fp /. 1 = fp . 1 by PARTFUN1:def 8
.= ((rpoly 1,z) . (1 -' 1)) * ((qpoly k,z) . ((i + 1) -' 1)) by A5, A8
.= ((rpoly 1,z) . 0 ) * ((qpoly k,z) . ((i + 1) -' 1)) by A6, 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 ;
A10: (i + 1) - 2 = i - 1 ;

A11: now

assume i <> 0 ; :: thesis: fp /. 2 = (qpoly k,z) . (i -' 1)
then i > 0 ;
then A12: 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 A5, A12, NAT_1:13;
then 2 in Seg (len fp) ;
then A13: 2 in dom fp by FINSEQ_1:def 3;
then A14: fp . 2 = ((rpoly 1,z) . (2 -' 1)) * ((qpoly k,z) . ((i + 1) -' 2)) by A5
.= ((rpoly 1,z) . 1) * ((qpoly k,z) . ((i + 1) -' 2)) by A7, 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 A13, PARTFUN1:def 8
.= (qpoly k,z) . (i -' 1) by A14, XREAL_0:def 2 ; :: thesis: verum

end;

A15: now

let j be Element of NAT ; :: thesis: ( j in dom fp & j <> 1 & j <> 2 implies fp . j = 0. L )
assume A16: ( j in dom fp & j <> 1 & j <> 2 ) ; :: thesis: fp . j = 0. L
then A17: j in Seg (len fp) by FINSEQ_1:def 3;
A18: fp . j = ((rpoly 1,z) . (j -' 1)) * ((qpoly k,z) . ((i + 1) -' j)) by A5, A16;

now

assume A19: ( 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 A16, A19; :: 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 (rpoly 1,z) . (j -' 1) = 0. L by Lm12;
hence fp . j = 0. L by A18, VECTSP_1:39; :: thesis: verum

end;

A20: now

assume i <> 0 ; :: thesis: ((rpoly 1,z) *' (qpoly k,z)) . i = (fp /. 1) + (fp /. 2)
then i > 0 ;
then A21: i + 1 > 0 + 1 by XREAL_1:10;
then A22: i >= 1 by NAT_1:13;
consider g1, g2 being FinSequence of L such that
A23: ( len g1 = 1 & len g2 = i & fp = g1 ^ g2 ) by A5, FINSEQ_2:26;
1 in Seg (len g2) by A22, A23;
then A24: 1 in dom g2 by FINSEQ_1:def 3;
A25: 1 + 1 = 2 ;
1 + 1 <= len fp by A5, A21, NAT_1:13;
then 2 in Seg (len fp) ;
then A26: 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 A27: ( i in dom g2 & i <> 1 ) ; :: thesis: g2 /. i = 0. L
then A28: i in Seg (len g2) by FINSEQ_1:def 3;
then A29: ( 1 <= i & i <= len g2 ) by FINSEQ_1:3;
then A30: g2 . i = fp . (i + 1) by A23, FINSEQ_1:86;
len fp = 1 + (len g2) by A23, FINSEQ_1:35;
then ( 1 <= i + 1 & i + 1 <= len fp ) by A29, NAT_1:11, XREAL_1:8;
then i + 1 in Seg (len fp) ;
then A31: i + 1 in dom fp by FINSEQ_1:def 3;
( i + 1 <> 0 + 1 & i + 1 <> 2 ) by A27, A28, FINSEQ_1:3;
then fp . (i + 1) = 0. L by A15, A31;
hence g2 /. i = 0. L by A27, A30, PARTFUN1:def 8; :: thesis: verum

end;

then A32: Sum g2 = g2 /. 1 by A24, POLYNOM2:5
.= g2 . 1 by A24, PARTFUN1:def 8
.= fp . 2 by A22, A23, A25, FINSEQ_1:86
.= fp /. 2 by A26, PARTFUN1:def 8 ;
A33: g1 = <*(g1 . 1)*> by A23, FINSEQ_1:57
.= <*(fp . 1)*> by A23, FINSEQ_1:85
.= <*(fp /. 1)*> by A8, PARTFUN1:def 8 ;
thus ((rpoly 1,z) *' (qpoly k,z)) . i = (Sum g1) + (fp /. 2) by A5, A23, A32, RLVECT_1:58
.= (fp /. 1) + (fp /. 2) by A33, RLVECT_1:61 ; :: thesis: verum

end;

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

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

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

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

A36: ( (k - 0 ) - 1 = k1 & k1 + 1 = k ) ;
fp = <*(fp . 1)*> by A5, A35, FINSEQ_1:57
.= <*(fp /. 1)*> by A8, PARTFUN1:def 8 ;
hence ((rpoly 1,z) *' (qpoly k,z)) . i' = (- z) * ((qpoly k,z) . 0 ) by A5, A9, A35, RLVECT_1:61
.= (- z) * ((power L) . z,k1) by A36, Def4
.= - (z * ((power L) . z,k1)) by VECTSP_1:41
.= - ((power L) . z,k) by A36, GROUP_1:def 8
.= (rpoly k,z) . i' by A1, A35, Lm11 ;
:: thesis: verum

end;

suppose A37: 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 A38: i -' 1 = i - 1 by XREAL_0:def 2;
k - i > i - i by A34, XREAL_1:11;
then reconsider ki = k - i as Element of NAT by INT_1:16;
ki > i - i by A34, 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;
A39: (k - (i -' 1)) - 1 = k - i by A38;
k - 1 < k - 0 by XREAL_1:12;
then ( i - 1 < k - 1 & k - 1 < k ) by A34, XREAL_1:11;
then A40: i - 1 < k by XXREAL_0:2;
A41: ki1 + 1 = ki ;
thus ((rpoly 1,z) *' (qpoly k,z)) . i' = ((- z) * ((power L) . z,ki1)) + ((qpoly k,z) . (i -' 1)) by A9, A11, A20, A34, A37, Def4
.= ((- z) * ((power L) . z,ki1)) + ((power L) . z,ki) by A39, A40, Def4
.= (- (z * ((power L) . z,ki1))) + ((power L) . z,ki) by VECTSP_1:41
.= (- ((power L) . z,ki)) + ((power L) . z,ki) by A41, GROUP_1:def 8
.= 0. L by RLVECT_1:16
.= (rpoly k,z) . i' by A34, A37, Lm12 ; :: thesis: verum

end;

end;

end;

suppose A42: 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 A43: i -' 1 = i - 1 by XREAL_0:def 2;
A44: (k - k1) - 1 = 0 ;
fp /. 1 = (- z) * (0. L) by A9, A42, Def4
.= 0. L by VECTSP_1:36 ;
hence ((rpoly 1,z) *' (qpoly k,z)) . i' = (qpoly k,z) . k1 by A11, A20, A42, A43, ALGSTR_1:def 5
.= (power L) . z,0 by A3, A44, Def4
.= 1_ L by GROUP_1:def 8
.= (rpoly k,z) . i' by A1, A42, Lm11 ;
:: thesis: verum

end;

suppose A45: 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 A46: i -' 1 = i - 1 by XREAL_0:def 2;
i >= k + 1 by A45, NAT_1:13;
then A47: i - 1 >= (k + 1) - 1 by XREAL_1:11;
fp /. 1 = (- z) * (0. L) by A9, A45, Def4
.= 0. L by VECTSP_1:36 ;
hence ((rpoly 1,z) *' (qpoly k,z)) . i' = (qpoly k,z) . (i -' 1) by A11, A20, A45, ALGSTR_1:def 5
.= 0. L by A46, A47, Def4
.= (rpoly k,z) . i' by A45, Lm12 ;
:: thesis: verum

end;

end;

end;

hence (rpoly 1,z) *' (qpoly k,z) = rpoly k,z by A4, FUNCT_1:9; :: thesis: verum