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: f is prime-factorization-like
A5: support f = (support ps) \/ (support pt) by A3, PRE_POLY:38;
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 A6, A5, XBOOLE_0:def 3;

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 A7, A1, INT_7:def 1; :: 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 A8, A2, INT_7:def 1; :: thesis: verum

end;

end;

end;

hence f is prime-factorization-like by INT_7:def 1; :: thesis: verum