reconsider f = (proj 1,1) " as PartFunc of REAL ,(REAL 1) by PARTFUN1:39;
f * g is PartFunc of (REAL n),(REAL 1) ;
hence ((proj 1,1) " ) * g is PartFunc of (REAL n),(REAL 1) ; :: thesis: verum