let Y be set ; :: thesis: for C being non empty set
for f being PartFunc of C,COMPLEX
for q being Complex st f | Y is constant holds
(q (#) f) | Y is constant
let C be non empty set ; :: thesis: for f being PartFunc of C,COMPLEX
for q being Complex st f | Y is constant holds
(q (#) f) | Y is constant
let f be PartFunc of C,COMPLEX; :: thesis: for q being Complex st f | Y is constant holds
(q (#) f) | Y is constant
let q be Complex; :: thesis: ( f | Y is constant implies (q (#) f) | Y is constant )
assume f | Y is constant ; :: thesis: (q (#) f) | Y is constant
then consider r being Element of COMPLEX such that
A1: for c being Element of C st c in Y /\ (dom f) holds
f /. c = r by PARTFUN2:35;
A2: q * r in COMPLEX by XCMPLX_0:def 2;

now :: thesis: for c being Element of C st c in Y /\ (dom (q (#) f)) holds
(q (#) f) /. c = q * r

let c be Element of C; :: thesis: ( c in Y /\ (dom (q (#) f)) implies (q (#) f) /. c = q * r )
assume A3: c in Y /\ (dom (q (#) f)) ; :: thesis: (q (#) f) /. c = q * r
then A4: c in Y by XBOOLE_0:def 4;
A5: c in dom (q (#) f) by A3, XBOOLE_0:def 4;
then c in dom f by Th4;
then A6: c in Y /\ (dom f) by A4, XBOOLE_0:def 4;
thus (q (#) f) /. c = q * (f /. c) by A5, Th4
.= q * r by A1, A6 ; :: thesis: verum

end;

hence (q (#) f) | Y is constant by A2, PARTFUN2:35; :: thesis: verum