consider r1 being Real such that
W1: for c being Element of C st c in dom f1 holds
f1 . c = r1 by PARTFUN2:def 1;
consider r2 being Real such that
W2: for c being Element of C st c in dom f2 holds
f2 . c = r2 by PARTFUN2:def 1;

now

let c be Element of C; :: thesis: ( c in dom (f1 (#) f2) implies (f1 (#) f2) . c = r1 * r2 )
assume Z: c in dom (f1 (#) f2) ; :: thesis: (f1 (#) f2) . c = r1 * r2
then c in (dom f1) /\ (dom f2) by VALUED_1:def 4;
then A: ( c in dom f1 & c in dom f2 ) by XBOOLE_0:def 4;
thus (f1 (#) f2) . c = (f1 . c) * (f2 . c) by Z, VALUED_1:def 4
.= (f1 . c) * r2 by A, W2
.= r1 * r2 by A, W1 ; :: thesis: verum

end;

hence f1 (#) f2 is constant by PARTFUN2:def 1; :: thesis: verum