let D be non empty set ; :: thesis: for F being PartFunc of D,REAL
for X being set st dom (F | X) is finite holds
FinS (F | X),X = FinS F,X
let F be PartFunc of D,REAL ; :: thesis: for X being set st dom (F | X) is finite holds
FinS (F | X),X = FinS F,X
let X be set ; :: thesis: ( dom (F | X) is finite implies FinS (F | X),X = FinS F,X )
assume A1: dom (F | X) is finite ; :: thesis: FinS (F | X),X = FinS F,X
then A2: FinS F,X,F | X are_fiberwise_equipotent by Def14;
(F | X) | X = F | X by RELAT_1:101;
hence FinS (F | X),X = FinS F,X by A1, A2, Def14; :: thesis: verum