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 )

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

hence
f is prime-factorization-like
by INT_7:def 1; :: thesis: verum
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 )

end;( 0 < n & f . x = x |^ n ) )

assume A6: x in support f ; :: thesis: ex n being Nat st

( 0 < n & f . x = x |^ n )