reconsider A = <*F2()*> as Element of (bool (bool F1())) * by FINSEQ_1:def 11;
defpred S1[ Nat, FinSequence of bool (bool F1()), set ] means $3 = $2 ^ <* { (union { F3(c,$1) where c is Element of F1() : for fq being Subset-Family of F1()
for q being Nat st q <= $1 & fq = $2 /. (q + 1) holds
P2[c,V,$1,fq] } ) where V is Subset of F1() : P1[V] } *>;
A1: for n being Nat
for x being Element of (bool (bool F1())) * ex y being Element of (bool (bool F1())) * st S1[n,x,y]
proof
let n be Nat; :: thesis: for x being Element of (bool (bool F1())) * ex y being Element of (bool (bool F1())) * st S1[n,x,y]
let x be Element of (bool (bool F1())) * ; :: thesis: ex y being Element of (bool (bool F1())) * st S1[n,x,y]
set T = { (union { F3(c,n) where c is Element of F1() : for fq being Subset-Family of F1()
for q being Nat st q <= n & fq = x /. (q + 1) holds
P2[c,V,n,fq] } ) where V is Subset of F1() : P1[V] } ;
now :: thesis: for X being object st X in { (union { F3(c,n) where c is Element of F1() : for fq being Subset-Family of F1()
for q being Nat st q <= n & fq = x /. (q + 1) holds
P2[c,V,n,fq] } ) where V is Subset of F1() : P1[V] } holds
X in bool F1()
let X be object ; :: thesis: ( X in { (union { F3(c,n) where c is Element of F1() : for fq being Subset-Family of F1()
for q being Nat st q <= n & fq = x /. (q + 1) holds
P2[c,V,n,fq] } ) where V is Subset of F1() : P1[V] } implies X in bool F1() )
reconsider XX = X as set by TARSKI:1;
assume X in { (union { F3(c,n) where c is Element of F1() : for fq being Subset-Family of F1()
for q being Nat st q <= n & fq = x /. (q + 1) holds
P2[c,V,n,fq] } ) where V is Subset of F1() : P1[V] } ; :: thesis: X in bool F1()
then consider V being Subset of F1() such that
A2: X = union { F3(c,n) where c is Element of F1() : for fq being Subset-Family of F1()
for q being Nat st q <= n & fq = x /. (q + 1) holds
P2[c,V,n,fq] } and
P1[V] ;
now :: thesis: for a being object st a in XX holds
a in F1()
let a be object ; :: thesis: ( a in XX implies a in F1() )
assume a in XX ; :: thesis: a in F1()
then consider P being set such that
A3: a in P and
A4: P in { F3(c,n) where c is Element of F1() : for fq being Subset-Family of F1()
for q being Nat st q <= n & fq = x /. (q + 1) holds
P2[c,V,n,fq] } by A2, TARSKI:def 4;
ex c being Element of F1() st
( P = F3(c,n) & ( for fq being Subset-Family of F1()
for q being Nat st q <= n & fq = x /. (q + 1) holds
P2[c,V,n,fq] ) ) by A4;
hence a in F1() by A3; :: thesis: verum
end;
then XX c= F1() ;
hence X in bool F1() ; :: thesis: verum
end;
then reconsider T = { (union { F3(c,n) where c is Element of F1() : for fq being Subset-Family of F1()
for q being Nat st q <= n & fq = x /. (q + 1) holds
P2[c,V,n,fq] } ) where V is Subset of F1() : P1[V] } as Subset-Family of F1() by TARSKI:def 3;
reconsider T1 = <*T*> as FinSequence of bool (bool F1()) ;
consider y being FinSequence of bool (bool F1()) such that
A5: y = x ^ T1 ;
reconsider y = y as Element of (bool (bool F1())) * by FINSEQ_1:def 11;
take y ; :: thesis: S1[n,x,y]
thus S1[n,x,y] by A5; :: thesis: verum
end;
consider g being sequence of ((bool (bool F1())) *) such that
A6: g . 0 = A and
A7: for n being Nat holds S1[n,g . n,g . (n + 1)] from RECDEF_1:sch 2(A1);
 defpred S2[ Nat] means len (g . $1) = $1 + 1;
A8: for k being Nat st S2[k] holds
S2[k + 1]
proof
let k be Nat; :: thesis: ( S2[k] implies S2[k + 1] )
assume A9: len (g . k) = k + 1 ; :: thesis: S2[k + 1]
len (g . (k + 1)) = len ((g . k) ^ <* { (union { F3(c,k) where c is Element of F1() : for fq being Subset-Family of F1()
for q being Nat st q <= k & fq = (g . k) /. (q + 1) holds
P2[c,V,k,fq] } ) where V is Subset of F1() : P1[V] } *>) by A7
.= (len (g . k)) + 1 by FINSEQ_2:16 ;
hence S2[k + 1] by A9; :: thesis: verum
end;
deffunc H1( Nat) -> Element of bool (bool F1()) = (g . $1) /. (len (g . $1));
consider f being sequence of (bool (bool F1())) such that
A10: for n being Element of NAT holds f . n = H1(n) from FUNCT_2:sch 4();
 A11: for n being Nat holds f . n = H1(n)
proof
let n be Nat; :: thesis: f . n = H1(n)
n in NAT by ORDINAL1:def 12;
hence f . n = H1(n) by A10; :: thesis: verum
end;
take f ; :: thesis: ( f . 0 = F2() & ( for n being Nat holds f . (n + 1) = { (union { F3(c,n) where c is Element of F1() : for fq being Subset-Family of F1()
for q being Nat st q <= n & fq = f . q holds
P2[c,V,n,fq] } ) where V is Subset of F1() : P1[V] } ) )
len <*F2()*> = 1 by FINSEQ_1:39;
hence f . 0 = <*F2()*> /. 1 by A6, A11
.= F2() by FINSEQ_4:16 ;
:: thesis: for n being Nat holds f . (n + 1) = { (union { F3(c,n) where c is Element of F1() : for fq being Subset-Family of F1()
for q being Nat st q <= n & fq = f . q holds
P2[c,V,n,fq] } ) where V is Subset of F1() : P1[V] }
let n be Nat; :: thesis: f . (n + 1) = { (union { F3(c,n) where c is Element of F1() : for fq being Subset-Family of F1()
for q being Nat st q <= n & fq = f . q holds
P2[c,V,n,fq] } ) where V is Subset of F1() : P1[V] }
reconsider n = n as Element of NAT by ORDINAL1:def 12;
defpred S3[ Nat] means for q being Nat st q <= $1 holds
f . q = (g . $1) /. (q + 1);
A12: S2[ 0 ] by A6, FINSEQ_1:39;
A13: for n being Nat holds S2[n] from NAT_1:sch 2(A12, A8);
 then A14: (len (g . n)) + 1 = (n + 1) + 1 ;
A15: for k being Nat st S3[k] holds
S3[k + 1]
proof
let k be Nat; :: thesis: ( S3[k] implies S3[k + 1] )
assume A16: for q being Nat st q <= k holds
f . q = (g . k) /. (q + 1) ; :: thesis: S3[k + 1]
let q be Nat; :: thesis: ( q <= k + 1 implies f . q = (g . (k + 1)) /. (q + 1) )
assume A17: q <= k + 1 ; :: thesis: f . q = (g . (k + 1)) /. (q + 1)
now :: thesis: f . q = (g . (k + 1)) /. (q + 1)
per cases ( q = k + 1 or q < k + 1 ) by A17, XXREAL_0:1;
suppose A18: q = k + 1 ; :: thesis: f . q = (g . (k + 1)) /. (q + 1)
thus f . q = (g . q) /. (len (g . q)) by A11
.= (g . (k + 1)) /. (q + 1) by A13, A18 ; :: thesis: verum
end;
suppose A19: q < k + 1 ; :: thesis: (g . (k + 1)) /. (q + 1) = f . q
A20: q + 1 >= 1 by NAT_1:11;
q + 1 <= k + 1 by A19, NAT_1:13;
then A21: q + 1 in Seg (k + 1) by A20, FINSEQ_1:1;
then q + 1 in Seg (len (g . k)) by A13;
then A22: q + 1 in dom (g . k) by FINSEQ_1:def 3;
A23: q <= k by A19, NAT_1:13;
(k + 1) + 1 >= k + 1 by NAT_1:11;
then Seg (k + 1) c= Seg ((k + 1) + 1) by FINSEQ_1:5;
then q + 1 in Seg ((k + 1) + 1) by A21;
then q + 1 in Seg (len (g . (k + 1))) by A13;
then q + 1 in dom (g . (k + 1)) by FINSEQ_1:def 3;
hence (g . (k + 1)) /. (q + 1) = (g . (k + 1)) . (q + 1) by PARTFUN1:def 6
.= ((g . k) ^ <* { (union { F3(c,k) where c is Element of F1() : for fq being Subset-Family of F1()
for q being Nat st q <= k & fq = (g . k) /. (q + 1) holds
P2[c,V,k,fq] } ) where V is Subset of F1() : P1[V] } *>) . (q + 1) by A7
.= (g . k) . (q + 1) by A22, FINSEQ_1:def 7
.= (g . k) /. (q + 1) by A22, PARTFUN1:def 6
.= f . q by A16, A23 ;
:: thesis: verum
end;
end;
end;
hence f . q = (g . (k + 1)) /. (q + 1) ; :: thesis: verum
end;
deffunc H2( set ) -> set = union { F3(c,n) where c is Element of F1() : for fq being Subset-Family of F1()
for q being Nat st q <= n & fq = (g . n) /. (q + 1) holds
P2[c,$1,n,fq] } ;
deffunc H3( set ) -> set = union { F3(c,n) where c is Element of F1() : for fq being Subset-Family of F1()
for q being Nat st q <= n & fq = f . q holds
P2[c,$1,n,fq] } ;
set NF = { H3(V) where V is Subset of F1() : P1[V] } ;
len (g . (n + 1)) = (n + 1) + 1 by A13;
then A24: dom (g . (n + 1)) = Seg ((n + 1) + 1) by FINSEQ_1:def 3;
A25: S3[ 0 ]
proof
let q be Nat; :: thesis: ( q <= 0 implies f . q = (g . 0) /. (q + 1) )
assume q <= 0 ; :: thesis: f . q = (g . 0) /. (q + 1)
then A26: q = 0 ;
thus f . q = (g . q) /. (len (g . q)) by A11
.= (g . 0) /. (q + 1) by A6, A26, FINSEQ_1:39 ; :: thesis: verum
end;
A27: for n being Nat holds S3[n] from NAT_1:sch 2(A25, A15);
 A28: for V being Subset of F1() st P1[V] holds
H3(V) = H2(V)
proof
deffunc H4( set ) -> Subset of F1() = F3($1,n);
let V be Subset of F1(); :: thesis: ( P1[V] implies H3(V) = H2(V) )
assume P1[V] ; :: thesis: H3(V) = H2(V)
defpred S4[ set ] means for fq being Subset-Family of F1()
for q being Nat st q <= n & fq = f . q holds
P2[$1,V,n,fq];
defpred S5[ set ] means for fq being Subset-Family of F1()
for q being Nat st q <= n & fq = (g . n) /. (q + 1) holds
P2[$1,V,n,fq];
A29: for c being Element of F1() holds
( S4[c] iff S5[c] )
proof
let c be Element of F1(); :: thesis: ( S4[c] iff S5[c] )
thus ( ( for fq being Subset-Family of F1()
for q being Nat st q <= n & fq = f . q holds
P2[c,V,n,fq] ) implies for fq being Subset-Family of F1()
for q being Nat st q <= n & fq = (g . n) /. (q + 1) holds
P2[c,V,n,fq] ) :: thesis: ( S5[c] implies S4[c] )
proof
assume A30: for fq being Subset-Family of F1()
for q being Nat st q <= n & fq = f . q holds
P2[c,V,n,fq] ; :: thesis: for fq being Subset-Family of F1()
for q being Nat st q <= n & fq = (g . n) /. (q + 1) holds
P2[c,V,n,fq]
let fq be Subset-Family of F1(); :: thesis: for q being Nat st q <= n & fq = (g . n) /. (q + 1) holds
P2[c,V,n,fq]
let q be Nat; :: thesis: ( q <= n & fq = (g . n) /. (q + 1) implies P2[c,V,n,fq] )
assume that
A31: q <= n and
A32: fq = (g . n) /. (q + 1) ; :: thesis: P2[c,V,n,fq]
fq = f . q by A27, A31, A32;
hence P2[c,V,n,fq] by A30, A31; :: thesis: verum
end;
assume A33: for fq being Subset-Family of F1()
for q being Nat st q <= n & fq = (g . n) /. (q + 1) holds
P2[c,V,n,fq] ; :: thesis: S4[c]
let fq be Subset-Family of F1(); :: thesis: for q being Nat st q <= n & fq = f . q holds
P2[c,V,n,fq]
let q be Nat; :: thesis: ( q <= n & fq = f . q implies P2[c,V,n,fq] )
assume that
A34: q <= n and
A35: fq = f . q ; :: thesis: P2[c,V,n,fq]
f . q = (g . n) /. (q + 1) by A27, A34;
hence P2[c,V,n,fq] by A33, A34, A35; :: thesis: verum
end;
{ H4(c) where c is Element of F1() : S4[c] } = { H4(c) where c is Element of F1() : S5[c] } from FRAENKEL:sch 3(A29);
 hence H3(V) = H2(V) ; :: thesis: verum
end;
A36: { H3(V) where V is Subset of F1() : P1[V] } = { H2(V) where V is Subset of F1() : P1[V] } from FRAENKEL:sch 6(A28);
 then A37: len (g . (n + 1)) = len ((g . n) ^ <* { H3(V) where V is Subset of F1() : P1[V] } *>) by A7
.= (len (g . n)) + 1 by FINSEQ_2:16 ;
reconsider n1 = n + 1 as Element of NAT ;
f . n1 = H1(n1) by A11
.= (g . n1) /. (len (g . n1))
.= (g . n1) /. ((len (g . n)) + 1) by A37
.= (g . (n + 1)) . ((len (g . n)) + 1) by A24, A14, FINSEQ_1:4, PARTFUN1:def 6
.= ((g . n) ^ <* { H3(V) where V is Subset of F1() : P1[V] } *>) . ((len (g . n)) + 1) by A7, A36
.= { H3(V) where V is Subset of F1() : P1[V] } by FINSEQ_1:42 ;
hence f . (n + 1) = { (union { F3(c,n) where c is Element of F1() : for fq being Subset-Family of F1()
for q being Nat st q <= n & fq = f . q holds
P2[c,V,n,fq] } ) where V is Subset of F1() : P1[V] } ; :: thesis: verum