let i, n be Nat; for p1, p2 being Point of (TOP-REAL n) st i in dom p1 holds
((p1 /. i) - (p2 /. i)) ^2 <= Sum (sqr (p1 - p2))
let p1, p2 be Point of (TOP-REAL n); ( i in dom p1 implies ((p1 /. i) - (p2 /. i)) ^2 <= Sum (sqr (p1 - p2)) )
assume A1:
i in dom p1
; ((p1 /. i) - (p2 /. i)) ^2 <= Sum (sqr (p1 - p2))
set e = sqr (p1 - p2);
A3:
dom (sqr (p1 - p2)) = dom (p1 - p2)
by VALUED_1:11;
A4:
dom (p1 - p2) = (dom p1) /\ (dom p2)
by VALUED_1:12;
A5: dom p1 =
Seg n
by FINSEQ_1:89
.=
dom p2
by FINSEQ_1:89
;
A6:
p1 . i = p1 /. i
by A1, PARTFUN1:def 6;
A7:
p2 . i = p2 /. i
by A1, A5, PARTFUN1:def 6;
(sqr (p1 - p2)) . i =
((p1 - p2) . i) ^2
by VALUED_1:11
.=
((p1 /. i) - (p2 /. i)) ^2
by A6, A7, A1, A5, A4, VALUED_1:13
;
hence
((p1 /. i) - (p2 /. i)) ^2 <= Sum (sqr (p1 - p2))
by A1, A2, A3, A5, A4, MATRPROB:5; verum