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

now

let n be Element of NAT ; :: thesis: ex F1 being FinSequence of bool X st
for k being Nat st k in dom F1 holds
F1 . k = X
set F1 = n |-> X;
A1: dom (n |-> X) = Seg n by FUNCOP_1:13;
rng (n |-> X) c= bool X

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng (n |-> X) or x in bool X )
assume x in rng (n |-> X) ; :: thesis: x in bool X
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: verum

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: verum

end;

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