let R be non degenerated comRing; :: thesis: for a, b being non zero Element of R
for n, m being Nat holds (anpoly (a,n)) *' (anpoly (b,m)) = anpoly ((a * b),(n + m))
let a, b be non zero Element of R; :: thesis: for n, m being Nat holds (anpoly (a,n)) *' (anpoly (b,m)) = anpoly ((a * b),(n + m))
let n, m be Nat; :: thesis: (anpoly (a,n)) *' (anpoly (b,m)) = anpoly ((a * b),(n + m))
set p = anpoly (a,n);
set q = anpoly (b,m);
set r = anpoly ((a * b),(n + m));

per cases ( n = 0 or m = 0 or ( n <> 0 & m <> 0 ) ) ;

suppose A1: n = 0 ; :: thesis: (anpoly (a,n)) *' (anpoly (b,m)) = anpoly ((a * b),(n + m))

hence (anpoly (a,n)) *' (anpoly (b,m)) = (a | R) *' (anpoly (b,m))
.= (a * (1_. R)) *' (anpoly (b,m)) by RING_4:16
.= a * ((1_. R) *' (anpoly (b,m))) by RING_4:10
.= anpoly ((a * b),(n + m)) by A1, Th10 ;
:: thesis: verum

end;

suppose A2: m = 0 ; :: thesis: (anpoly (a,n)) *' (anpoly (b,m)) = anpoly ((a * b),(n + m))

hence (anpoly (a,n)) *' (anpoly (b,m)) = (anpoly (a,n)) *' (b | R)
.= (anpoly (a,n)) *' (b * (1_. R)) by RING_4:16
.= b * ((anpoly (a,n)) *' (1_. R)) by RING_4:10
.= anpoly ((a * b),(n + m)) by A2, Th10 ;
:: thesis: verum

end;

suppose A3: ( n <> 0 & m <> 0 ) ; :: thesis: (anpoly (a,n)) *' (anpoly (b,m)) = anpoly ((a * b),(n + m))

then A4: ( n >= 0 + 1 & m >= 0 + 1 ) by NAT_1:13;

now :: thesis: for i being Element of NAT holds (anpoly ((a * b),(n + m))) . i = ((anpoly (a,n)) *' (anpoly (b,m))) . i

let i be Element of NAT ; :: thesis: (anpoly ((a * b),(n + m))) . b₁ = ((anpoly (a,n)) *' (anpoly (b,m))) . b₁
consider F being FinSequence of the carrier of R such that
A5: ( len F = i + 1 & ((anpoly (a,n)) *' (anpoly (b,m))) . i = Sum F & ( for k being Element of NAT st k in dom F holds
F . k = ((anpoly (a,n)) . (k -' 1)) * ((anpoly (b,m)) . ((i + 1) -' k)) ) ) by POLYNOM3:def 9;
A6: for k being Element of NAT st k in dom F & k <> len (anpoly (a,n)) holds
F /. k = 0. R

proof

let k be Element of NAT ; :: thesis: ( k in dom F & k <> len (anpoly (a,n)) implies F /. k = 0. R )
assume A7: ( k in dom F & k <> len (anpoly (a,n)) ) ; :: thesis: F /. k = 0. R
A8: deg (anpoly (a,n)) = n by Lm1;

now :: thesis: not k -' 1 = n

assume A9: k -' 1 = n ; :: thesis: contradiction
then k - 1 = k -' 1 by A3, XREAL_0:def 2;
hence contradiction by A7, A9, A8; :: thesis: verum

end;

then A10: (anpoly (a,n)) . (k -' 1) = 0. R by POLYDIFF:25;
thus F /. k = F . k by A7, PARTFUN1:def 6
.= (0. R) * ((anpoly (b,m)) . ((i + 1) -' k)) by A10, A7, A5
.= 0. R ; :: thesis: verum

end;

A11: dom F = Seg (i + 1) by FINSEQ_1:def 3, A5;

per cases ( i = n + m or i <> n + m ) ;

suppose A12: i = n + m ; :: thesis: (anpoly ((a * b),(n + m))) . b₁ = ((anpoly (a,n)) *' (anpoly (b,m))) . b₁

A13: deg (anpoly (a,n)) = n by Lm1;
then A14: len (anpoly (a,n)) <= (n + 1) + m by NAT_1:11;
A15: dom F = Seg ((n + m) + 1) by A12, A5, FINSEQ_1:def 3;
((len (anpoly (a,n))) - 1) + 1 >= 1 + 1 by A13, A4, XREAL_1:6;
then A16: 1 <= len (anpoly (a,n)) by XXREAL_0:2;
A17: (len (anpoly (a,n))) -' 1 = n by A13, XREAL_0:def 2;
m = (i + 1) - (len (anpoly (a,n))) by A13, A12;
then A18: (i + 1) -' (len (anpoly (a,n))) = m by XREAL_0:def 2;
Sum F = F /. (len (anpoly (a,n))) by A16, A6, A14, A15, FINSEQ_1:1, POLYNOM2:3
.= F . (len (anpoly (a,n))) by A16, A14, A15, FINSEQ_1:1, PARTFUN1:def 6
.= ((anpoly (a,n)) . n) * ((anpoly (b,m)) . m) by A16, A14, A15, FINSEQ_1:1, A17, A18, A5
.= a * ((anpoly (b,m)) . m) by POLYDIFF:24
.= a * b by POLYDIFF:24 ;
hence (anpoly ((a * b),(n + m))) . i = ((anpoly (a,n)) *' (anpoly (b,m))) . i by A5, A12, POLYDIFF:24; :: thesis: verum

end;

suppose A19: i <> n + m ; :: thesis: (anpoly ((a * b),(n + m))) . b₁ = ((anpoly (a,n)) *' (anpoly (b,m))) . b₁

Sum F = 0. R

proof

per cases ( i < (len (anpoly (a,n))) - 1 or i >= (len (anpoly (a,n))) - 1 ) ;

suppose i < (len (anpoly (a,n))) - 1 ; :: thesis: Sum F = 0. R

then A20: i + 1 < ((len (anpoly (a,n))) - 1) + 1 by XREAL_1:6;

now :: thesis: for k being Element of NAT st k in dom F holds
0. R = F . k

let k be Element of NAT ; :: thesis: ( k in dom F implies 0. R = F . k )
assume A21: k in dom F ; :: thesis: 0. R = F . k
then ( 1 <= k & k <= i + 1 ) by A11, FINSEQ_1:1;
hence 0. R = F /. k by A20, A21, A6
.= F . k by A21, PARTFUN1:def 6 ;
:: thesis: verum

end;

hence Sum F = 0. R by POLYNOM3:1; :: thesis: verum

end;

suppose A22: i >= (len (anpoly (a,n))) - 1 ; :: thesis: Sum F = 0. R

now :: thesis: for k being Element of NAT st k in dom F holds
0. R = F . k

let k be Element of NAT ; :: thesis: ( k in dom F implies 0. R = F . b₁ )
assume A23: k in dom F ; :: thesis: 0. R = F . b₁

per cases ( k <> len (anpoly (a,n)) or k = len (anpoly (a,n)) ) ;

suppose k <> len (anpoly (a,n)) ; :: thesis: 0. R = F . b₁

hence 0. R = F /. k by A23, A6
.= F . k by A23, PARTFUN1:def 6 ;
:: thesis: verum

end;

suppose A24: k = len (anpoly (a,n)) ; :: thesis: F . b₁ = 0. R

A25: deg (anpoly (a,n)) = n by Lm1;
i + 1 >= ((len (anpoly (a,n))) - 1) + 1 by A22, XREAL_1:6;
then (i + 1) - (len (anpoly (a,n))) >= (len (anpoly (a,n))) - (len (anpoly (a,n))) by XREAL_1:6;
then (i + 1) -' (len (anpoly (a,n))) = i - n by A25, XREAL_0:def 2;
then A26: (i + 1) -' (len (anpoly (a,n))) <> m by A19;
thus F . k = ((anpoly (a,n)) . ((len (anpoly (a,n))) -' 1)) * ((anpoly (b,m)) . ((i + 1) -' (len (anpoly (a,n))))) by A5, A23, A24
.= ((anpoly (a,n)) . ((len (anpoly (a,n))) -' 1)) * (0. R) by A26, POLYDIFF:25
.= 0. R ; :: thesis: verum

end;

end;

end;

hence Sum F = 0. R by POLYNOM3:1; :: thesis: verum

end;

end;

end;

hence (anpoly ((a * b),(n + m))) . i = ((anpoly (a,n)) *' (anpoly (b,m))) . i by A5, A19, POLYDIFF:25; :: thesis: verum

end;

end;

end;

hence (anpoly (a,n)) *' (anpoly (b,m)) = anpoly ((a * b),(n + m)) ; :: thesis: verum

end;

end;