theorem Th6: :: PDIFF_9:6

for i being Element of NAT
for f being PartFunc of (REAL i),REAL
for x being Element of REAL i st x in dom f holds
( (<>* f) . x = <*(f . x)*> & (<>* f) /. x = <*(f /. x)*> )