reconsider A = |[0,0]|, B = |[1,1]| as Element of REAL 2 by EUCLID:22;
( |[0,0]| `1 = 0 & |[0,0]| `2 = 0 & |[1,1]| `1 = 1 & |[1,1]| `2 = 1 ) by EUCLID:52;
then A1: ( (A - B) . 1 = 0 - 1 & (A - B) . 2 = 0 - 1 ) by RVSUM_1:27;
reconsider f = A - B as FinSequence of REAL ;
( len f = len (A - B) & len (A - B) = 2 ) by FINSEQ_2:132;
then A2: |.(A - B).| = sqrt (((- 1) ^2) + ((- 1) ^2)) by A1, EUCLID_3:22;
(- 1) ^2 = 1 ^2 by SQUARE_1:3
.= 1 * 1 by SQUARE_1:def 1
.= 1 ;
hence (Pitag_dist 2) . (|[0,0]|,|[1,1]|) = sqrt 2 by A2, EUCLID:def 6; :: thesis: verum