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);

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

((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

A3:
dom (sqr (p1 - p2)) = dom (p1 - p2)
by VALUED_1:11;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;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

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