consider r2 being Element of REAL such that

A13: for c being Element of C st c in dom f2 holds

f2 . c = r2 by PARTFUN2:def 1;

consider r1 being Element of REAL such that

A14: for c being Element of C st c in dom f1 holds

f1 . c = r1 by PARTFUN2:def 1;

A13: for c being Element of C st c in dom f2 holds

f2 . c = r2 by PARTFUN2:def 1;

consider r1 being Element of REAL such that

A14: for c being Element of C st c in dom f1 holds

f1 . c = r1 by PARTFUN2:def 1;

now :: thesis: for c being Element of C st c in dom (f1 (#) f2) holds

(f1 (#) f2) . c = r1 * r2

hence
f1 (#) f2 is constant
by PARTFUN2:def 1; :: thesis: verum(f1 (#) f2) . c = r1 * r2

let c be Element of C; :: thesis: ( c in dom (f1 (#) f2) implies (f1 (#) f2) . c = r1 * r2 )

assume A15: c in dom (f1 (#) f2) ; :: thesis: (f1 (#) f2) . c = r1 * r2

then A16: c in (dom f1) /\ (dom f2) by VALUED_1:def 4;

then A17: c in dom f1 by XBOOLE_0:def 4;

A18: c in dom f2 by A16, XBOOLE_0:def 4;

thus (f1 (#) f2) . c = (f1 . c) * (f2 . c) by A15, VALUED_1:def 4

.= (f1 . c) * r2 by A13, A18

.= r1 * r2 by A14, A17 ; :: thesis: verum

end;assume A15: c in dom (f1 (#) f2) ; :: thesis: (f1 (#) f2) . c = r1 * r2

then A16: c in (dom f1) /\ (dom f2) by VALUED_1:def 4;

then A17: c in dom f1 by XBOOLE_0:def 4;

A18: c in dom f2 by A16, XBOOLE_0:def 4;

thus (f1 (#) f2) . c = (f1 . c) * (f2 . c) by A15, VALUED_1:def 4

.= (f1 . c) * r2 by A13, A18

.= r1 * r2 by A14, A17 ; :: thesis: verum