let R be domRing; :: thesis: for p, q being Ppoly of R holds p *' q is Ppoly of R
let p, q be Ppoly of R; :: thesis: p *' q is Ppoly of R
consider Fp being non empty FinSequence of (Polynom-Ring R) such that
B0: ( p = Product Fp & ( for i being Nat st i in dom Fp holds
ex a being Element of R st Fp . i = rpoly (1,a) ) ) by dpp1;
consider Fq being non empty FinSequence of (Polynom-Ring R) such that
B1: ( q = Product Fq & ( for i being Nat st i in dom Fq holds
ex a being Element of R st Fq . i = rpoly (1,a) ) ) by dpp1;
set G = Fp ^ Fq;
A: now :: thesis: for i being Nat st i in dom (Fp ^ Fq) holds
ex a being Element of R st (Fp ^ Fq) . i = rpoly (1,a)
let i be Nat; :: thesis: ( i in dom (Fp ^ Fq) implies ex a being Element of R st (Fp ^ Fq) . a = rpoly (1,b2) )
assume AS: i in dom (Fp ^ Fq) ; :: thesis: ex a being Element of R st (Fp ^ Fq) . a = rpoly (1,b2)
per cases ( i in dom Fp or ex n being Nat st
( n in dom Fq & i = (len Fp) + n ) ) by AS, FINSEQ_1:25;
suppose B2: i in dom Fp ; :: thesis: ex a being Element of R st (Fp ^ Fq) . a = rpoly (1,b2)
then Fp . i = (Fp ^ Fq) . i by FINSEQ_1:def 7;
hence ex a being Element of R st (Fp ^ Fq) . i = rpoly (1,a) by B0, B2; :: thesis: verum
end;
suppose ex n being Nat st
( n in dom Fq & i = (len Fp) + n ) ; :: thesis: ex a being Element of R st (Fp ^ Fq) . a = rpoly (1,b2)
then consider n being Nat such that
B2: ( n in dom Fq & i = (len Fp) + n ) ;
(Fp ^ Fq) . i = Fq . n by B2, FINSEQ_1:def 7;
hence ex a being Element of R st (Fp ^ Fq) . i = rpoly (1,a) by B1, B2; :: thesis: verum
end;
end;
end;
Product (Fp ^ Fq) = (Product Fp) * (Product Fq) by GROUP_4:5
.= p *' q by B0, B1, POLYNOM3:def 10 ;
hence p *' q is Ppoly of R by A, dpp1; :: thesis: verum