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