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))
A1: rng (Sgm (dom fss)) c= dom fss by FINSEQ_1:def 14;
Seq fss = fss * (Sgm (dom fss)) by FINSEQ_1:def 15;
hence dom (Seq fss) = dom (Sgm (dom fss)) by A1, RELAT_1:27; :: thesis: verum