let D be non empty set ; 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; for X being set st dom (F | X) is finite holds
FinS (F,(dom (F | X))) = FinS (F,X)
let X be set ; ( 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
; 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; verum