:: deftheorem Def7 defines (#) RFUNCT_3:def 7 :
for D being non empty set
for f being FinSequence of PFuncs (D,REAL)
for R being FinSequence of REAL
for b₄ being FinSequence of PFuncs (D,REAL) holds
( b₄ = R (#) f iff ( len b₄ = min ((len R),(len f)) & ( for n being Nat st n in dom b₄ holds
for F being PartFunc of D,REAL
for r being Real st r = R . n & F = f . n holds
b₄ . n = r (#) F ) ) );