consider r being Element of REAL such that
A3: for c being Element of C st c in dom f holds
f . c = r by PARTFUN2:def 1;

now :: thesis: ex r1 being Element of REAL st
for c being Element of C st c in dom (p (#) f) holds
(p (#) f) . c = r1

reconsider r1 = p * r as Element of REAL by XREAL_0:def 1;
take r1 = r1; :: thesis: for c being Element of C st c in dom (p (#) f) holds
(p (#) f) . c = r1
let c be Element of C; :: thesis: ( c in dom (p (#) f) implies (p (#) f) . c = r1 )
assume c in dom (p (#) f) ; :: thesis: (p (#) f) . c = r1
then c in dom f by VALUED_1:def 5;
then p * (f . c) = r1 by A3;
hence (p (#) f) . c = r1 by VALUED_1:6; :: thesis: verum

end;

hence p (#) f is constant by PARTFUN2:def 1; :: thesis: verum