let X be set ; :: thesis: for fs being FinSequence of X
for fss being Subset of fs holds dom (Seq fss) = dom (Sgm (dom fss))
let fs be FinSequence of X; :: thesis: for fss being Subset of fs holds dom (Seq fss) = dom (Sgm (dom fss))
let fss be Subset of fs; :: thesis: dom (Seq fss) = dom (Sgm (dom fss))
ex k being Nat st dom fss c= Seg k by FINSEQ_1:def 12;
then A1: rng (Sgm (dom fss)) c= dom fss by FINSEQ_1:def 13;
Seq fss = fss * (Sgm (dom fss)) by FINSEQ_1:def 14;
hence dom (Seq fss) = dom (Sgm (dom fss)) by A1, RELAT_1:27; :: thesis: verum