let f be Function of E,F; ( f is isometric & f is midpoints-preserving implies f is Affine )
assume that
A1:
f is isometric
and
A2:
f is midpoints-preserving
; f is Affine
let a be Point of E; MAZURULM:def 2 for b being Point of E
for t being Real st 0 <= t & t <= 1 holds
f . (((1 - t) * a) + (t * b)) = ((1 - t) * (f . a)) + (t * (f . b))
let b be Point of E; for t being Real st 0 <= t & t <= 1 holds
f . (((1 - t) * a) + (t * b)) = ((1 - t) * (f . a)) + (t * (f . b))
let t be Real; ( 0 <= t & t <= 1 implies f . (((1 - t) * a) + (t * b)) = ((1 - t) * (f . a)) + (t * (f . b)) )
assume
( 0 <= t & t <= 1 )
; f . (((1 - t) * a) + (t * b)) = ((1 - t) * (f . a)) + (t * (f . b))
then
t in [.0,1.]
by XXREAL_1:1;
then consider s being Real_Sequence such that
A3:
rng s c= DYADIC
and
A4:
s is convergent
and
A5:
lim s = t
by Th2, MEASURE6:64;
A6:
dom f = the carrier of E
by FUNCT_2:def 1;
set stb = s * b;
set 1t = 1 + (- s);
set s1ta = (1 + (- s)) * a;
set s1 = ((1 + (- s)) * a) + (s * b);
set za = (1 + (- s)) * (f . a);
set zb = s * (f . b);
A7:
f is_continuous_on dom f
by A1, Th24;
A8:
- s is convergent
by A4;
A9:
((1 + (- s)) * a) + (s * b) is convergent
by A4, NORMSP_1:19;
A10:
lim ((1 + (- s)) * a) = (lim (1 + (- s))) * a
by A8, Th10;
A11:
lim (- s) = - (lim s)
by A4, SEQ_2:10;
A12: lim (1 + (- s)) =
1 + (lim (- s))
by A8, Th7
.=
1 - (lim s)
by A11
.=
1 - t
by A5
;
lim (s * b) = (lim s) * b
by A4, Th10;
then A13:
lim (((1 + (- s)) * a) + (s * b)) = ((1 - t) * a) + (t * b)
by A5, A10, A12, A4, NORMSP_1:25;
A14:
lim ((1 + (- s)) * (f . a)) = (1 - t) * (f . a)
by A8, A12, Th10;
A15:
lim (s * (f . b)) = t * (f . b)
by A4, A5, Th10;
A16:
f /* (((1 + (- s)) * a) + (s * b)) = ((1 + (- s)) * (f . a)) + (s * (f . b))
A21:
rng (((1 + (- s)) * a) + (s * b)) c= the carrier of E
;
thus f . (((1 - t) * a) + (t * b)) =
f /. (((1 - t) * a) + (t * b))
.=
lim (f /* (((1 + (- s)) * a) + (s * b)))
by A6, A7, A21, A9, A13, NFCONT_1:18
.=
((1 - t) * (f . a)) + (t * (f . b))
by A14, A15, A4, A16, NORMSP_1:25
; verum