:: The Correspondence Between Monotonic Many Sorted Signatures and Well-Founded Graphs. {P}art {II} :: by Czes{\l}aw Byli\'nski and Piotr Rudnicki :: :: Received April 10, 1996 :: Copyright (c) 1996-2012 Association of Mizar Users
uniqueness
for b1, b2 being set st ( for x being set holds ( x in b1 iff ex op, v being set st ( x =[op,v] & op in the carrier' of S & v in the carrier of S & ex n being Nat ex args being Element of the carrier of S * st ( the Arity of S . op = args & n indom args & args . n = v ) ) ) ) & ( for x being set holds ( x in b2 iff ex op, v being set st ( x =[op,v] & op in the carrier' of S & v in the carrier of S & ex n being Nat ex args being Element of the carrier of S * st ( the Arity of S . op = args & n indom args & args . n = v ) ) ) ) holds b1= b2