let f, g be FinSequence; :: thesis: ( f,g are_fiberwise_equipotent implies ( len f = len g & dom f = dom g ) )
A1: dom f = Seg (len f) by FINSEQ_1:def 3;
assume f,g are_fiberwise_equipotent ; :: thesis: ( len f = len g & dom f = dom g )
then A2: ( card (f " (rng f)) = card (g " (rng f)) & rng f = rng g ) by CLASSES1:75, CLASSES1:78;
A3: Seg (len g) = dom g by FINSEQ_1:def 3;
thus len f = card (Seg (len f)) by FINSEQ_1:57
.= card (g " (rng g)) by A1, A2, RELAT_1:134
.= card (Seg (len g)) by A3, RELAT_1:134
.= len g by FINSEQ_1:57 ; :: thesis: dom f = dom g
hence dom f = dom g by A1, FINSEQ_1:def 3; :: thesis: verum