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₁[n] from NAT_1:sch 2(Lm1, Lm2);
hence ex f being FinSequence st F | X,f are_fiberwise_equipotent by A1; :: thesis: verum