:: Fundamental {T}heorem of {A}rithmetic :: by Artur Korni{\l}owicz and Piotr Rudnicki :: :: Received February 13, 2004 :: Copyright (c) 2004-2012 Association of Mizar Users
uniqueness
for b1, b2 being ManySortedSet of X st ( for i being set holds b1. i = a *(b . i) ) & ( for i being set holds b2. i = a *(b . i) ) holds b1= b2
existence
ex b1 being ManySortedSet of X st for i being set holds ( ( b1 . i <= b2 . i implies b1. i = b1 . i ) & ( b1 . i > b2 . i implies b1. i = b2 . i ) )
uniqueness
for b1, b2 being ManySortedSet of X st ( for i being set holds ( ( b1 . i <= b2 . i implies b1. i = b1 . i ) & ( b1 . i > b2 . i implies b1. i = b2 . i ) ) ) & ( for i being set holds ( ( b1 . i <= b2 . i implies b2. i = b1 . i ) & ( b1 . i > b2 . i implies b2. i = b2 . i ) ) ) holds b1= b2
existence
ex b1 being ManySortedSet of X st for i being set holds ( ( b1 . i <= b2 . i implies b1. i = b2 . i ) & ( b1 . i > b2 . i implies b1. i = b1 . i ) )
uniqueness
for b1, b2 being ManySortedSet of X st ( for i being set holds ( ( b1 . i <= b2 . i implies b1. i = b2 . i ) & ( b1 . i > b2 . i implies b1. i = b1 . i ) ) ) & ( for i being set holds ( ( b1 . i <= b2 . i implies b2. i = b2 . i ) & ( b1 . i > b2 . i implies b2. i = b1 . i ) ) ) holds b1= b2