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

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