set x = dom (F | X);
consider b being FinSequence such that
A2: F | (dom (F | X)),b are_fiberwise_equipotent by A1, RFINSEQ:18;
dom (F | X) = (dom F) /\ X by RELAT_1:90;
then A3: F | (dom (F | X)) = (F | (dom F)) | X by RELAT_1:100
.= F | X by RELAT_1:97 ;
( rng (F | (dom (F | X))) c= rng F & rng F c= REAL & rng (F | (dom (F | X))) = rng b ) by A2, CLASSES1:83, RELAT_1:99;
then reconsider b = b as FinSequence of REAL by FINSEQ_1:def 4;
consider a being non-increasing FinSequence of REAL such that
A4: b,a are_fiberwise_equipotent by RFINSEQ:35;
take a ; :: thesis: F | X,a are_fiberwise_equipotent
thus F | X,a are_fiberwise_equipotent by A2, A3, A4, CLASSES1:84; :: thesis: verum