let X be finite set ; :: thesis: for F being Function st card (dom (F | X)) = 0 holds
ex a being FinSequence st F | X,a are_fiberwise_equipotent
let F be Function; :: thesis: ( card (dom (F | X)) = 0 implies ex a being FinSequence st F | X,a are_fiberwise_equipotent )
assume card (dom (F | X)) = 0 ; :: thesis: ex a being FinSequence st F | X,a are_fiberwise_equipotent
then A1: dom (F | X) = {} ;
take A = {} ; :: thesis: F | X,A are_fiberwise_equipotent
let x be set ; :: according to CLASSES1:def 9 :: thesis: card (Coim (F | X),x) = card (Coim A,x)
( (F | X) " {x} c= dom (F | X) & A " {x} c= dom A ) by RELAT_1:167;
then ( (F | X) " {x} = {} & A " {x} = {} ) by A1, XBOOLE_1:3;
hence card (Coim (F | X),x) = card (Coim A,x) ; :: thesis: verum