let p be XFinSequence; :: thesis: for B being set holds
( len (SubXFinS (p,B)) = card (B /\ (Segm (len p))) & ( for i being Nat st i < len (SubXFinS (p,B)) holds
(SubXFinS (p,B)) . i = p . ((Sgm0 (B /\ (Segm (len p)))) . i) ) )
let B be set ; :: thesis: ( len (SubXFinS (p,B)) = card (B /\ (Segm (len p))) & ( for i being Nat st i < len (SubXFinS (p,B)) holds
(SubXFinS (p,B)) . i = p . ((Sgm0 (B /\ (Segm (len p)))) . i) ) )
B /\ (Segm (len p)) c= dom p by XBOOLE_1:17;
then rng (Sgm0 (B /\ (Segm (len p)))) c= dom p by Def4;
then dom (SubXFinS (p,B)) = len (Sgm0 (B /\ (Segm (len p)))) by RELAT_1:27
.= card (B /\ (Segm (len p))) by Th20 ;
hence len (SubXFinS (p,B)) = card (B /\ (Segm (len p))) ; :: thesis: for i being Nat st i < len (SubXFinS (p,B)) holds
(SubXFinS (p,B)) . i = p . ((Sgm0 (B /\ (Segm (len p)))) . i)
let i be Nat; :: thesis: ( i < len (SubXFinS (p,B)) implies (SubXFinS (p,B)) . i = p . ((Sgm0 (B /\ (Segm (len p)))) . i) )
assume i < len (SubXFinS (p,B)) ; :: thesis: (SubXFinS (p,B)) . i = p . ((Sgm0 (B /\ (Segm (len p)))) . i)
hence (SubXFinS (p,B)) . i = p . ((Sgm0 (B /\ (Segm (len p)))) . i) by FUNCT_1:12, AFINSQ_1:86; :: thesis: verum