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

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