let ps, pt, f be bag of SetPrimes ; :: thesis: ( ps is prime-factorization-like & pt is prime-factorization-like & f = ps + pt & support ps misses support pt implies f is prime-factorization-like )
assume A1: ps is prime-factorization-like ; :: thesis: ( not pt is prime-factorization-like or not f = ps + pt or not support ps misses support pt or f is prime-factorization-like )
assume A2: pt is prime-factorization-like ; :: thesis: ( not f = ps + pt or not support ps misses support pt or f is prime-factorization-like )
assume A3: f = ps + pt ; :: thesis: ( not support ps misses support pt or f is prime-factorization-like )
assume A4: support ps misses support pt ; :: thesis:
A5: support f = (support ps) \/ (support pt) by ;
for x being Prime st x in support f holds
ex n being Nat st
( 0 < n & f . x = x |^ n )
proof
let x be Prime; :: thesis: ( x in support f implies ex n being Nat st
( 0 < n & f . x = x |^ n ) )

assume A6: x in support f ; :: thesis: ex n being Nat st
( 0 < n & f . x = x |^ n )

per cases ( x in support ps or x in support pt ) by ;
suppose A7: x in support ps ; :: thesis: ex n being Nat st
( 0 < n & f . x = x |^ n )

ps . x = f . x by A3, A4, A7, Th3;
hence ex n being Nat st
( 0 < n & f . x = x |^ n ) by ; :: thesis: verum
end;
suppose A8: x in support pt ; :: thesis: ex n being Nat st
( 0 < n & f . x = x |^ n )

pt . x = f . x by A3, A4, A8, Th4;
hence ex n being Nat st
( 0 < n & f . x = x |^ n ) by ; :: thesis: verum
end;
end;
end;
hence f is prime-factorization-like by INT_7:def 1; :: thesis: verum