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

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

hence
f is sequence of (bool X)
by A1, FUNCT_2:2; :: thesis: verum
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 } ;

z = union { (B . k) where k is Nat : n <= k } by A2, A4;

hence z in bool X by A8; :: thesis: verum

end;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

then A8:
union { (B . k) where k is Nat : n <= k } is Subset of X
by TARSKI:def 3;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;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

z = union { (B . k) where k is Nat : n <= k } by A2, A4;

hence z in bool X by A8; :: thesis: verum