let D be non empty finite set ; :: thesis: for A being FinSequence of bool D
for k being Nat st 1 <= k & k <= len A holds
A . k is finite
let A be FinSequence of bool D; :: thesis: for k being Nat st 1 <= k & k <= len A holds
A . k is finite
let k be Nat; :: thesis: ( 1 <= k & k <= len A implies A . k is finite )
assume ( 1 <= k & k <= len A ) ; :: thesis: A . k is finite
then k in dom A by FINSEQ_3:25;
then A . k in bool D by FINSEQ_2:11;
hence A . k is finite ; :: thesis: verum