let R be Ring; :: thesis: for a, b being Element of R holds (a | R) *' (b | R) = (a * b) | R
let a, b be Element of R; :: thesis: (a | R) *' (b | R) = (a * b) | R
set p = a | R;
set q = b | R;

now :: thesis: for x being object st x in NAT holds
((a | R) *' (b | R)) . x = ((a * b) | R) . x

let x be object ; :: thesis: ( x in NAT implies ((a | R) *' (b | R)) . b₁ = ((a * b) | R) . b₁ )
assume x in NAT ; :: thesis: ((a | R) *' (b | R)) . b₁ = ((a * b) | R) . b₁
then reconsider i = x as Element of NAT ;
consider F being FinSequence of the carrier of R such that
H: ( len F = i + 1 & ((a | R) *' (b | R)) . i = Sum F & ( for k being Element of NAT st k in dom F holds
F . k = ((a | R) . (k -' 1)) * ((b | R) . ((i + 1) -' k)) ) ) by POLYNOM3:def 9;

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

suppose A: i = 0 ; :: thesis: ((a | R) *' (b | R)) . b₁ = ((a * b) | R) . b₁

then 1 in Seg (len F) by H, FINSEQ_1:1;
then 1 in dom F by FINSEQ_1:def 3;
then F . 1 = ((a | R) . ((0 + 1) -' 1)) * ((b | R) . ((i + 1) -' 1)) by H
.= ((a | R) . 0) * ((b | R) . ((i + 1) -' 1)) by NAT_D:34
.= ((a | R) . 0) * ((b | R) . 0) by NAT_D:34, A
.= a * ((b | R) . 0) by Th28
.= a * b by Th28 ;
then F = <*(a * b)*> by FINSEQ_1:40, A, H;
hence ((a | R) *' (b | R)) . x = a * b by H, RLVECT_1:44
.= ((a * b) | R) . x by A, Th28 ;
:: thesis: verum

end;

suppose A: i > 0 ; :: thesis: ((a | R) *' (b | R)) . b₁ = ((a * b) | R) . b₁

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

let j be Element of NAT ; :: thesis: ( j in dom F implies 0. R = F . j )
assume B: j in dom F ; :: thesis: 0. R = F . j
then j in Seg (len F) by FINSEQ_1:def 3;
then C: ( 1 <= j & j <= i + 1 ) by H, FINSEQ_1:1;
( (a | R) . (j -' 1) = 0. R or (b | R) . ((i + 1) -' j) = 0. R )

proof

assume (a | R) . (j -' 1) <> 0. R ; :: thesis: (b | R) . ((i + 1) -' j) = 0. R
then j <= 1 by NAT_D:36, Th28;
then j = 1 by C, XXREAL_0:1;
then (i + 1) -' j = i by NAT_D:34;
hence (b | R) . ((i + 1) -' j) = 0. R by A, Th28; :: thesis: verum

end;

hence 0. R = ((a | R) . (j -' 1)) * ((b | R) . ((i + 1) -' j))
.= F . j by B, H ;
:: thesis: verum

end;

hence ((a | R) *' (b | R)) . x = 0. R by H, POLYNOM3:1
.= ((a * b) | R) . x by A, Th28 ;
:: thesis: verum

end;

end;

end;

hence (a | R) *' (b | R) = (a * b) | R by FUNCT_2:12; :: thesis: verum