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