let X be set ; :: thesis: for F1 being FinSequence of bool X holds dom (Complement F1) = dom F1
let F1 be FinSequence of bool X; :: thesis: dom (Complement F1) = dom F1
thus dom (Complement F1) = Seg (len (Complement F1)) by FINSEQ_1:def 3
.= Seg (len F1) by Def8
.= dom F1 by FINSEQ_1:def 3 ; :: thesis: verum