let a be Element of R; :: thesis: ( a is factorizable implies a is uniquely_factorizable )
assume AS: a is factorizable ; :: thesis: a is uniquely_factorizable
hence a is factorizable ; :: according to RING_2:def 14 :: thesis: for F, G being Factorization of a ex B being Function of (dom F),(dom G) st
( B is bijective & ( for i being Element of dom F holds G . (B . i) is_associated_to F . i ) )
let F, G be Factorization of a; :: thesis: ex B being Function of (dom F),(dom G) st
( B is bijective & ( for i being Element of dom F holds G . (B . i) is_associated_to F . i ) )
( F is_a_factorization_of a & G is_a_factorization_of a ) by AS, ddf;
hence ex B being Function of (dom F),(dom G) st
( B is bijective & ( for i being Element of dom F holds G . (B . i) is_associated_to F . i ) ) by lemfactunique; :: thesis: verum