set W = (proj (1,1)) " ;
let u be PartFunc of (REAL 2),REAL; for x, y being Real st <*x,y*> in dom u holds
(<>* u) /. <*x,y*> = <*(u /. <*x,y*>)*>
let x, y be Real; ( <*x,y*> in dom u implies (<>* u) /. <*x,y*> = <*(u /. <*x,y*>)*> )
assume A1:
<*x,y*> in dom u
; (<>* 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
;
verum