set x = dom (F | X);
consider b being FinSequence such that
A2: F | (dom (F | X)),b are_fiberwise_equipotent by A1, RFINSEQ:5;
rng (F | (dom (F | X))) = rng b by A2, CLASSES1:75;
then reconsider b = b as FinSequence of REAL by FINSEQ_1:def 4;
consider a being non-increasing FinSequence of REAL such that
A3: b,a are_fiberwise_equipotent by RFINSEQ:22;
take a ; :: thesis: F | X,a are_fiberwise_equipotent
dom (F | X) = (dom F) /\ X by RELAT_1:61;
then F | (dom (F | X)) = (F | (dom F)) | X by RELAT_1:71
.= F | X by RELAT_1:68 ;
hence F | X,a are_fiberwise_equipotent by A2, A3, CLASSES1:76; :: thesis: verum