let R be non empty right_unital doubleLoopStr ; :: thesis: for a being Element of R holds
( a is irreducible iff <*a*> is_a_factorization_of a )
let a be Element of R; :: thesis: ( a is irreducible iff <*a*> is_a_factorization_of a )
rng <*a*> c= the carrier of R ;
then reconsider f = <*a*> as Function of (dom <*a*>),R by FUNCT_2:2;
A: now :: thesis: ( a is irreducible implies <*a*> is_a_factorization_of a )
assume AS: a is irreducible ; :: thesis: <*a*> is_a_factorization_of a
now :: thesis: for i being Element of dom <*a*> holds <*a*> . i is irreducible
let i be Element of dom <*a*>; :: thesis: <*a*> . i is irreducible
i in dom <*a*> ;
then i in Seg 1 by FINSEQ_1:38;
then i = 1 by TARSKI:def 1, FINSEQ_1:2;
hence <*a*> . i is irreducible by AS, FINSEQ_1:40; :: thesis: verum
end;
hence <*a*> is_a_factorization_of a by GROUP_4:9; :: thesis: verum
end;
now :: thesis: ( <*a*> is_a_factorization_of a implies a is irreducible )
assume AS: <*a*> is_a_factorization_of a ; :: thesis: a is irreducible
dom <*a*> = {1} by FINSEQ_1:2, FINSEQ_1:38;
then reconsider e = 1 as Element of dom <*a*> by TARSKI:def 1;
f . e = a by FINSEQ_1:40;
hence a is irreducible by AS; :: thesis: verum
end;
hence ( a is irreducible iff <*a*> is_a_factorization_of a ) by A; :: thesis: verum