let n be Element of NAT ; :: thesis: for x, y being Element of REAL n
for u, v being Point of (REAL-US n) st x = u & y = v holds
(Euclid_scalar n) . u,v = |(x,y)|
let x, y be Element of REAL n; :: thesis: for u, v being Point of (REAL-US n) st x = u & y = v holds
(Euclid_scalar n) . u,v = |(x,y)|
let u, v be Point of (REAL-US n); :: thesis: ( x = u & y = v implies (Euclid_scalar n) . u,v = |(x,y)| )
assume ( x = u & y = v ) ; :: thesis: (Euclid_scalar n) . u,v = |(x,y)|
hence (Euclid_scalar n) . u,v = (Euclid_scalar n) . x,y
.= |(x,y)| by REAL_NS1:def 5 ;
:: thesis: verum