let p be XFinSequence; :: thesis: for B being set holds
( len (SubXFinS p,B) = card (B /\ (len p)) & ( for i being Nat st i < len (SubXFinS p,B) holds
(SubXFinS p,B) . i = p . ((Sgm0 (B /\ (len p))) . i) ) )
let B be set ; :: thesis: ( len (SubXFinS p,B) = card (B /\ (len p)) & ( for i being Nat st i < len (SubXFinS p,B) holds
(SubXFinS p,B) . i = p . ((Sgm0 (B /\ (len p))) . i) ) )
B /\ (len p) c= dom p by XBOOLE_1:17;
then rng (Sgm0 (B /\ (len p))) c= dom p by Def5;
then dom (SubXFinS p,B) = len (Sgm0 (B /\ (len p))) by RELAT_1:46
.= card (B /\ (len p)) by Th31 ;
hence len (SubXFinS p,B) = card (B /\ (len p)) ; :: thesis: for i being Nat st i < len (SubXFinS p,B) holds
(SubXFinS p,B) . i = p . ((Sgm0 (B /\ (len p))) . i)
let i be Nat; :: thesis: ( i < len (SubXFinS p,B) implies (SubXFinS p,B) . i = p . ((Sgm0 (B /\ (len p))) . i) )
assume i < len (SubXFinS p,B) ; :: thesis: (SubXFinS p,B) . i = p . ((Sgm0 (B /\ (len p))) . i)
then i in dom (SubXFinS p,B) by NAT_1:45;
hence (SubXFinS p,B) . i = p . ((Sgm0 (B /\ (len p))) . i) by FUNCT_1:22; :: thesis: verum