let p1, p2 be Element of REAL 3; |(p1,p2)| = (((p1 . 1) * (p2 . 1)) + ((p1 . 2) * (p2 . 2))) + ((p1 . 3) * (p2 . 3))
reconsider f1 = p1, f2 = p2 as FinSequence of REAL ;
A1: len f1 =
len <*(p1 . 1),(p1 . 2),(p1 . 3)*>
by Th1
.=
3
by FINSEQ_1:45
;
len f2 =
len <*(p2 . 1),(p2 . 2),(p2 . 3)*>
by Th1
.=
3
by FINSEQ_1:45
;
then |(p1,p2)| =
Sum <*((f1 . 1) * (f2 . 1)),((f1 . 2) * (f2 . 2)),((f1 . 3) * (f2 . 3))*>
by A1, EUCLID_5:28
.=
(((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))
; verum