let x, y be Element of REAL 1; :: thesis: (Pitag_dist 1) . (x,y) = |.((x . 1) - (y . 1)).|
A1: (Pitag_dist 1) . (x,y) = |.(x - y).| by EUCLID:def 6;
reconsider f = x - y as Element of (TOP-REAL 1) by EUCLID:22;
consider r being Real such that
A2: f = <*r*> by JORDAN2B:20;
sqr (x - y) = <*(r ^2)*> by A2, RVSUM_1:55;
then Sum (sqr (x - y)) = r ^2 by RVSUM_1:73;
then A3: sqrt (Sum (sqr (x - y))) = |.r.| by COMPLEX1:72;
( f . 1 = (x - y) . 1 & (x - y) . 1 = (x . 1) - (y . 1) ) by RVSUM_1:27;
hence (Pitag_dist 1) . (x,y) = |.((x . 1) - (y . 1)).| by A1, A3, A2, FINSEQ_1:def 8; :: thesis: verum