set U = Polish-ext-domain (B,J);
set S = Polish-ext-complement (B,J);
set V = Polish-WFF-set B;
set T = dom B;
reconsider A = B as Polish-arity-function of dom B by Th1;
set D = ((Polish-ext-domain (B,J)) --> 0) +* B;
A1: Polish-WFF-set B = Polish-WFF-set ((dom B),A) by Def4;
A2: dom (((Polish-ext-domain (B,J)) --> 0) +* B) = (dom ((Polish-ext-domain (B,J)) --> 0)) \/ (dom A) by FUNCT_4:def 1
.= Polish-ext-domain (B,J) by Def9, XBOOLE_1:12 ;
A0: rng A c= rng (((Polish-ext-domain (B,J)) --> 0) +* B) by FUNCT_4:18;
0 in rng A by FREEALG:def 2;
then ((Polish-ext-domain (B,J)) --> 0) +* B is with_zero by A0;
then ((Polish-ext-domain (B,J)) --> 0) +* B is Polish-arity-function by A2, Def2;
then reconsider D = ((Polish-ext-domain (B,J)) --> 0) +* B as Polish-arity-function of Polish-ext-domain (B,J) by A2, Th1;
take D ; :: thesis: J = Polish-WFF-set ((Polish-ext-domain (B,J)),D)
A4: J is -closed ;
A6: for a being object st a in Polish-ext-complement (B,J) holds
( a in dom D & not a in dom A & D . a = 0 )

proof

let a be object ; :: thesis: ( a in Polish-ext-complement (B,J) implies ( a in dom D & not a in dom A & D . a = 0 ) )
assume a in Polish-ext-complement (B,J) ; :: thesis: ( a in dom D & not a in dom A & D . a = 0 )
then A7: ( a in Polish-ext-domain (B,J) & not a in dom B ) by Lm21;
then reconsider p = a as Element of Polish-ext-domain (B,J) ;
thus ( a in dom D & not a in dom A ) by A7, FUNCT_2:def 1; :: thesis: D . a = 0
thus D . a = ((Polish-ext-domain (B,J)) --> 0) . p by A7, FUNCT_4:11
.= 0 ; :: thesis: verum

end;

set X = Polish-WFF-set ((Polish-ext-domain (B,J)),D);
A9: J is -closed

proof

let p be FinSequence; :: according to POLNOT_2:def 6 :: thesis: for n being Nat
for q being FinSequence st p in Polish-ext-domain (B,J) & n = D . p & q in J ^^ n holds
p ^ q in J
let n be Nat; :: thesis: for q being FinSequence st p in Polish-ext-domain (B,J) & n = D . p & q in J ^^ n holds
p ^ q in J
let q be FinSequence; :: thesis: ( p in Polish-ext-domain (B,J) & n = D . p & q in J ^^ n implies p ^ q in J )
assume that
A10: p in Polish-ext-domain (B,J) and
A11: n = D . p and
A12: q in J ^^ n ; :: thesis: p ^ q in J
reconsider p = p as Element of Polish-ext-domain (B,J) by A10;

per cases ( p in dom B or not p in dom B ) ;

suppose A13: p in dom B ; :: thesis: p ^ q in J

then A . p = n by A11, FUNCT_4:13;
hence p ^ q in J by A4, A12, A13; :: thesis: verum

end;

suppose not p in dom B ; :: thesis: p ^ q in J

then A21: p in Polish-ext-complement (B,J) by XBOOLE_0:def 3;
then D . p = 0 by A6;
then q in {{}} by A11, A12, POLNOT_1:6;
then q = {} by TARSKI:def 1;
then p ^ q = p by FINSEQ_1:34;
hence p ^ q in J by A21; :: thesis: verum

end;

end;

end;

for a being object holds
( a in J iff a in Polish-WFF-set ((Polish-ext-domain (B,J)),D) )

proof

defpred S₁[ Nat] means J |` $1 c= Polish-WFF-set ((Polish-ext-domain (B,J)),D);
A30: S₁[ 0 ]

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in J |` 0 or a in Polish-WFF-set ((Polish-ext-domain (B,J)),D) )
assume A31: a in J |` 0 ; :: thesis: a in Polish-WFF-set ((Polish-ext-domain (B,J)),D)
then reconsider p = a as Element of J ;
len p <= 0 by A31, Lm19;
then p = {} ;
then A33: ( J = {{}} & Polish-WFF-set B = {{}} & dom B = {{}} & Polish-ext-complement (B,J) = {} ) by Lm23;
then dom ((Polish-ext-domain (B,J)) --> 0) c= dom A ;
then D = A by FUNCT_4:19;
then p in Polish-WFF-set ((Polish-ext-domain (B,J)),D) by A1, A33;
hence a in Polish-WFF-set ((Polish-ext-domain (B,J)),D) ; :: thesis: verum

end;

A40: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A41: S₁[n] ; :: thesis: S₁[n + 1]
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in J |` (n + 1) or a in Polish-WFF-set ((Polish-ext-domain (B,J)),D) )
assume A42: a in J |` (n + 1) ; :: thesis: a in Polish-WFF-set ((Polish-ext-domain (B,J)),D)
then reconsider p = a as Element of J ;
A43: len p <= n + 1 by A42, Lm19;

per cases ( ( {} in dom B & p is dom B -headed ) or ( not {} in dom B & p is dom B -headed ) or not p is dom B -headed ) ;

suppose ( {} in dom B & p is dom B -headed ) ; :: thesis: a in Polish-WFF-set ((Polish-ext-domain (B,J)),D)

then A44: ( J = {{}} & Polish-WFF-set B = {{}} & dom B = {{}} & Polish-ext-complement (B,J) = {} ) by Lm23;
then dom ((Polish-ext-domain (B,J)) --> 0) c= dom A ;
then D = A by FUNCT_4:19;
then p in Polish-WFF-set ((Polish-ext-domain (B,J)),D) by A1, A44;
hence a in Polish-WFF-set ((Polish-ext-domain (B,J)),D) ; :: thesis: verum

end;

suppose that A50: not {} in dom B and
A51: p is dom B -headed ; :: thesis: a in Polish-WFF-set ((Polish-ext-domain (B,J)),D)

set q = (dom B) -head p;
set r = (dom B) -tail p;
A52: (dom B) -head p in dom B by A51, POLNOT_1:def 22;
then A54: (len ((dom B) -head p)) + (len ((dom B) -tail p)) >= (len ((dom B) -tail p)) + 1 by A50, FINSEQ_1:20, XREAL_1:6;
p = ((dom B) -head p) ^ ((dom B) -tail p) ;
then (len ((dom B) -head p)) + (len ((dom B) -tail p)) <= n + 1 by A43, FINSEQ_1:22;
then (len ((dom B) -tail p)) + 1 <= n + 1 by A54, XXREAL_0:2;
then A56: len ((dom B) -tail p) <= n by XREAL_1:6;
set m = A . ((dom B) -head p);
A57: (J ^^ (A . ((dom B) -head p))) |` n c= (J |` n) ^^ (A . ((dom B) -head p)) by Lm20;
A58: (J |` n) ^^ (A . ((dom B) -head p)) c= (Polish-WFF-set ((Polish-ext-domain (B,J)),D)) ^^ (A . ((dom B) -head p)) by A41, POLNOT_1:17;
J is (A) ;
then (dom B) -tail p in J ^^ (A . ((dom B) -head p)) by A51;
then (dom B) -tail p in (J ^^ (A . ((dom B) -head p))) |` n by A56;
then A59: (dom B) -tail p in (Polish-WFF-set ((Polish-ext-domain (B,J)),D)) ^^ (A . ((dom B) -head p)) by A57, A58;
A60: A . ((dom B) -head p) = D . ((dom B) -head p) by A52, FUNCT_4:13;
A61: (dom B) -head p in Polish-ext-domain (B,J) by A52, XBOOLE_0:def 3;
((dom B) -head p) ^ ((dom B) -tail p) = p ;
hence a in Polish-WFF-set ((Polish-ext-domain (B,J)),D) by A59, A60, A61, Def6; :: thesis: verum

end;

suppose not p is dom B -headed ; :: thesis: a in Polish-WFF-set ((Polish-ext-domain (B,J)),D)

then p in Polish-ext-complement (B,J) ;
then ( p in dom D & D . p = 0 ) by A6;
then ( p in Polish-ext-domain (B,J) & D . p = 0 ) by FUNCT_2:def 1;
then p in Polish-atoms ((Polish-ext-domain (B,J)),D) by POLNOT_1:def 7;
hence a in Polish-WFF-set ((Polish-ext-domain (B,J)),D) by POLNOT_1:36, TARSKI:def 3; :: thesis: verum

end;

end;

end;

A70: for n being Nat holds S₁[n] from NAT_1:sch 2(A30, A40);
let a be object ; :: thesis: ( a in J iff a in Polish-WFF-set ((Polish-ext-domain (B,J)),D) )
thus ( a in J implies a in Polish-WFF-set ((Polish-ext-domain (B,J)),D) ) :: thesis: ( a in Polish-WFF-set ((Polish-ext-domain (B,J)),D) implies a in J )

proof

assume a in J ; :: thesis: a in Polish-WFF-set ((Polish-ext-domain (B,J)),D)
then reconsider p = a as Element of J ;
set m = len p;
p in J |` (len p) ;
hence a in Polish-WFF-set ((Polish-ext-domain (B,J)),D) by A70, TARSKI:def 3; :: thesis: verum

end;

Polish-WFF-set ((Polish-ext-domain (B,J)),D) c= J by A9, POLNOT_1:37;
hence ( a in Polish-WFF-set ((Polish-ext-domain (B,J)),D) implies a in J ) ; :: thesis: verum

end;

hence J = Polish-WFF-set ((Polish-ext-domain (B,J)),D) by TARSKI:2; :: thesis: verum