:: deftheorem Def8 defines # RFUNCT_3:def 8 :
for D being non empty set
for f being FinSequence of PFuncs (D,REAL)
for d being Element of D
for b₄ being FinSequence of REAL holds
( b₄ = f # d iff ( len b₄ = len f & ( for n being Element of NAT st n in dom b₄ holds
b₄ . n = (f . n) . d ) ) );