let n be non zero Nat; :: thesis: for X being non-empty n -element FinSequence
for S being SemiringFamily of X holds dom S = dom X
let X be non-empty n -element FinSequence; :: thesis: for S being SemiringFamily of X holds dom S = dom X
let S be SemiringFamily of X; :: thesis: dom S = dom X
dom S = Seg n by FINSEQ_1:89;
hence dom S = dom X by FINSEQ_1:89; :: thesis: verum