set W = (proj (1,1)) " ;
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*>)*>
rng u c= dom ((proj (1,1)) ") by PDIFF_1:2;
then dom (<>* u) = dom u by RELAT_1:27;
hence (<>* u) /. <*x,y*> = (<>* u) . <*x,y*> by A1, PARTFUN1:def 6
.= ((proj (1,1)) ") . (u . <*x,y*>) by A1, FUNCT_1:13
.= <*(u . <*x,y*>)*> by PDIFF_1:1
.= <*(u /. <*x,y*>)*> by A1, PARTFUN1:def 6 ;
:: thesis: verum