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