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

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

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

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

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

A2: ex k being Nat st dom fss c= Seg k by FINSEQ_1:def 12;

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

then dom (Seq fss) = dom (Sgm (dom fss)) by A1, RELAT_1:27;

then dom (Seq fss) = Seg (card (dom fss)) by A2, FINSEQ_3:40;

then len (Seq fss) = card (dom fss) by FINSEQ_1:def 3;

hence len (Seq fss) = card fss by CARD_1:62; :: thesis: verum

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

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

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

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

A2: ex k being Nat st dom fss c= Seg k by FINSEQ_1:def 12;

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

then dom (Seq fss) = dom (Sgm (dom fss)) by A1, RELAT_1:27;

then dom (Seq fss) = Seg (card (dom fss)) by A2, FINSEQ_3:40;

then len (Seq fss) = card (dom fss) by FINSEQ_1:def 3;

hence len (Seq fss) = card fss by CARD_1:62; :: thesis: verum