let X be set ; :: thesis: for fs being FinSequence of X

for fss being Subset of fs holds len (Seq fss) <= len fs

let fs be FinSequence of X; :: thesis: for fss being Subset of fs holds len (Seq fss) <= len fs

let fss be Subset of fs; :: thesis: len (Seq fss) <= len fs

A1: Seq fss = fss * (Sgm (dom fss)) by FINSEQ_1:def 14;

dom fss c= dom fs by FINSEQ_6:151;

then A2: dom fss c= Seg (len fs) by FINSEQ_1:def 3;

then rng (Sgm (dom fss)) = dom fss by FINSEQ_1:def 13;

then len (Seq fss) = len (Sgm (dom fss)) by A1, FINSEQ_2:29

.= card (dom fss) by A2, FINSEQ_3:39

.= card fss by CARD_1:62 ;

hence len (Seq fss) <= len fs by NAT_1:43; :: thesis: verum

for fss being Subset of fs holds len (Seq fss) <= len fs

let fs be FinSequence of X; :: thesis: for fss being Subset of fs holds len (Seq fss) <= len fs

let fss be Subset of fs; :: thesis: len (Seq fss) <= len fs

A1: Seq fss = fss * (Sgm (dom fss)) by FINSEQ_1:def 14;

dom fss c= dom fs by FINSEQ_6:151;

then A2: dom fss c= Seg (len fs) by FINSEQ_1:def 3;

then rng (Sgm (dom fss)) = dom fss by FINSEQ_1:def 13;

then len (Seq fss) = len (Sgm (dom fss)) by A1, FINSEQ_2:29

.= card (dom fss) by A2, FINSEQ_3:39

.= card fss by CARD_1:62 ;

hence len (Seq fss) <= len fs by NAT_1:43; :: thesis: verum