let i be Element of NAT ; :: thesis: 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)*> )
let f be PartFunc of (REAL i),REAL; :: thesis: for x being Element of REAL i st x in dom f holds
( (<>* f) . x = <*(f . x)*> & (<>* f) /. x = <*(f /. x)*> )
let x be Element of REAL i; :: thesis: ( x in dom f implies ( (<>* f) . x = <*(f . x)*> & (<>* f) /. x = <*(f /. x)*> ) )
set I = (proj (1,1)) " ;
assume A1: x in dom f ; :: thesis: ( (<>* f) . x = <*(f . x)*> & (<>* f) /. x = <*(f /. x)*> )
then (<>* f) . x = ((proj (1,1)) ") . (f . x) by FUNCT_1:13;
hence A2: (<>* f) . x = <*(f . x)*> by PDIFF_1:1; :: thesis: (<>* f) /. x = <*(f /. x)*>
x in dom (<>* f) by A1, Th3;
then (<>* f) /. x = (<>* f) . x by PARTFUN1:def 6;
hence (<>* f) /. x = <*(f /. x)*> by A1, A2, PARTFUN1:def 6; :: thesis: verum