let Y be set ; :: thesis: for C being non empty set
for p being real number
for f being PartFunc of C,REAL st f | Y is constant holds
(p (#) f) | Y is constant
let C be non empty set ; :: thesis: for p being real number
for f being PartFunc of C,REAL st f | Y is constant holds
(p (#) f) | Y is constant
let p be real number ; :: thesis: for f being PartFunc of C,REAL st f | Y is constant holds
(p (#) f) | Y is constant
let f be PartFunc of C,REAL ; :: thesis: ( f | Y is constant implies (p (#) f) | Y is constant )
(p (#) f) | Y = p (#) (f | Y) by Th65;
hence ( f | Y is constant implies (p (#) f) | Y is constant ) ; :: thesis: verum