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

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