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:24;
A1: len f1 = len <*(p1 `1),(p1 `2),(p1 `3)*> by Th27
.= 3 by FINSEQ_1:45 ;
A2: len f2 = len <*(p2 `1),(p2 `2),(p2 `3)*> by Th27
.= 3 by FINSEQ_1:45 ;
|(p1,p2)| = Sum (mlt (f1,f2)) by RVSUM_1:def 16
.= 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:78 ;
hence |(p1,p2)| = (((p1 `1) * (p2 `1)) + ((p1 `2) * (p2 `2))) + ((p1 `3) * (p2 `3)) ; :: thesis: verum