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:167, XBOOLE_1:3;
hence card (Coim (F | X),x) = card (Coim A,x) by XBOOLE_1:3; :: thesis: verum