let X be set ; :: thesis: for B being SetSequence of X
for f being Function st dom f = NAT & ( for n being Nat holds f . n = union { (B . k) where k is Nat : n <= k } ) holds
f is sequence of (bool X)
let B be SetSequence of X; :: thesis: for f being Function st dom f = NAT & ( for n being Nat holds f . n = union { (B . k) where k is Nat : n <= k } ) holds
f is sequence of (bool X)
let f be Function; :: thesis: ( dom f = NAT & ( for n being Nat holds f . n = union { (B . k) where k is Nat : n <= k } ) implies f is sequence of (bool X) )
assume that
A1: dom f = NAT and
A2: for n being Nat holds f . n = union { (B . k) where k is Nat : n <= k } ; :: thesis: f is sequence of (bool X)
rng f c= bool X

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in rng f or z in bool X )
assume z in rng f ; :: thesis: z in bool X
then consider x being object such that
A3: x in dom f and
A4: z = f . x by FUNCT_1:def 3;
reconsider n = x as Nat by A1, A3;
set Y = { (B . k) where k is Nat : n <= k } ;
set y = union { (B . k) where k is Nat : n <= k } ;

now :: thesis: for z being object st z in union { (B . k) where k is Nat : n <= k } holds
z in X

let z be object ; :: thesis: ( z in union { (B . k) where k is Nat : n <= k } implies z in X )
assume z in union { (B . k) where k is Nat : n <= k } ; :: thesis: z in X
then ex Z being set st
( z in Z & Z in { (B . k) where k is Nat : n <= k } ) by TARSKI:def 4;
then consider Z1 being set such that
A5: Z1 in { (B . k) where k is Nat : n <= k } and
A6: z in Z1 ;
consider k1 being Nat such that
A7: ( Z1 = B . k1 & n <= k1 ) by A5;
reconsider k1 = k1 as Element of NAT by ORDINAL1:def 12;
Z1 = B . k1 by A7;
hence z in X by A6; :: thesis: verum

end;

then A8: union { (B . k) where k is Nat : n <= k } is Subset of X by TARSKI:def 3;
z = union { (B . k) where k is Nat : n <= k } by A2, A4;
hence z in bool X by A8; :: thesis: verum

end;

hence f is sequence of (bool X) by A1, FUNCT_2:2; :: thesis: verum