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

for k being Nat st k in dom F1 holds

F1 . k = X ; :: thesis: verum

for k being Nat st k in dom F1 holds

F1 . k = X

now :: thesis: for n being Element of NAT ex F1 being FinSequence of bool X st

for k being Nat st k in dom F1 holds

F1 . k = X

hence
ex F1 being FinSequence of bool X st for k being Nat st k in dom F1 holds

F1 . k = X

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

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

then A2:
n |-> X is FinSequence of bool X
by FINSEQ_1:def 4;
let x be object ; :: 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;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

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

for k being Nat st k in dom F1 holds

F1 . k = X ; :: thesis: verum