let R be non almost_left_invertible factorial domRing; :: thesis: for a being non zero NonUnit of R ex b being Element of R st b is_a_irreducible_factor_of a
let a be non zero NonUnit of R; :: thesis: ex b being Element of R st b is_a_irreducible_factor_of a
consider F being non empty FinSequence of R such that
A1: F is_a_factorization_of a by RING_2:def 12;
len F <> 0 ;
then consider G being FinSequence of R, d being Element of R such that
A2: F = G ^ <*d*> by FINSEQ_2:19;
take d ; :: thesis: d is_a_irreducible_factor_of a
(Product G) * (Product <*d*>) = a by A1, A2, GROUP_4:5;
then A3: Product <*d*> divides a by GCD_1:def 1;
reconsider lf = len F as Element of dom F by FINSEQ_5:6;
len F = (len G) + (len <*d*>) by A2, FINSEQ_1:22
.= (len G) + 1 by FINSEQ_1:39 ;
then F . lf = d by A2, FINSEQ_1:42;
hence d is_a_irreducible_factor_of a by A1, A3, GROUP_4:9; :: thesis: verum