let a be Element of R; :: thesis: ( a is factorizable implies ( not a is zero & not a is unital ) )
assume a is factorizable ; :: thesis: ( not a is zero & not a is unital )
then consider F being non empty FinSequence of R such that
AS: F is_a_factorization_of a ;
now :: thesis: not a is zero
assume a is zero ; :: thesis: contradiction
then consider i being Nat such that
A: ( i in dom F & F . i = 0. R ) by AS, prod5;
0. R is irreducible by A, AS;
hence contradiction ; :: thesis: verum
end;
hence not a is zero ; :: thesis: not a is unital
rng F c= the carrier of R ;
then reconsider f = F as Function of (dom F),R by FUNCT_2:2;
now :: thesis: not a is unital
assume A1: a is unital ; :: thesis: contradiction
consider q being FinSequence, x being object such that
A2: F = q ^ <*x*> by FINSEQ_1:46;
reconsider q = q as FinSequence of R by A2, FINSEQ_1:36;
rng <*x*> = {x} by FINSEQ_1:39;
then A5: x in rng <*x*> by TARSKI:def 1;
A6: rng <*x*> c= rng F by A2, FINSEQ_1:30;
then x in rng F by A5;
then reconsider x = x as Element of R ;
a = (Product q) * x by GROUP_4:6, A2, AS;
then x divides a ;
then A3: x is unital by A1, GCD_1:2;
consider i being Nat such that
A7: ( i in dom F & F . i = x ) by A5, A6, FINSEQ_2:10;
x is irreducible by AS, A7;
hence contradiction by A3; :: thesis: verum
end;
hence not a is unital ; :: thesis: verum