:: deftheorem Def3 defines (#) VFUNCT_1:def 3 :
for C being non empty set
for V being non empty RLSStruct
for f1 being PartFunc of C,REAL
for f2, b₅ being PartFunc of C,V holds
( b₅ = f1 (#) f2 iff ( dom b₅ = (dom f1) /\ (dom f2) & ( for c being Element of C st c in dom b₅ holds
b₅ /. c = (f1 . c) * (f2 /. c) ) ) );