let m be non zero Nat; :: thesis: for x, y, z, w being Element of REAL m
for i being Nat
for d, p, q, r being Real st 1 <= i & i <= m & |.(y - x).| < d & |.(z - x).| < d & p = (proj (i,m)) . y & z = (reproj (i,y)) . q & r in [.p,q.] & w = (reproj (i,y)) . r holds
|.(w - x).| < d
let x, y, z, w be Element of REAL m; :: thesis: for i being Nat
for d, p, q, r being Real st 1 <= i & i <= m & |.(y - x).| < d & |.(z - x).| < d & p = (proj (i,m)) . y & z = (reproj (i,y)) . q & r in [.p,q.] & w = (reproj (i,y)) . r holds
|.(w - x).| < d
let i be Nat; :: thesis: for d, p, q, r being Real st 1 <= i & i <= m & |.(y - x).| < d & |.(z - x).| < d & p = (proj (i,m)) . y & z = (reproj (i,y)) . q & r in [.p,q.] & w = (reproj (i,y)) . r holds
|.(w - x).| < d
let d, p, q, r be Real; :: thesis: ( 1 <= i & i <= m & |.(y - x).| < d & |.(z - x).| < d & p = (proj (i,m)) . y & z = (reproj (i,y)) . q & r in [.p,q.] & w = (reproj (i,y)) . r implies |.(w - x).| < d )
assume that
A1: ( 1 <= i & i <= m ) and
A2: ( |.(y - x).| < d & |.(z - x).| < d ) and
A3: ( p = (proj (i,m)) . y & z = (reproj (i,y)) . q ) and
A4: r in [.p,q.] and
A5: w = (reproj (i,y)) . r ; :: thesis: |.(w - x).| < d
set wx = w - x;
set yx = y - x;
set zx = z - x;
A6: ( Sum (sqr (y - x)) = |.(y - x).| ^2 & Sum (sqr (w - x)) = |.(w - x).| ^2 & Sum (sqr (z - x)) = |.(z - x).| ^2 ) by TOPREAL9:5;
A7: ( (proj (i,m)) . z = q & (proj (i,m)) . w = r ) by A1, A3, A5, Th39;
A8: ( p <= r & r <= q ) by A4, XXREAL_1:1;
i in Seg m by A1;
then A9: ( i in dom (y - x) & i in dom (w - x) & i in dom (z - x) ) by FINSEQ_1:89;
set x1 = x;
reconsider r = r as Element of REAL by XREAL_0:def 1;
A10: for l being Nat st l in Seg m & l <> i holds
(sqr (y - x)) . l = (sqr (w - x)) . l

proof

let l be Nat; :: thesis: ( l in Seg m & l <> i implies (sqr (y - x)) . l = (sqr (w - x)) . l )
assume A11: ( l in Seg m & l <> i ) ; :: thesis: (sqr (y - x)) . l = (sqr (w - x)) . l
then A12: ( l in dom (y - x) & l in dom (w - x) & l in dom y ) by FINSEQ_1:89;
then A13: l in Seg (len y) by FINSEQ_1:def 3;
then A14: ( 1 <= l & l <= len y ) by FINSEQ_1:1;
( l in Seg (len y) & l in Seg (len (Replace (y,i,r))) ) by A13, FINSEQ_7:5;
then A15: ( l in dom y & l in dom (Replace (y,i,r)) ) by FINSEQ_1:def 3;
( sqr (y - x) = sqrreal * (y - x) & sqr (w - x) = sqrreal * (w - x) ) by RVSUM_1:def 8;
then ( (sqr (y - x)) . l = sqrreal . ((y - x) . l) & (sqr (w - x)) . l = sqrreal . ((w - x) . l) ) by A12, FUNCT_1:13;
then ( (sqr (y - x)) . l = ((y - x) . l) ^2 & (sqr (w - x)) . l = ((w - x) . l) ^2 ) by RVSUM_1:def 2;
then A16: ( (sqr (y - x)) . l = ((y . l) - (x . l)) ^2 & (sqr (w - x)) . l = ((w . l) - (x . l)) ^2 ) by A12, VALUED_1:13;
w . l = (Replace (y,i,r)) . l by A5, PDIFF_1:def 5;
then w . l = (Replace (y,i,r)) /. l by A15, PARTFUN1:def 6;
then w . l = y /. l by A11, A14, FINSEQ_7:10;
hence (sqr (y - x)) . l = (sqr (w - x)) . l by A15, A16, PARTFUN1:def 6; :: thesis: verum

end;

A17: for l being Nat st l in Seg m & l <> i holds
(sqr (z - x)) . l = (sqr (w - x)) . l

proof

let l be Nat; :: thesis: ( l in Seg m & l <> i implies (sqr (z - x)) . l = (sqr (w - x)) . l )
assume A18: ( l in Seg m & l <> i ) ; :: thesis: (sqr (z - x)) . l = (sqr (w - x)) . l
then A19: ( l in dom (z - x) & l in dom (w - x) & l in dom z ) by FINSEQ_1:89;
then A20: l in Seg (len z) by FINSEQ_1:def 3;
then A21: ( 1 <= l & l <= len z ) by FINSEQ_1:1;
( l in Seg (len z) & l in Seg (len (Replace (z,i,r))) ) by A20, FINSEQ_7:5;
then A22: ( l in dom z & l in dom (Replace (z,i,r)) ) by FINSEQ_1:def 3;
( sqr (z - x) = sqrreal * (z - x) & sqr (w - x) = sqrreal * (w - x) ) by RVSUM_1:def 8;
then ( (sqr (z - x)) . l = sqrreal . ((z - x) . l) & (sqr (w - x)) . l = sqrreal . ((w - x) . l) ) by A19, FUNCT_1:13;
then ( (sqr (z - x)) . l = ((z - x) . l) ^2 & (sqr (w - x)) . l = ((w - x) . l) ^2 ) by RVSUM_1:def 2;
then A23: ( (sqr (z - x)) . l = ((z . l) - (x . l)) ^2 & (sqr (w - x)) . l = ((w . l) - (x . l)) ^2 ) by A19, VALUED_1:13;
w . l = ((reproj (i,z)) . r) . l by A1, A3, Th40, A5;
then w . l = (Replace (z,i,r)) . l by PDIFF_1:def 5;
then w . l = (Replace (z,i,r)) /. l by A22, PARTFUN1:def 6;
then w . l = z /. l by A18, A21, FINSEQ_7:10;
hence (sqr (z - x)) . l = (sqr (w - x)) . l by A22, A23, PARTFUN1:def 6; :: thesis: verum

end;

A24: now :: thesis: ( |.(w - x).| > |.(y - x).| implies not |.(w - x).| > |.(z - x).| )

assume A25: ( |.(w - x).| > |.(y - x).| & |.(w - x).| > |.(z - x).| ) ; :: thesis: contradiction

A26: now :: thesis: not (sqr (w - x)) . i <= (sqr (y - x)) . i

assume A27: (sqr (w - x)) . i <= (sqr (y - x)) . i ; :: thesis: contradiction
A28: len (sqr (w - x)) = m by CARD_1:def 7
.= len (sqr (y - x)) by CARD_1:def 7 ;
for l being Element of NAT st l in dom (sqr (w - x)) holds
(sqr (w - x)) . l <= (sqr (y - x)) . l

proof

let l be Element of NAT ; :: thesis: ( l in dom (sqr (w - x)) implies (sqr (w - x)) . l <= (sqr (y - x)) . l )
assume l in dom (sqr (w - x)) ; :: thesis: (sqr (w - x)) . l <= (sqr (y - x)) . l
then A29: l in Seg m by FINSEQ_1:89;

per cases ( l = i or l <> i ) ;

suppose l = i ; :: thesis: (sqr (w - x)) . l <= (sqr (y - x)) . l

hence (sqr (w - x)) . l <= (sqr (y - x)) . l by A27; :: thesis: verum

end;

suppose l <> i ; :: thesis: (sqr (w - x)) . l <= (sqr (y - x)) . l

hence (sqr (w - x)) . l <= (sqr (y - x)) . l by A29, A10; :: thesis: verum

end;

end;

end;

hence contradiction by A28, A6, A25, INTEGRA5:3, SQUARE_1:16; :: thesis: verum

end;

A30: now :: thesis: not (sqr (w - x)) . i <= (sqr (z - x)) . i

assume A31: (sqr (w - x)) . i <= (sqr (z - x)) . i ; :: thesis: contradiction
A32: len (sqr (w - x)) = m by CARD_1:def 7
.= len (sqr (z - x)) by CARD_1:def 7 ;
for l being Element of NAT st l in dom (sqr (w - x)) holds
(sqr (w - x)) . l <= (sqr (z - x)) . l

proof

let l be Element of NAT ; :: thesis: ( l in dom (sqr (w - x)) implies (sqr (w - x)) . l <= (sqr (z - x)) . l )
assume l in dom (sqr (w - x)) ; :: thesis: (sqr (w - x)) . l <= (sqr (z - x)) . l
then A33: l in Seg m by FINSEQ_1:89;

per cases ( l = i or l <> i ) ;

suppose l = i ; :: thesis: (sqr (w - x)) . l <= (sqr (z - x)) . l

hence (sqr (w - x)) . l <= (sqr (z - x)) . l by A31; :: thesis: verum

end;

suppose l <> i ; :: thesis: (sqr (w - x)) . l <= (sqr (z - x)) . l

hence (sqr (w - x)) . l <= (sqr (z - x)) . l by A33, A17; :: thesis: verum

end;

end;

end;

hence contradiction by A32, A6, A25, INTEGRA5:3, SQUARE_1:16; :: thesis: verum

end;

( sqr (y - x) = sqrreal * (y - x) & sqr (w - x) = sqrreal * (w - x) & sqr (z - x) = sqrreal * (z - x) ) by RVSUM_1:def 8;
then ( (sqr (y - x)) . i = sqrreal . ((y - x) . i) & (sqr (w - x)) . i = sqrreal . ((w - x) . i) & (sqr (z - x)) . i = sqrreal . ((z - x) . i) ) by A9, FUNCT_1:13;
then A34: ( (sqr (y - x)) . i = ((y - x) . i) ^2 & (sqr (w - x)) . i = ((w - x) . i) ^2 & (sqr (z - x)) . i = ((z - x) . i) ^2 ) by RVSUM_1:def 2;
( y . i = p & w . i = r & z . i = q ) by A3, A7, PDIFF_1:def 1;
then A35: ( (sqr (y - x)) . i = (p - (x . i)) ^2 & (sqr (w - x)) . i = (r - (x . i)) ^2 & (sqr (z - x)) . i = (q - (x . i)) ^2 ) by A34, A9, VALUED_1:13;
A36: p <= q by A8, XXREAL_0:2;

per cases ( x . i < p or ( p <= x . i & x . i <= r ) or ( r < x . i & x . i <= q ) or q < x . i ) ;

suppose x . i < p ; :: thesis: contradiction

then ( x . i < r & x . i < q ) by A8, A36, XXREAL_0:2;
then ( q - (x . i) > 0 & r - (x . i) > 0 ) by XREAL_1:50;
then q - (x . i) < r - (x . i) by A35, A30, SQUARE_1:15;
hence contradiction by A8, XREAL_1:13; :: thesis: verum

end;

suppose A37: ( p <= x . i & x . i <= r ) ; :: thesis: contradiction

then x . i <= q by A8, XXREAL_0:2;
then ( r - (x . i) >= 0 & q - (x . i) >= 0 ) by A37, XREAL_1:48;
then q - (x . i) < r - (x . i) by A35, A30, SQUARE_1:15;
hence contradiction by A8, XREAL_1:13; :: thesis: verum

end;

suppose A38: ( r < x . i & x . i <= q ) ; :: thesis: contradiction

then p < x . i by A8, XXREAL_0:2;
then A39: ( (x . i) - p >= 0 & (x . i) - r >= 0 ) by A38, XREAL_1:48;
( (p - (x . i)) ^2 = ((x . i) - p) ^2 & (r - (x . i)) ^2 = ((x . i) - r) ^2 ) ;
then (x . i) - p < (x . i) - r by A35, A26, A39, SQUARE_1:15;
hence contradiction by A8, XREAL_1:13; :: thesis: verum

end;

suppose q < x . i ; :: thesis: contradiction

then r < x . i by A8, XXREAL_0:2;
then ( p < x . i & r < x . i ) by A8, XXREAL_0:2;
then A40: ( (x . i) - r >= 0 & (x . i) - p >= 0 ) by XREAL_1:48;
( (p - (x . i)) ^2 = ((x . i) - p) ^2 & (r - (x . i)) ^2 = ((x . i) - r) ^2 ) ;
then (x . i) - p < (x . i) - r by A35, A26, A40, SQUARE_1:15;
hence contradiction by A8, XREAL_1:13; :: thesis: verum

end;

end;

end;

per cases ( |.(w - x).| <= |.(y - x).| or |.(w - x).| <= |.(z - x).| ) by A24;

suppose |.(w - x).| <= |.(y - x).| ; :: thesis: |.(w - x).| < d

hence |.(w - x).| < d by A2, XXREAL_0:2; :: thesis: verum

end;

suppose |.(w - x).| <= |.(z - x).| ; :: thesis: |.(w - x).| < d

hence |.(w - x).| < d by A2, XXREAL_0:2; :: thesis: verum

end;

end;