defpred S1[ set , set , set , set ] means ( P2[$1,$2,$3] & not $1 in union $4 );
consider f being sequence of (bool (bool F1())) such that
A1: f . 0 = F2() and
A2: 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
S1[c,V,n,fq] } ) where V is Subset of F1() : P1[V] } from PCOMPS_2:sch 2();
 take f ; :: thesis: ( f . 0 = F2() & ( for n being Nat holds f . (n + 1) = { (union { F3(c,n) where c is Element of F1() : ( P2[c,V,n] & not c in union { (union (f . q)) where q is Nat : q <= n } ) } ) where V is Subset of F1() : P1[V] } ) )
thus f . 0 = F2() by A1; :: thesis: for n being Nat holds f . (n + 1) = { (union { F3(c,n) where c is Element of F1() : ( P2[c,V,n] & not c in union { (union (f . q)) where q is Nat : q <= n } ) } ) 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() : ( P2[c,V,n] & not c in union { (union (f . q)) where q is Nat : q <= n } ) } ) where V is Subset of F1() : P1[V] }
deffunc H1( 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] & not c in union fq ) } ;
deffunc H2( set ) -> set = union { F3(c,n) where c is Element of F1() : ( P2[c,$1,n] & not c in union { (union (f . q)) where q is Nat : q <= n } ) } ;
set fxxx1 = { H1(V) where V is Subset of F1() : P1[V] } ;
set fxxx = { H2(V) where V is Subset of F1() : P1[V] } ;
A3: now :: thesis: for V being Subset of F1() st P1[V] holds
H1(V) = H2(V)
deffunc H3( set ) -> Subset of F1() = F3($1,n);
let V be Subset of F1(); :: thesis: ( P1[V] implies H1(V) = H2(V) )
assume P1[V] ; :: thesis: H1(V) = H2(V)
defpred S2[ set ] means for fq being Subset-Family of F1()
for q being Nat st q <= n & fq = f . q holds
( P2[$1,V,n] & not $1 in union fq );
defpred S3[ set ] means ( P2[$1,V,n] & not $1 in union { (union (f . q1)) where q1 is Nat : q1 <= n } );
A4: now :: thesis: for c being Element of F1() holds
( S2[c] iff S3[c] )
let c be Element of F1(); :: thesis: ( S2[c] iff S3[c] )
A5: ( ( for fq being Subset-Family of F1()
for q being Nat st q <= n & fq = f . q holds
not c in union fq ) iff not c in union { (union (f . q)) where q is Nat : q <= n } )
proof
thus ( ( for fq being Subset-Family of F1()
for q being Nat st q <= n & fq = f . q holds
not c in union fq ) implies not c in union { (union (f . q)) where q is Nat : q <= n } ) :: thesis: ( not c in union { (union (f . q)) where q is Nat : q <= n } implies for fq being Subset-Family of F1()
for q being Nat st q <= n & fq = f . q holds
not c in union fq )
proof
assume A6: for fq being Subset-Family of F1()
for q being Nat st q <= n & fq = f . q holds
not c in union fq ; :: thesis: not c in union { (union (f . q)) where q is Nat : q <= n }
assume c in union { (union (f . q)) where q is Nat : q <= n } ; :: thesis: contradiction
then consider C being set such that
A7: c in C and
A8: C in { (union (f . q)) where q is Nat : q <= n } by TARSKI:def 4;
consider q being Nat such that
A9: ( C = union (f . q) & q <= n ) by A8;
reconsider q = q as Element of NAT by ORDINAL1:def 12;
f . q = f . q ;
hence contradiction by A6, A7, A9; :: thesis: verum
end;
assume A10: not c in union { (union (f . q)) where q is Nat : q <= n } ; :: thesis: for fq being Subset-Family of F1()
for q being Nat st q <= n & fq = f . q holds
not c in union fq
let fq be Subset-Family of F1(); :: thesis: for q being Nat st q <= n & fq = f . q holds
not c in union fq
let q be Nat; :: thesis: ( q <= n & fq = f . q implies not c in union fq )
assume ( q <= n & fq = f . q ) ; :: thesis: not c in union fq
then union fq in { (union (f . p)) where p is Nat : p <= n } ;
hence not c in union fq by A10, TARSKI:def 4; :: thesis: verum
end;
thus ( S2[c] iff S3[c] ) :: thesis: verum
proof
hereby :: thesis: ( S3[c] implies S2[c] )
reconsider q = n as Element of NAT by ORDINAL1:def 12;
assume A11: for fq being Subset-Family of F1()
for q being Nat st q <= n & fq = f . q holds
( P2[c,V,n] & not c in union fq ) ; :: thesis: ( P2[c,V,n] & not c in union { (union (f . p)) where p is Nat : p <= n } )
ex fq being Subset-Family of F1() st fq = f . q ;
hence P2[c,V,n] by A11; :: thesis: not c in union { (union (f . p)) where p is Nat : p <= n }
thus not c in union { (union (f . p)) where p is Nat : p <= n } by A5, A11; :: thesis: verum
end;
assume ( P2[c,V,n] & not c in union { (union (f . q)) where q is Nat : q <= n } ) ; :: thesis: S2[c]
hence S2[c] by A5; :: thesis: verum
end;
end;
{ H3(c) where c is Element of F1() : S2[c] } = { H3(c) where c is Element of F1() : S3[c] } from FRAENKEL:sch 3(A4);
hence H1(V) = H2(V) ; :: thesis: verum
end;
{ H1(V) where V is Subset of F1() : P1[V] } = { H2(V) where V is Subset of F1() : P1[V] } from FRAENKEL:sch 6(A3);
 hence f . (n + 1) = { (union { F3(c,n) where c is Element of F1() : ( P2[c,V,n] & not c in union { (union (f . q)) where q is Nat : q <= n } ) } ) where V is Subset of F1() : P1[V] } by A2; :: thesis: verum