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
dom fss c= dom fs by GRAPH_2:27;
then A1: dom fss c= Seg (len fs) by FINSEQ_1:def 3;
A2: Seq fss = fss * (Sgm (dom fss)) by FINSEQ_1:def 14;
rng (Sgm (dom fss)) = dom fss by A1, FINSEQ_1:def 13;
then len (Seq fss) = len (Sgm (dom fss)) by A2, FINSEQ_2:33
.= card (dom fss) by A1, FINSEQ_3:44
.= card fss by CARD_1:104 ;
hence len (Seq fss) <= len fs by NAT_1:44; :: thesis: verum