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:90
.= {} ;
then len (FinS F,{} ) = 0 by Th70, CARD_1:47;
hence FinS F,{} = <*> REAL ; :: thesis: verum