let F be Field; :: thesis: for G being non empty FinSequence of the carrier of (Polynom-Ring F) st ( for i being Nat st i in dom G holds
ex a being Element of F st G . i = rpoly (1,a) ) holds
G is Factorization of Product G
let G be non empty FinSequence of the carrier of (Polynom-Ring F); :: thesis: ( ( for i being Nat st i in dom G holds
ex a being Element of F st G . i = rpoly (1,a) ) implies G is Factorization of Product G )
assume A: for i being Nat st i in dom G holds
ex a being Element of F st G . i = rpoly (1,a) ; :: thesis: G is Factorization of Product G

C: now :: thesis: for i being Element of dom G holds G . i is irreducible

let i be Element of dom G; :: thesis: G . i is irreducible
consider a being Element of F such that
B: G . i = rpoly (1,a) by A;
deg (rpoly (1,a)) = 1 by HURWITZ:27;
hence G . i is irreducible by B, RING_4:42; :: thesis: verum

end;

then B: G is_a_factorization_of Product G by RING_2:def 11;
Product G is factorizable by C, RING_2:def 11, RING_2:def 12;
hence G is Factorization of Product G by B, RING_2:def 13; :: thesis: verum