let n be Nat; :: thesis: for D being non empty finite set
for a being FinSequence of bool D st n in dom a holds
a . n c= D
let D be non empty finite set ; :: thesis: for a being FinSequence of bool D st n in dom a holds
a . n c= D
let a be FinSequence of bool D; :: thesis: ( n in dom a implies a . n c= D )
assume n in dom a ; :: thesis: a . n c= D
then a . n in bool D by FINSEQ_2:11;
hence a . n c= D ; :: thesis: verum