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:72;
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 Def13;
hence FinS ((F | X),X) = FinS (F,X) by A2, A1, Def13; :: thesis: verum