let C be non empty set ; :: thesis: for f1, f2 being PartFunc of C,COMPLEX holds
( dom (f1 (#) f2) = (dom f1) /\ (dom f2) & ( for c being Element of C st c in dom (f1 (#) f2) holds
(f1 (#) f2) /. c = (f1 /. c) * (f2 /. c) ) )
let f1, f2 be PartFunc of C,COMPLEX; :: thesis: ( dom (f1 (#) f2) = (dom f1) /\ (dom f2) & ( for c being Element of C st c in dom (f1 (#) f2) holds
(f1 (#) f2) /. c = (f1 /. c) * (f2 /. c) ) )
thus A1: dom (f1 (#) f2) = (dom f1) /\ (dom f2) by VALUED_1:def 4; :: thesis: for c being Element of C st c in dom (f1 (#) f2) holds
(f1 (#) f2) /. c = (f1 /. c) * (f2 /. c)

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

let c be Element of C; :: thesis: ( c in dom (f1 (#) f2) implies (f1 (#) f2) /. c = (f1 /. c) * (f2 /. c) )
assume A2: c in dom (f1 (#) f2) ; :: thesis: (f1 (#) f2) /. c = (f1 /. c) * (f2 /. c)
then c in dom f1 by A1, XBOOLE_0:def 4;
then A3: f1 . c = f1 /. c by PARTFUN1:def 6;
c in dom f2 by A1, A2, XBOOLE_0:def 4;
then A4: f2 . c = f2 /. c by PARTFUN1:def 6;
thus (f1 (#) f2) /. c = (f1 (#) f2) . c by A2, PARTFUN1:def 6
.= (f1 /. c) * (f2 /. c) by A2, A3, A4, VALUED_1:def 4 ; :: thesis: verum

end;

hence for c being Element of C st c in dom (f1 (#) f2) holds
(f1 (#) f2) /. c = (f1 /. c) * (f2 /. c) ; :: thesis: verum