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