let F be Function; :: thesis: for X being finite set ex f being FinSequence st F | X,f are_fiberwise_equipotent

let X be finite set ; :: thesis: ex f being FinSequence st F | X,f are_fiberwise_equipotent

A1: card (dom (F | X)) = card (dom (F | X)) ;

for n being Nat holds S_{1}[n]
from NAT_1:sch 2(Lm1, Lm2);

hence ex f being FinSequence st F | X,f are_fiberwise_equipotent by A1; :: thesis: verum

let X be finite set ; :: thesis: ex f being FinSequence st F | X,f are_fiberwise_equipotent

A1: card (dom (F | X)) = card (dom (F | X)) ;

for n being Nat holds S

hence ex f being FinSequence st F | X,f are_fiberwise_equipotent by A1; :: thesis: verum