let F be XFinSequence; :: thesis: for X being set holds dom (SubXFinS (F,X)) = dom (Sgm0 (X /\ (dom F)))
let X be set ; :: thesis: dom (SubXFinS (F,X)) = dom (Sgm0 (X /\ (dom F)))
len (SubXFinS (F,X)) = card (X /\ (Segm (len F))) by AFINSQ_2:36
.= card (Sgm0 (X /\ (dom F))) by AFINSQ_2:20 ;
hence dom (SubXFinS (F,X)) = dom (Sgm0 (X /\ (dom F))) ; :: thesis: verum