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