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