let n be Ordinal; :: thesis: for i being Nat
for b, b1, b2 being bag of n st i > 1 & i < len (decomp b) & (decomp b) /. i = <*b1,b2*> holds
( b1 <> EmptyBag n & b2 <> EmptyBag n )
let i be Nat; :: thesis: for b, b1, b2 being bag of n st i > 1 & i < len (decomp b) & (decomp b) /. i = <*b1,b2*> holds
( b1 <> EmptyBag n & b2 <> EmptyBag n )
let b, b1, b2 be bag of n; :: thesis: ( i > 1 & i < len (decomp b) & (decomp b) /. i = <*b1,b2*> implies ( b1 <> EmptyBag n & b2 <> EmptyBag n ) )
assume that
A1: ( i > 1 & i < len (decomp b) ) and
A2: (decomp b) /. i = <*b1,b2*> ; :: thesis: ( b1 <> EmptyBag n & b2 <> EmptyBag n )
reconsider p = (divisors b) /. i as bag of n ;
A3: i in dom (decomp b) by A1, FINSEQ_3:25;
then A4: (decomp b) /. i = <*p,(b -' p)*> by Def16;
then A5: b2 = b -' p by A2, FINSEQ_1:77;
A6: dom (decomp b) = dom (divisors b) by Def16;
then A7: len (decomp b) = len (divisors b) by FINSEQ_3:29;
b1 = p by A2, A4, FINSEQ_1:77;
hence b1 <> EmptyBag n by A1, A7, Th64; :: thesis: b2 <> EmptyBag n
assume b2 = EmptyBag n ; :: thesis: contradiction
then p = b by A6, A3, A5, Th55, Th62;
hence contradiction by A1, A7, Th64; :: thesis: verum