reconsider f = (proj (1,1)) " as PartFunc of REAL,(REAL 1) by PARTFUN1:9;
(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