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 )
A1: (F | X) | X = F | X by RELAT_1:101;
assume A2: dom (F | X) is finite ; :: thesis: FinS (F | X),X = FinS F,X
then FinS F,X,F | X are_fiberwise_equipotent by Def14;
hence FinS (F | X),X = FinS F,X by A2, A1, Def14; :: thesis: verum