set x = dom (F | X);
consider b being FinSequence such that
A2: F | (dom (F | X)),b are_fiberwise_equipotent by A1, RFINSEQ:18;
rng (F | (dom (F | X))) = rng b by A2, CLASSES1:83;
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:35;
take a ; :: thesis: F | X,a are_fiberwise_equipotent
dom (F | X) = (dom F) /\ X by RELAT_1:90;
then F | (dom (F | X)) = (F | (dom F)) | X by RELAT_1:100
.= F | X by RELAT_1:97 ;
hence F | X,a are_fiberwise_equipotent by A2, A3, CLASSES1:84; :: thesis: verum