let i, n be Nat; :: thesis: 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); :: thesis: ( i in dom p1 implies ((p1 /. i) - (p2 /. i)) ^2 <= Sum (sqr (p1 - p2)) )
assume A1: i in dom p1 ; :: thesis: ((p1 /. i) - (p2 /. i)) ^2 <= Sum (sqr (p1 - p2))
set e = sqr (p1 - p2);
A2: now :: thesis: for i being Nat st i in dom (sqr (p1 - p2)) holds
0 <= (sqr (p1 - p2)) . i
let i be Nat; :: thesis: ( i in dom (sqr (p1 - p2)) implies 0 <= (sqr (p1 - p2)) . i )
assume i in dom (sqr (p1 - p2)) ; :: thesis: 0 <= (sqr (p1 - p2)) . i
(sqr (p1 - p2)) . i = ((p1 - p2) . i) ^2 by VALUED_1:11;
hence 0 <= (sqr (p1 - p2)) . i ; :: thesis: verum
end;
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; :: thesis: verum