let u be PartFunc of (REAL 2),REAL ; :: thesis: for x, y being Real st <*x,y*> in dom u holds
(<>* u) /. <*x,y*> = <*(u /. <*x,y*>)*>
let x, y be Real; :: thesis: ( <*x,y*> in dom u implies (<>* u) /. <*x,y*> = <*(u /. <*x,y*>)*> )
assume A1: <*x,y*> in dom u ; :: thesis: (<>* u) /. <*x,y*> = <*(u /. <*x,y*>)*>
set W = (proj 1,1) " ;
rng u c= dom ((proj 1,1) " ) by PDIFF_1:2;
then dom (<>* u) = dom u by RELAT_1:46;
hence (<>* u) /. <*x,y*> = (<>* u) . <*x,y*> by A1, PARTFUN1:def 8
.= ((proj 1,1) " ) . (u . <*x,y*>) by A1, FUNCT_1:23
.= <*(u . <*x,y*>)*> by PDIFF_1:1
.= <*(u /. <*x,y*>)*> by A1, PARTFUN1:def 8 ;
:: thesis: verum