let u be PartFunc of (REAL 2),REAL; :: thesis: for xy being Element of REAL 2 st xy in dom u holds
(<>* u) . xy = <*(u . xy)*>
let xy be Element of REAL 2; :: thesis: ( xy in dom u implies (<>* u) . xy = <*(u . xy)*> )
assume xy in dom u ; :: thesis: (<>* u) . xy = <*(u . xy)*>
hence (<>* u) . xy = ((proj (1,1)) ") . (u . xy) by FUNCT_1:13
.= <*(u . xy)*> by PDIFF_1:1 ;
:: thesis: verum