set U = Polish-ext-domain (B,J);
let A, D be Polish-arity-function of Polish-ext-domain (B,J); :: thesis: ( J = Polish-WFF-set ((Polish-ext-domain (B,J)),A) & J = Polish-WFF-set ((Polish-ext-domain (B,J)),D) implies A = D )
assume ( J = Polish-WFF-set ((Polish-ext-domain (B,J)),A) & J = Polish-WFF-set ((Polish-ext-domain (B,J)),D) ) ; :: thesis: A = D
hence A = Polish-arity (Polish-WFF-set ((Polish-ext-domain (B,J)),D))
.= D ;
:: thesis: verum