let p1, p2 be Point of (TOP-REAL 3); :: thesis: |(p1,p2)| = (((p1 `1 ) * (p2 `1 )) + ((p1 `2 ) * (p2 `2 ))) + ((p1 `3 ) * (p2 `3 ))
reconsider f1 = p1, f2 = p2 as FinSequence of REAL by EUCLID:27;
A1: len f1 = len <*(p1 `1 ),(p1 `2 ),(p1 `3 )*> by Th27
.= 3 by FINSEQ_1:62 ;
A2: len f2 = len <*(p2 `1 ),(p2 `2 ),(p2 `3 )*> by Th27
.= 3 by FINSEQ_1:62 ;
|(p1,p2)| = Sum (mlt f1,f2) by EUCLID_2:def 1
.= Sum <*((f1 . 1) * (f2 . 1)),((f1 . 2) * (f2 . 2)),((f1 . 3) * (f2 . 3))*> by A1, A2, Th28
.= (((p1 `1 ) * (p2 `1 )) + ((p1 `2 ) * (p2 `2 ))) + ((p1 `3 ) * (f2 . 3)) by RVSUM_1:108 ;
hence |(p1,p2)| = (((p1 `1 ) * (p2 `1 )) + ((p1 `2 ) * (p2 `2 ))) + ((p1 `3 ) * (p2 `3 )) ; :: thesis: verum