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 A1: card (dom (F | X)) = 0 ; :: thesis: ex a being FinSequence st F | X,a are_fiberwise_equipotent
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))
dom (F | X) = {} by A1;
then ( A " {x} c= dom A & (F | X) " {x} = {} ) by RELAT_1:132, XBOOLE_1:3;
hence card (Coim ((F | X),x)) = card (Coim (A,x)) by XBOOLE_1:3; :: thesis: verum