for F being Field
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