let n be Ordinal; :: thesis: for R being non degenerated Ring
for a, b being Element of R holds (a | (n,R)) *' (b | (n,R)) = (a * b) | (n,R)
let L be non degenerated Ring; :: thesis: for a, b being Element of L holds (a | (n,L)) *' (b | (n,L)) = (a * b) | (n,L)
let a, b be Element of L; :: thesis: (a | (n,L)) *' (b | (n,L)) = (a * b) | (n,L)
set p = (a * b) | (n,L);
set q = (a | (n,L)) *' (b | (n,L));
set ap = a | (n,L);
set bp = b | (n,L);

A2: now :: thesis: for x being object st x in dom ((a * b) | (n,L)) holds
((a | (n,L)) *' (b | (n,L))) . x = ((a * b) | (n,L)) . x

let x be object ; :: thesis: ( x in dom ((a * b) | (n,L)) implies ((a | (n,L)) *' (b | (n,L))) . b₁ = ((a * b) | (n,L)) . b₁ )
assume x in dom ((a * b) | (n,L)) ; :: thesis: ((a | (n,L)) *' (b | (n,L))) . b₁ = ((a * b) | (n,L)) . b₁
then reconsider i = x as Element of Bags n ;
consider s being FinSequence of the carrier of L such that
A3: ( ((a | (n,L)) *' (b | (n,L))) . i = Sum s & len s = len (decomp i) & ( for k being Element of NAT st k in dom s holds
ex b1, b2 being bag of n st
( (decomp i) /. k = <*b1,b2*> & s /. k = ((a | (n,L)) . b1) * ((b | (n,L)) . b2) ) ) ) by POLYNOM1:def 10;

per cases ( i <> EmptyBag n or i = EmptyBag n ) ;

suppose H0: i <> EmptyBag n ; :: thesis: ((a | (n,L)) *' (b | (n,L))) . b₁ = ((a * b) | (n,L)) . b₁

H1: for b1, b2 being bag of n st ( b1 <> EmptyBag n or b2 <> EmptyBag n ) holds
((a | (n,L)) . b1) * ((b | (n,L)) . b2) = 0. L

proof

let b1, b2 be bag of n; :: thesis: ( ( b1 <> EmptyBag n or b2 <> EmptyBag n ) implies ((a | (n,L)) . b1) * ((b | (n,L)) . b2) = 0. L )
assume ( b1 <> EmptyBag n or b2 <> EmptyBag n ) ; :: thesis: ((a | (n,L)) . b1) * ((b | (n,L)) . b2) = 0. L

per cases then ( b1 <> EmptyBag n or b2 <> EmptyBag n ) ;

suppose b1 <> EmptyBag n ; :: thesis: ((a | (n,L)) . b1) * ((b | (n,L)) . b2) = 0. L

then (a | (n,L)) . b1 = 0. L by POLYNOM7:18;
hence ((a | (n,L)) . b1) * ((b | (n,L)) . b2) = 0. L ; :: thesis: verum

end;

suppose b2 <> EmptyBag n ; :: thesis: ((a | (n,L)) . b1) * ((b | (n,L)) . b2) = 0. L

then (b | (n,L)) . b2 = 0. L by POLYNOM7:18;
hence ((a | (n,L)) . b1) * ((b | (n,L)) . b2) = 0. L ; :: thesis: verum

end;

end;

end;

1 <= len (decomp i) by NAT_1:14;
then 1 in Seg (len s) by A3;
then H2: 1 in dom s by FINSEQ_1:def 3;
H3: for k being Element of NAT st k in dom s holds
s /. k = 0. L

proof

let k be Element of NAT ; :: thesis: ( k in dom s implies s /. k = 0. L )
assume H4: k in dom s ; :: thesis: s /. k = 0. L
then consider b1, b2 being bag of n such that
H5: ( (decomp i) /. k = <*b1,b2*> & s /. k = ((a | (n,L)) . b1) * ((b | (n,L)) . b2) ) by A3;
H8: dom s = Seg (len (decomp i)) by A3, FINSEQ_1:def 3
.= dom (decomp i) by FINSEQ_1:def 3 ;
then H6: b1 = (divisors i) /. k by H4, H5, PRE_POLY:70;
then (decomp i) /. k = <*b1,(i -' b1)*> by H4, H8, PRE_POLY:def 17;
then H10: b2 = i -' b1 by H5, FINSEQ_1:77;
dom (divisors i) = dom (decomp i) by PRE_POLY:def 17;
then H7: k in Seg (len (divisors i)) by H4, H8, FINSEQ_1:def 3;
then H11: ( 1 <= k & k <= len (divisors i) ) by FINSEQ_1:1;

per cases ( k = 1 or k <> 1 ) ;

suppose k = 1 ; :: thesis: s /. k = 0. L

then b1 = EmptyBag n by H6, PRE_POLY:65;
then b2 = i by H10, PRE_POLY:54;
hence s /. k = 0. L by H0, H1, H5; :: thesis: verum

end;

suppose k <> 1 ; :: thesis: s /. k = 0. L

then H8: 1 < k by H11, XXREAL_0:1;

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

suppose k = len (divisors i) ; :: thesis: s /. k = 0. L

then b1 = i by H6, PRE_POLY:65;
hence s /. k = 0. L by H0, H1, H5; :: thesis: verum

end;

suppose k < len (divisors i) ; :: thesis: s /. k = 0. L

then b1 <> EmptyBag n by H8, H6, PRE_POLY:66;
hence s /. k = 0. L by H5, H1; :: thesis: verum

end;

suppose k > len (divisors i) ; :: thesis: s /. k = 0. L

hence s /. k = 0. L by H7, FINSEQ_1:1; :: thesis: verum

end;

end;

end;

end;

end;

then for k being Element of NAT st k in dom s & k <> 1 holds
s /. k = 0. L ;
then Sum s = s /. 1 by H2, POLYNOM2:3
.= ((a | (n,L)) . i) * (0. L) by H3, H2 ;
hence ((a | (n,L)) *' (b | (n,L))) . x = ((a * b) | (n,L)) . x by H0, A3, POLYNOM7:18; :: thesis: verum

end;

suppose AS: i = EmptyBag n ; :: thesis: ((a | (n,L)) *' (b | (n,L))) . b₁ = ((a * b) | (n,L)) . b₁

then F: decomp i = <*<*(EmptyBag n),(EmptyBag n)*>*> by PRE_POLY:73;
then F1: ( len (decomp i) = 1 & (decomp i) . 1 = <*(EmptyBag n),(EmptyBag n)*> ) by FINSEQ_1:40;
dom (decomp i) = Seg 1 by F, FINSEQ_1:38;
then F2: (decomp i) /. 1 = <*(EmptyBag n),(EmptyBag n)*> by F1, FINSEQ_1:3, PARTFUN1:def 6;
H4: 1 = len s by F, A3, FINSEQ_1:40;
then 1 in Seg (len s) ;
then H3: 1 in dom s by FINSEQ_1:def 3;
then consider b1, b2 being bag of n such that
H2: ( (decomp i) /. 1 = <*b1,b2*> & s /. 1 = ((a | (n,L)) . b1) * ((b | (n,L)) . b2) ) by A3;
s = <*(s . 1)*> by H4, FINSEQ_1:40
.= <*(s /. 1)*> by H3, PARTFUN1:def 6 ;
then Sum s = ((a | (n,L)) . b1) * ((b | (n,L)) . b2) by H2, RLVECT_1:44
.= ((a | (n,L)) . (EmptyBag n)) * ((b | (n,L)) . b2) by F2, H2, FINSEQ_1:77
.= ((a | (n,L)) . (EmptyBag n)) * ((b | (n,L)) . (EmptyBag n)) by F2, H2, FINSEQ_1:77
.= a * ((b | (n,L)) . (EmptyBag n)) by POLYNOM7:18
.= a * b by POLYNOM7:18 ;
hence ((a | (n,L)) *' (b | (n,L))) . x = ((a * b) | (n,L)) . x by AS, A3, POLYNOM7:18; :: thesis: verum

end;

end;

end;

dom ((a * b) | (n,L)) = Bags n by FUNCT_2:def 1;
hence (a | (n,L)) *' (b | (n,L)) = (a * b) | (n,L) by A2; :: thesis: verum