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;

.= p *' q by B0, B1, POLYNOM3:def 10 ;

hence p *' q is Ppoly of R by A, dpp1; :: thesis: verum

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)

Product (Fp ^ Fq) =
(Product Fp) * (Product Fq)
by GROUP_4:5
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,b_{2}) )

assume AS: i in dom (Fp ^ Fq) ; :: thesis: ex a being Element of R st (Fp ^ Fq) . a = rpoly (1,b_{2})

end;assume AS: i in dom (Fp ^ Fq) ; :: thesis: ex a being Element of R st (Fp ^ Fq) . a = rpoly (1,b

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;

end;

( 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,b_{2})

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;hence ex a being Element of R st (Fp ^ Fq) . i = rpoly (1,a) by B0, B2; :: thesis: verum

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,b_{2})

( n in dom Fq & i = (len Fp) + n ) ; :: thesis: ex a being Element of R st (Fp ^ Fq) . a = rpoly (1,b

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;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

.= p *' q by B0, B1, POLYNOM3:def 10 ;

hence p *' q is Ppoly of R by A, dpp1; :: thesis: verum