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

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