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