let Y be set ; :: thesis: for C being non empty set

for p being Real

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

for f being PartFunc of C,REAL st f | Y is constant holds

(p (#) f) | Y is constant

let p be Real; :: 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 Th49;

hence ( f | Y is constant implies (p (#) f) | Y is constant ) ; :: thesis: verum

for p being Real

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

for f being PartFunc of C,REAL st f | Y is constant holds

(p (#) f) | Y is constant

let p be Real; :: 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 Th49;

hence ( f | Y is constant implies (p (#) f) | Y is constant ) ; :: thesis: verum