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