for X being set
for fs, fs1, fs2 being FinSequence of X
for fss, fss2 being Subset of fs
for fss1 being Subset of fs1 st Seq fss = fs1 & Seq fss1 = fs2 & fss2 = fss | (rng ((Sgm (dom fss)) | (dom fss1))) holds
Seq fss2 = fs2