let n be Ordinal; :: thesis: for i being Nat
for b, b1, b2 being bag of 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 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 ; :: thesis: ( i > 1 & i < len (decomp b) & (decomp b) /. i = <*b1,b2*> implies ( b1 <> EmptyBag n & b2 <> EmptyBag n ) )
assume that
A1: i > 1 and
A2: i < len (decomp b) and
A3: (decomp b) /. i = <*b1,b2*> ; :: thesis: ( b1 <> EmptyBag n & b2 <> EmptyBag n )
A4: dom (decomp b) = dom (divisors b) by Def19;
then A5: len (decomp b) = len (divisors b) by FINSEQ_3:31;
reconsider p = (divisors b) /. i as bag of by Def14;
A6: i in dom (decomp b) by A1, A2, FINSEQ_3:27;
then (decomp b) /. i = <*p,(b -' p)*> by Def19;
then A7: ( b1 = p & b2 = b -' p ) by A3, GROUP_7:2;
hence b1 <> EmptyBag n by A1, A2, A5, Th70; :: thesis: b2 <> EmptyBag n
assume b2 = EmptyBag n ; :: thesis: contradiction
then p = b by A4, A6, A7, Th61, Th68;
hence contradiction by A1, A2, A5, Th70; :: thesis: verum