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;

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

hence
p (#) f is constant
by PARTFUN2:def 1; :: thesis: verumfor 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;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