let X be set ; :: thesis:

let n be Element of NAT ; :: thesis:
set F1 = n |-> X;
A1: dom (n |-> X) = Seg n by FUNCOP_1:13;
rng (n |-> X) c= bool X

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in rng (n |-> X) ; :: thesis:
then ex i being Nat st
( i in dom (n |-> X) & (n |-> X) . i = x ) by FINSEQ_2:10;
then x = X by A1, FINSEQ_2:57;
hence x in bool X by ZFMISC_1:def 1; :: thesis:

end;

then A2: n |-> X is FinSequence of bool X by FINSEQ_1:def 4;
for k being Nat st k in dom (n |-> X) holds
(n |-> X) . k = X by A1, FINSEQ_2:57;
hence ex F1 being FinSequence of bool X st
for k being Nat st k in dom F1 holds
F1 . k = X by A2; :: thesis:

end;

hence ex F1 being FinSequence of bool X st
for k being Nat st k in dom F1 holds
F1 . k = X ; :: thesis: