for x being Prime st x in support (A -bag) holds
ex n being Nat st
( 0 < n & (A -bag) . x = x |^ n )

proof

let x be Prime; :: thesis: ( x in support (A -bag) implies ex n being Nat st
( 0 < n & (A -bag) . x = x |^ n ) )
assume x in support (A -bag) ; :: thesis: ex n being Nat st
( 0 < n & (A -bag) . x = x |^ n )
then (A -bag) . x = x |^ 1 by BagValue;
hence ex n being Nat st
( 0 < n & (A -bag) . x = x |^ n ) ; :: thesis: verum

end;

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