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