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