let T be Polish-language; :: thesis:
let A be Polish-arity-function of T; :: thesis:
let D be non empty set ; :: thesis:
let f be Polish-recursion-function of A,D; :: thesis:
let K1, K2 be Function of (Polish-WFF-set (T,A)),D; :: thesis:
assume that
A1: K1 is f -recursive and
A2: K2 is f -recursive ; :: thesis:
set W = Polish-WFF-set (T,A);
set X = { F where F is Polish-WFF of T,A : K1 . F = K2 . F } ;
for a being object st a in { F where F is Polish-WFF of T,A : K1 . F = K2 . F } holds
a in Polish-WFF-set (T,A)

let a be object ; :: thesis:
assume a in { F where F is Polish-WFF of T,A : K1 . F = K2 . F } ; :: thesis:
then consider F being Polish-WFF of T,A such that
A3: a = F and
K1 . F = K2 . F ;
thus a in Polish-WFF-set (T,A) by A3; :: thesis:

end;

then A4: { F where F is Polish-WFF of T,A : K1 . F = K2 . F } c= Polish-WFF-set (T,A) ;
then reconsider X = { F where F is Polish-WFF of T,A : K1 . F = K2 . F } as antichain-like Subset of (T *) by XBOOLE_1:1;
ex p being FinSequence st p in X

not Polish-atoms (T,A) is empty ;
then consider a being object such that
B1: a in Polish-atoms (T,A) ;
reconsider a = a as Polish-WFF of T,A by B1, Th34, TARSKI:def 3;
take a ; :: thesis:
K1 . a = K2 . a by Lm71, A1, A2, B1;
hence a in X ; :: thesis:

end;

then reconsider X = X as Polish-language of T ;
A15: for a being object st a in X holds
K1 . a = K2 . a

let a be object ; :: thesis:
assume a in X ; :: thesis:
then consider F being Polish-WFF of T,A such that
A16: a = F and
A17: K1 . F = K2 . F ;
thus K1 . a = K2 . a by A16, A17; :: thesis:

end;

for p being FinSequence
for n being Nat
for q being FinSequence st p in dom A & n = A . p & q in X ^^ n holds
p ^ q in X

end;