theorem Th3: :: CFUNCT_1:3

for C being non empty set
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) ) )