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 object ; :: according to CLASSES1:def 10 :: thesis: card (Coim ((F | X),x)) = card (Coim (A,x))
dom (F | X) = {} by A1;
hence card (Coim ((F | X),x)) = card (Coim (A,x)) by RELAT_1:132, XBOOLE_1:3; :: thesis: verum