let U, V be Polish-language of (dom B); :: thesis: ( ex T being Polish-language ex A being Polish-arity-function of T st
( A = B & U = Polish-WFF-set (T,A) ) & ex T being Polish-language ex A being Polish-arity-function of T st
( A = B & V = Polish-WFF-set (T,A) ) implies U = V )
given T1 being Polish-language, A1 being Polish-arity-function of T1 such that A1: A1 = B and
A2: U = Polish-WFF-set (T1,A1) ; :: thesis: ( for T being Polish-language
for A being Polish-arity-function of T holds
( not A = B or not V = Polish-WFF-set (T,A) ) or U = V )
given T2 being Polish-language, A2 being Polish-arity-function of T2 such that A3: A2 = B and
A4: V = Polish-WFF-set (T2,A2) ; :: thesis: U = V
T1 = dom A2 by A1, A3, FUNCT_2:def 1
.= T2 by FUNCT_2:def 1 ;
hence U = V by A1, A2, A3, A4; :: thesis: verum