let D be non empty set ; :: thesis: for F being PartFunc of D,REAL holds FinS (F,{}) = <*> REAL
let F be PartFunc of D,REAL; :: thesis: FinS (F,{}) = <*> REAL
dom (F | {}) = (dom F) /\ {} by RELAT_1:61
.= {} ;
then len (FinS (F,{})) = 0 by Th67, CARD_1:27;
hence FinS (F,{}) = <*> REAL ; :: thesis: verum