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,(dom (F | 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,(dom (F | X))) = FinS (F,X)
let X be set ; :: thesis: ( dom (F | X) is finite implies FinS (F,(dom (F | X))) = FinS (F,X) )
A1: F | (dom (F | X)) = F | ((dom F) /\ X) by RELAT_1:61
.= (F | (dom F)) | X by RELAT_1:71
.= F | X by RELAT_1:68 ;
assume A2: dom (F | X) is finite ; :: thesis: FinS (F,(dom (F | X))) = FinS (F,X)
then FinS (F,X),F | X are_fiberwise_equipotent by Def13;
hence FinS (F,(dom (F | X))) = FinS (F,X) by A2, A1, Def13; :: thesis: verum