:: MAZURULM semantic presentation

begin


registration
cluster I[01]  ->  closed for SubSpace of R^1 ;
coherence
 for b1 being SubSpace of R^1 st b1 = I[01] holds
b1 is closed by TOPMETR:20, TREAL_1:2;
end;

reconsider D = DYADIC as Subset of I[01] by BORSUK_1:40, URYSOHN2:28;

Lm1:  Cl D = [#] I[01]
proof
reconsider P = [.0,1.] as Subset of R^1 by MEMBERED:3, TOPMETR:17;
A1: I[01] = R^1 | P by TOPMETR:19, TOPMETR:20;
reconsider D1 = D as Subset of (R^1 | P) by TOPMETR:19, TOPMETR:20;
A2: Cl D = (Cl (Up D1)) /\ P by A1, CONNSP_3:30;
thus  Cl D c= [#] I[01] ; :: according to XBOOLE_0:def_10 ::_thesis: [#] I[01] c= Cl D
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in [#] I[01] or x in Cl D )
assume A3: x in [#] I[01] ; ::_thesis: x in Cl D
reconsider p = x as Point of RealSpace by A3, BORSUK_1:40;
now__::_thesis:_for_r_being_real_number_st_r_>_0_holds_
Ball_(p,r)_meets_D
let r be real number ; ::_thesis: ( r > 0 implies Ball (p,b1) meets D )
assume A4: r > 0 ; ::_thesis: Ball (p,b1) meets D
A5: p - r < p - 0 by A4, XREAL_1:10;
A6: p <= 1 by A3, BORSUK_1:43;
 r is Real by XREAL_0:def_1;
then A7: Ball (p,r) = ].(p - r),(p + r).[ by FRECHET:7;
percases ( r <= p or r > p ) ;
suppose r <= p ; ::_thesis: Ball (p,b1) meets D
then  r - r <= p - r by XREAL_1:9;
then consider c being Real such that
A8: c in D and
A9: p - r < c and
A10: c < p by A5, A6, URYSOHN2:24;
 p + 0 < p + r by A4, XREAL_1:8;
then  c < p + r by A10, XXREAL_0:2;
then  c in Ball (p,r) by A9, A7, XXREAL_1:4;
hence  Ball (p,r) meets D by A8, XBOOLE_0:3; ::_thesis: verum
end;
suppose r > p ; ::_thesis: Ball (p,b1) meets D
then A11: p - r < p - p by XREAL_1:10;
 0 <= p by A3, BORSUK_1:43;
then  0 in Ball (p,r) by A4, A11, A7, XXREAL_1:4;
hence  Ball (p,r) meets D by URYSOHN2:27, XBOOLE_0:3; ::_thesis: verum
end;
end;
end;
then  x in Cl (Up D1) by GOBOARD6:92, TOPMETR:def_6;
hence  x in Cl D by A3, A2, BORSUK_1:40, XBOOLE_0:def_4; ::_thesis: verum
end;

theorem :: MAZURULM:1
DYADIC is dense Subset of I[01]
proof
 D is dense
proof
thus  Cl D = [#] I[01] by Lm1; :: according to TOPS_1:def_3 ::_thesis: verum
end;
hence  DYADIC is dense Subset of I[01] ; ::_thesis: verum
end;

theorem Th2: :: MAZURULM:2
Cl DYADIC = [.0,1.]
proof
reconsider W = D as Subset of R^1 by TOPMETR:17;
thus  Cl DYADIC = Cl W by JORDAN5A:24
.= [.0,1.] by Lm1, BORSUK_1:40, TOPS_3:55 ; ::_thesis: verum
end;

theorem Th3: :: MAZURULM:3
for E being RealNormSpace
for a being Point of E holds a + a = 2 * a
proof
let E be RealNormSpace; ::_thesis: for a being Point of E holds a + a = 2 * a
let a be Point of E; ::_thesis: a + a = 2 * a
 1 * a = a by RLVECT_1:def_8;
hence a + a = (1 + 1) * a by RLVECT_1:def_6
.= 2 * a ;
::_thesis: verum
end;

theorem Th4: :: MAZURULM:4
for E being RealNormSpace
for a, b being Point of E holds (a + b) - b = a
proof
let E be RealNormSpace; ::_thesis: for a, b being Point of E holds (a + b) - b = a
let a, b be Point of E; ::_thesis: (a + b) - b = a
thus (a + b) - b = a + (b - b) by RLVECT_1:28
.= a + (0. E) by RLVECT_1:15
.= a by RLVECT_1:4 ; ::_thesis: verum
end;

registration
let A be real-membered bounded_above set ;
let r be real non negative number ;
clusterr ** A ->  bounded_above ;
coherence
 r ** A is bounded_above
proof
percases ( A <> {} or A = {} ) ;
supposeA1: A <> {} ; ::_thesis: r ** A is bounded_above
A2: r in REAL by XREAL_0:def_1;
 A c= REAL by MEMBERED:3;
hence  r ** A is bounded_above by A1, A2, INTEGRA2:9; ::_thesis: verum
end;
suppose A = {} ; ::_thesis: r ** A is bounded_above
hence  r ** A is bounded_above ; ::_thesis: verum
end;
end;
end;
end;

registration
let A be real-membered bounded_above set ;
let r be real non positive number ;
clusterr ** A ->  bounded_below ;
coherence
 r ** A is bounded_below
proof
percases ( A <> {} or A = {} ) ;
supposeA1: A <> {} ; ::_thesis: r ** A is bounded_below
A2: r in REAL by XREAL_0:def_1;
 A c= REAL by MEMBERED:3;
hence  r ** A is bounded_below by A1, A2, INTEGRA2:10; ::_thesis: verum
end;
suppose A = {} ; ::_thesis: r ** A is bounded_below
hence  r ** A is bounded_below ; ::_thesis: verum
end;
end;
end;
end;

registration
let A be real-membered bounded_below set ;
let r be real non negative number ;
clusterr ** A ->  bounded_below ;
coherence
 r ** A is bounded_below
proof
percases ( A <> {} or A = {} ) ;
supposeA1: A <> {} ; ::_thesis: r ** A is bounded_below
A2: r in REAL by XREAL_0:def_1;
 A c= REAL by MEMBERED:3;
hence  r ** A is bounded_below by A1, A2, INTEGRA2:11; ::_thesis: verum
end;
suppose A = {} ; ::_thesis: r ** A is bounded_below
hence  r ** A is bounded_below ; ::_thesis: verum
end;
end;
end;
end;

registration
let A be non empty real-membered bounded_below set ;
let r be real non positive number ;
clusterr ** A ->  bounded_above ;
coherence
 r ** A is bounded_above
proof
A1: r in REAL by XREAL_0:def_1;
 A c= REAL by MEMBERED:3;
hence  r ** A is bounded_above by A1, INTEGRA2:12; ::_thesis: verum
end;
end;

theorem Th5: :: MAZURULM:5
for t being real number
for f being Real_Sequence holds f + (NAT --> t) = t + f
proof
let t be real number ; ::_thesis: for f being Real_Sequence holds f + (NAT --> t) = t + f
let f be Real_Sequence; ::_thesis: f + (NAT --> t) = t + f
let n be Element of NAT ; :: according to FUNCT_2:def_8 ::_thesis: (f + (NAT --> t)) . n = (t + f) . n
A1: (NAT --> t) . n = t by FUNCOP_1:7;
thus (f + (NAT --> t)) . n = (f . n) + ((NAT --> t) . n) by VALUED_1:1
.= (f + t) . n by A1, VALUED_1:2 ; ::_thesis: verum
end;

theorem Th6: :: MAZURULM:6
for r being Real holds lim (NAT --> r) = r
proof
let r be Real; ::_thesis: lim (NAT --> r) = r
thus  lim (NAT --> r) = (NAT --> r) . 0 by SEQ_4:26
.= r by FUNCOP_1:7 ; ::_thesis: verum
end;

theorem Th7: :: MAZURULM:7
for t being real number
for f being convergent Real_Sequence holds lim (t + f) = t + (lim f)
proof
let t be real number ; ::_thesis: for f being convergent Real_Sequence holds lim (t + f) = t + (lim f)
let f be convergent Real_Sequence; ::_thesis: lim (t + f) = t + (lim f)
reconsider r = t as Real by XREAL_0:def_1;
 f + (NAT --> t) = t + f by Th5;
hence  lim (t + f) = (lim (NAT --> r)) + (lim f) by SEQ_2:6
.= t + (lim f) by Th6 ;
::_thesis: verum
end;

registration
let f be convergent Real_Sequence;
let t be real number ;
clustert + f ->  convergent for Real_Sequence;
coherence
 for b1 being Real_Sequence st b1 = t + f holds
b1 is convergent
proof
reconsider r = t as Real by XREAL_0:def_1;
 f + (NAT --> r) = t + f by Th5;
hence  for b1 being Real_Sequence st b1 = t + f holds
b1 is convergent by SEQ_2:5; ::_thesis: verum
end;
end;

theorem Th8: :: MAZURULM:8
for E being RealNormSpace
for a being Point of E
for f being Real_Sequence holds f (#) (NAT --> a) = f * a
proof
let E be RealNormSpace; ::_thesis: for a being Point of E
for f being Real_Sequence holds f (#) (NAT --> a) = f * a
let a be Point of E; ::_thesis: for f being Real_Sequence holds f (#) (NAT --> a) = f * a
let f be Real_Sequence; ::_thesis: f (#) (NAT --> a) = f * a
let n be Element of NAT ; :: according to FUNCT_2:def_8 ::_thesis: (f (#) (NAT --> a)) . n = (f * a) . n
A1: (NAT --> a) . n = a by FUNCOP_1:7;
thus (f (#) (NAT --> a)) . n = (f . n) * ((NAT --> a) . n) by NDIFF_1:def_2
.= (f * a) . n by A1, NDIFF_1:def_3 ; ::_thesis: verum
end;

theorem Th9: :: MAZURULM:9
for E being RealNormSpace
for a being Point of E holds lim (NAT --> a) = a
proof
let E be RealNormSpace; ::_thesis: for a being Point of E holds lim (NAT --> a) = a
let a be Point of E; ::_thesis: lim (NAT --> a) = a
thus  lim (NAT --> a) = (NAT --> a) . 0 by NDIFF_1:18
.= a by FUNCOP_1:7 ; ::_thesis: verum
end;

theorem Th10: :: MAZURULM:10
for E being RealNormSpace
for a being Point of E
for f being convergent Real_Sequence holds lim (f * a) = (lim f) * a
proof
let E be RealNormSpace; ::_thesis: for a being Point of E
for f being convergent Real_Sequence holds lim (f * a) = (lim f) * a
let a be Point of E; ::_thesis: for f being convergent Real_Sequence holds lim (f * a) = (lim f) * a
let f be convergent Real_Sequence; ::_thesis: lim (f * a) = (lim f) * a
 f (#) (NAT --> a) = f * a by Th8;
hence  lim (f * a) = (lim f) * (lim (NAT --> a)) by NDIFF_1:14, NDIFF_1:18
.= (lim f) * a by Th9 ;
::_thesis: verum
end;

registration
let f be convergent Real_Sequence;
let E be RealNormSpace;
let a be Point of E;
clusterf * a ->  convergent ;
coherence
 f * a is convergent
proof
 f (#) (NAT --> a) = f * a by Th8;
hence  f * a is convergent by NDIFF_1:13, NDIFF_1:18; ::_thesis: verum
end;
end;

definition
let E, F be non empty NORMSTR ;
let f be Function of E,F;
attrf is isometric  means :Def1: :: MAZURULM:def 1
 for a, b being Point of E holds ||.((f . a) - (f . b)).|| = ||.(a - b).||;
end;

:: deftheorem Def1 defines isometric MAZURULM:def_1_:_
 for E, F being non empty NORMSTR
for f being Function of E,F holds
( f is isometric iff for a, b being Point of E holds ||.((f . a) - (f . b)).|| = ||.(a - b).|| );

definition
let E, F be non empty RLSStruct ;
let f be Function of E,F;
attrf is Affine  means :Def2: :: MAZURULM:def 2
 for a, b being Point of E
for t being real number st 0 <= t & t <= 1 holds
f . (((1 - t) * a) + (t * b)) = ((1 - t) * (f . a)) + (t * (f . b));
attrf is midpoints-preserving  means :Def3: :: MAZURULM:def 3
 for a, b being Point of E holds f . ((1 / 2) * (a + b)) = (1 / 2) * ((f . a) + (f . b));
end;

:: deftheorem Def2 defines Affine MAZURULM:def_2_:_
 for E, F being non empty RLSStruct
for f being Function of E,F holds
( f is Affine iff for a, b being Point of E
for t being real number st 0 <= t & t <= 1 holds
f . (((1 - t) * a) + (t * b)) = ((1 - t) * (f . a)) + (t * (f . b)) );

:: deftheorem Def3 defines midpoints-preserving MAZURULM:def_3_:_
 for E, F being non empty RLSStruct
for f being Function of E,F holds
( f is midpoints-preserving iff for a, b being Point of E holds f . ((1 / 2) * (a + b)) = (1 / 2) * ((f . a) + (f . b)) );

registration
let E be non empty NORMSTR ;
cluster id E ->  isometric ;
coherence
 id E is isometric
proof
let a, b be Point of E; :: according to MAZURULM:def_1 ::_thesis: ||.(((id E) . a) - ((id E) . b)).|| = ||.(a - b).||
 ( (id E) . a = a & (id E) . b = b ) by FUNCT_1:18;
hence  ||.(((id E) . a) - ((id E) . b)).|| = ||.(a - b).|| ; ::_thesis: verum
end;
end;

registration
let E be non empty RLSStruct ;
cluster id E ->  Affine midpoints-preserving ;
coherence
 ( id E is midpoints-preserving & id E is Affine )
proof
thus  id E is midpoints-preserving ::_thesis: id E is Affine
proof
let a, b be Point of E; :: according to MAZURULM:def_3 ::_thesis: (id E) . ((1 / 2) * (a + b)) = (1 / 2) * (((id E) . a) + ((id E) . b))
 ( (id E) . a = a & (id E) . b = b ) by FUNCT_1:18;
hence  (id E) . ((1 / 2) * (a + b)) = (1 / 2) * (((id E) . a) + ((id E) . b)) by FUNCT_1:18; ::_thesis: verum
end;
let a, b be Point of E; :: according to MAZURULM:def_2 ::_thesis: for t being real number st 0 <= t & t <= 1 holds
(id E) . (((1 - t) * a) + (t * b)) = ((1 - t) * ((id E) . a)) + (t * ((id E) . b))
 ( (id E) . a = a & (id E) . b = b ) by FUNCT_1:18;
hence  for t being real number st 0 <= t & t <= 1 holds
(id E) . (((1 - t) * a) + (t * b)) = ((1 - t) * ((id E) . a)) + (t * ((id E) . b)) by FUNCT_1:18; ::_thesis: verum
end;
end;

registration
let E be non empty NORMSTR ;
cluster non empty V4() V7( the carrier of E) V8( the carrier of E) Function-like total quasi_total bijective isometric Affine midpoints-preserving for Element of K10(K11( the carrier of E, the carrier of E));
existence
 ex b1 being UnOp of E st
( b1 is bijective & b1 is isometric & b1 is midpoints-preserving & b1 is Affine )
proof
take  id E ; ::_thesis: ( id E is bijective & id E is isometric & id E is midpoints-preserving & id E is Affine )
thus  ( id E is bijective & id E is isometric & id E is midpoints-preserving & id E is Affine ) ; ::_thesis: verum
end;
end;

theorem Th11: :: MAZURULM:11
for E, F, G being RealNormSpace
for f being Function of E,F
for g being Function of F,G st f is isometric & g is isometric holds
g * f is isometric
proof
let E, F, G be RealNormSpace; ::_thesis: for f being Function of E,F
for g being Function of F,G st f is isometric & g is isometric holds
g * f is isometric
let f be Function of E,F; ::_thesis: for g being Function of F,G st f is isometric & g is isometric holds
g * f is isometric
let g be Function of F,G; ::_thesis: ( f is isometric & g is isometric implies g * f is isometric )
assume that
A1: f is isometric and
A2: g is isometric ; ::_thesis: g * f is isometric
set h = g * f;
let a be Point of E; :: according to MAZURULM:def_1 ::_thesis: for b being Point of E holds ||.(((g * f) . a) - ((g * f) . b)).|| = ||.(a - b).||
let b be Point of E; ::_thesis: ||.(((g * f) . a) - ((g * f) . b)).|| = ||.(a - b).||
 ( (g * f) . a = g . (f . a) & (g * f) . b = g . (f . b) ) by FUNCT_2:15;
hence ||.(((g * f) . a) - ((g * f) . b)).|| = ||.((f . a) - (f . b)).|| by A2, Def1
.= ||.(a - b).|| by A1, Def1 ;
::_thesis: verum
end;

registration
let E be RealNormSpace;
let f, g be isometric UnOp of E;
clusterg * f ->  isometric for UnOp of E;
coherence
 for b1 being UnOp of E st b1 = g * f holds
b1 is isometric by Th11;
end;

Lm2: now__::_thesis:_for_E,_F_being_RealNormSpace
for_f_being_Function_of_E,F_st_f_is_bijective_holds_
for_a_being_Point_of_F_holds_f_._((f_/")_._a)_=_a
let E, F be RealNormSpace; ::_thesis: for f being Function of E,F st f is bijective holds
for a being Point of F holds f . ((f /") . a) = a
let f be Function of E,F; ::_thesis: ( f is bijective implies for a being Point of F holds f . ((f /") . a) = a )
assume A1: f is bijective ; ::_thesis: for a being Point of F holds f . ((f /") . a) = a
set g = f /" ;
let a be Point of F; ::_thesis: f . ((f /") . a) = a
 rng f = [#] F by A1, FUNCT_2:def_3;
then A2: (f /") /" = f by A1, TOPS_2:51;
A3: f /" = f " by A1, TOPS_2:def_4;
A4: f /" is bijective by A1, PENCIL_2:12;
 f = (f /") " by A2, A4, TOPS_2:def_4;
hence  f . ((f /") . a) = a by A1, A3, FUNCT_2:26; ::_thesis: verum
end;

theorem Th12: :: MAZURULM:12
for E, F being RealNormSpace
for f being Function of E,F st f is bijective & f is isometric holds
f /" is isometric
proof
let E, F be RealNormSpace; ::_thesis: for f being Function of E,F st f is bijective & f is isometric holds
f /" is isometric
let f be Function of E,F; ::_thesis: ( f is bijective & f is isometric implies f /" is isometric )
assume that
A1: f is bijective and
A2: f is isometric ; ::_thesis: f /" is isometric
set g = f /" ;
let a, b be Point of F; :: according to MAZURULM:def_1 ::_thesis: ||.(((f /") . a) - ((f /") . b)).|| = ||.(a - b).||
 ( f . ((f /") . a) = a & f . ((f /") . b) = b ) by A1, Lm2;
hence  ||.(((f /") . a) - ((f /") . b)).|| = ||.(a - b).|| by A2, Def1; ::_thesis: verum
end;

registration
let E be RealNormSpace;
let f be bijective isometric UnOp of E;
clusterf /"  ->  isometric ;
coherence
 f /" is isometric by Th12;
end;

theorem Th13: :: MAZURULM:13
for E, F, G being RealNormSpace
for f being Function of E,F
for g being Function of F,G st f is midpoints-preserving & g is midpoints-preserving holds
g * f is midpoints-preserving
proof
let E, F, G be RealNormSpace; ::_thesis: for f being Function of E,F
for g being Function of F,G st f is midpoints-preserving & g is midpoints-preserving holds
g * f is midpoints-preserving
let f be Function of E,F; ::_thesis: for g being Function of F,G st f is midpoints-preserving & g is midpoints-preserving holds
g * f is midpoints-preserving
let g be Function of F,G; ::_thesis: ( f is midpoints-preserving & g is midpoints-preserving implies g * f is midpoints-preserving )
assume that
A1: f is midpoints-preserving and
A2: g is midpoints-preserving ; ::_thesis: g * f is midpoints-preserving
set h = g * f;
let a be Point of E; :: according to MAZURULM:def_3 ::_thesis: for b being Point of E holds (g * f) . ((1 / 2) * (a + b)) = (1 / 2) * (((g * f) . a) + ((g * f) . b))
let b be Point of E; ::_thesis: (g * f) . ((1 / 2) * (a + b)) = (1 / 2) * (((g * f) . a) + ((g * f) . b))
A3: ( (g * f) . a = g . (f . a) & (g * f) . b = g . (f . b) ) by FUNCT_2:15;
thus (g * f) . ((1 / 2) * (a + b)) = g . (f . ((1 / 2) * (a + b))) by FUNCT_2:15
.= g . ((1 / 2) * ((f . a) + (f . b))) by A1, Def3
.= (1 / 2) * (((g * f) . a) + ((g * f) . b)) by A3, A2, Def3 ; ::_thesis: verum
end;

registration
let E be RealNormSpace;
let f, g be midpoints-preserving UnOp of E;
clusterg * f ->  midpoints-preserving for UnOp of E;
coherence
 for b1 being UnOp of E st b1 = g * f holds
b1 is midpoints-preserving by Th13;
end;

Lm3: now__::_thesis:_for_E,_F_being_RealNormSpace
for_f_being_Function_of_E,F_st_f_is_bijective_holds_
(f_/")_*_f_=_id_E
let E, F be RealNormSpace; ::_thesis: for f being Function of E,F st f is bijective holds
(f /") * f = id E
let f be Function of E,F; ::_thesis: ( f is bijective implies (f /") * f = id E )
assume A1: f is bijective ; ::_thesis: (f /") * f = id E
then A2: rng f = [#] F by FUNCT_2:def_3;
 dom f = [#] E by FUNCT_2:def_1;
hence  (f /") * f = id E by A1, A2, TOPS_2:52; ::_thesis: verum
end;

theorem Th14: :: MAZURULM:14
for E, F being RealNormSpace
for f being Function of E,F st f is bijective & f is midpoints-preserving holds
f /" is midpoints-preserving
proof
let E, F be RealNormSpace; ::_thesis: for f being Function of E,F st f is bijective & f is midpoints-preserving holds
f /" is midpoints-preserving
let f be Function of E,F; ::_thesis: ( f is bijective & f is midpoints-preserving implies f /" is midpoints-preserving )
assume that
A1: f is bijective and
A2: f is midpoints-preserving ; ::_thesis: f /" is midpoints-preserving
set g = f /" ;
let a, b be Point of F; :: according to MAZURULM:def_3 ::_thesis: (f /") . ((1 / 2) * (a + b)) = (1 / 2) * (((f /") . a) + ((f /") . b))
A3: (f /") * f = id E by A1, Lm3;
 ( f . ((f /") . a) = a & f . ((f /") . b) = b ) by A1, Lm2;
hence (f /") . ((1 / 2) * (a + b)) = (f /") . (f . ((1 / 2) * (((f /") . a) + ((f /") . b)))) by A2, Def3
.= ((f /") * f) . ((1 / 2) * (((f /") . a) + ((f /") . b))) by FUNCT_2:15
.= (1 / 2) * (((f /") . a) + ((f /") . b)) by A3, FUNCT_1:18 ;
::_thesis: verum
end;

registration
let E be RealNormSpace;
let f be bijective midpoints-preserving UnOp of E;
clusterf /"  ->  midpoints-preserving ;
coherence
 f /" is midpoints-preserving by Th14;
end;

theorem Th15: :: MAZURULM:15
for E, F, G being RealNormSpace
for f being Function of E,F
for g being Function of F,G st f is Affine & g is Affine holds
g * f is Affine
proof
let E, F, G be RealNormSpace; ::_thesis: for f being Function of E,F
for g being Function of F,G st f is Affine & g is Affine holds
g * f is Affine
let f be Function of E,F; ::_thesis: for g being Function of F,G st f is Affine & g is Affine holds
g * f is Affine
let g be Function of F,G; ::_thesis: ( f is Affine & g is Affine implies g * f is Affine )
assume that
A1: f is Affine and
A2: g is Affine ; ::_thesis: g * f is Affine
set h = g * f;
let a be Point of E; :: according to MAZURULM:def_2 ::_thesis: for b being Point of E
for t being real number st 0 <= t & t <= 1 holds
(g * f) . (((1 - t) * a) + (t * b)) = ((1 - t) * ((g * f) . a)) + (t * ((g * f) . b))
let b be Point of E; ::_thesis: for t being real number st 0 <= t & t <= 1 holds
(g * f) . (((1 - t) * a) + (t * b)) = ((1 - t) * ((g * f) . a)) + (t * ((g * f) . b))
let t be real number ; ::_thesis: ( 0 <= t & t <= 1 implies (g * f) . (((1 - t) * a) + (t * b)) = ((1 - t) * ((g * f) . a)) + (t * ((g * f) . b)) )
assume A3: ( 0 <= t & t <= 1 ) ; ::_thesis: (g * f) . (((1 - t) * a) + (t * b)) = ((1 - t) * ((g * f) . a)) + (t * ((g * f) . b))
A4: ( (g * f) . a = g . (f . a) & (g * f) . b = g . (f . b) ) by FUNCT_2:15;
thus (g * f) . (((1 - t) * a) + (t * b)) = g . (f . (((1 - t) * a) + (t * b))) by FUNCT_2:15
.= g . (((1 - t) * (f . a)) + (t * (f . b))) by A1, A3, Def2
.= ((1 - t) * ((g * f) . a)) + (t * ((g * f) . b)) by A2, A3, A4, Def2 ; ::_thesis: verum
end;

registration
let E be RealNormSpace;
let f, g be Affine UnOp of E;
clusterg * f ->  Affine for UnOp of E;
coherence
 for b1 being UnOp of E st b1 = g * f holds
b1 is Affine by Th15;
end;

theorem Th16: :: MAZURULM:16
for E, F being RealNormSpace
for f being Function of E,F st f is bijective & f is Affine holds
f /" is Affine
proof
let E, F be RealNormSpace; ::_thesis: for f being Function of E,F st f is bijective & f is Affine holds
f /" is Affine
let f be Function of E,F; ::_thesis: ( f is bijective & f is Affine implies f /" is Affine )
assume that
A1: f is bijective and
A2: f is Affine ; ::_thesis: f /" is Affine
set g = f /" ;
let a, b be Point of F; :: according to MAZURULM:def_2 ::_thesis: for t being real number st 0 <= t & t <= 1 holds
(f /") . (((1 - t) * a) + (t * b)) = ((1 - t) * ((f /") . a)) + (t * ((f /") . b))
let t be real number ; ::_thesis: ( 0 <= t & t <= 1 implies (f /") . (((1 - t) * a) + (t * b)) = ((1 - t) * ((f /") . a)) + (t * ((f /") . b)) )
assume A3: ( 0 <= t & t <= 1 ) ; ::_thesis: (f /") . (((1 - t) * a) + (t * b)) = ((1 - t) * ((f /") . a)) + (t * ((f /") . b))
A4: (f /") * f = id E by A1, Lm3;
 ( f . ((f /") . a) = a & f . ((f /") . b) = b ) by A1, Lm2;
hence (f /") . (((1 - t) * a) + (t * b)) = (f /") . (f . (((1 - t) * ((f /") . a)) + (t * ((f /") . b)))) by A3, A2, Def2
.= ((f /") * f) . (((1 - t) * ((f /") . a)) + (t * ((f /") . b))) by FUNCT_2:15
.= ((1 - t) * ((f /") . a)) + (t * ((f /") . b)) by A4, FUNCT_1:18 ;
::_thesis: verum
end;

registration
let E be RealNormSpace;
let f be bijective Affine UnOp of E;
clusterf /"  ->  Affine ;
coherence
 f /" is Affine by Th16;
end;

definition
let E be non empty RLSStruct ;
let a be Point of E;
funca -reflection  ->  UnOp of E means :Def4: :: MAZURULM:def 4
 for b being Point of E holds it . b = (2 * a) - b;
existence
 ex b1 being UnOp of E st
for b being Point of E holds b1 . b = (2 * a) - b
proof
deffunc H1( Point of E) ->  Element of the carrier of E = (2 * a) - $1;
 ex f being UnOp of E st
for x being Point of E holds f . x = H1(x) from FUNCT_2:sch_4();
hence  ex b1 being UnOp of E st
for b being Point of E holds b1 . b = (2 * a) - b ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being UnOp of E st ( for b being Point of E holds b1 . b = (2 * a) - b ) & ( for b being Point of E holds b2 . b = (2 * a) - b ) holds
b1 = b2
proof
let f1, f2 be UnOp of E; ::_thesis: ( ( for b being Point of E holds f1 . b = (2 * a) - b ) & ( for b being Point of E holds f2 . b = (2 * a) - b ) implies f1 = f2 )
assume that
A1: for b being Point of E holds f1 . b = (2 * a) - b and
A2: for b being Point of E holds f2 . b = (2 * a) - b ; ::_thesis: f1 = f2
let b be Point of E; :: according to FUNCT_2:def_8 ::_thesis: f1 . b = f2 . b
thus f1 . b = (2 * a) - b by A1
.= f2 . b by A2 ; ::_thesis: verum
end;
end;

:: deftheorem Def4 defines -reflection MAZURULM:def_4_:_
 for E being non empty RLSStruct
for a being Point of E
for b3 being UnOp of E holds
( b3 = a -reflection iff for b being Point of E holds b3 . b = (2 * a) - b );

theorem Th17: :: MAZURULM:17
for E being RealNormSpace
for a being Point of E holds (a -reflection) * (a -reflection) = id E
proof
let E be RealNormSpace; ::_thesis: for a being Point of E holds (a -reflection) * (a -reflection) = id E
let a be Point of E; ::_thesis: (a -reflection) * (a -reflection) = id E
set R = a -reflection ;
let b be Point of E; :: according to FUNCT_2:def_8 ::_thesis: ((a -reflection) * (a -reflection)) . b = (id E) . b
thus ((a -reflection) * (a -reflection)) . b = (a -reflection) . ((a -reflection) . b) by FUNCT_2:15
.= (2 * a) - ((a -reflection) . b) by Def4
.= (2 * a) - ((2 * a) - b) by Def4
.= ((2 * a) - (2 * a)) + b by RLVECT_1:29
.= (0. E) + b by RLVECT_1:5
.= b by RLVECT_1:4
.= (id E) . b by FUNCT_1:18 ; ::_thesis: verum
end;

registration
let E be RealNormSpace;
let a be Point of E;
clustera -reflection  ->  bijective ;
coherence
 a -reflection is bijective
proof
set R = a -reflection ;
 (a -reflection) * (a -reflection) = id E by Th17;
hence  ( a -reflection is one-to-one & a -reflection is onto ) by FUNCT_2:23; :: according to FUNCT_2:def_4 ::_thesis: verum
end;
end;

theorem Th18: :: MAZURULM:18
for E being RealNormSpace
for a being Point of E holds
( (a -reflection) . a = a & ( for b being Point of E st (a -reflection) . b = b holds
a = b ) )
proof
let E be RealNormSpace; ::_thesis: for a being Point of E holds
( (a -reflection) . a = a & ( for b being Point of E st (a -reflection) . b = b holds
a = b ) )
let a be Point of E; ::_thesis: ( (a -reflection) . a = a & ( for b being Point of E st (a -reflection) . b = b holds
a = b ) )
set R = a -reflection ;
thus (a -reflection) . a = (2 * a) - a by Def4
.= (a + a) - a by Th3
.= a + (a - a) by RLVECT_1:28
.= a + (0. E) by RLVECT_1:15
.= a by RLVECT_1:def_4 ; ::_thesis: for b being Point of E st (a -reflection) . b = b holds
a = b
let b be Point of E; ::_thesis: ( (a -reflection) . b = b implies a = b )
assume  (a -reflection) . b = b ; ::_thesis: a = b
then A1: ((a -reflection) . b) + b = 2 * b by Th3;
 (a -reflection) . b = (2 * a) - b by Def4;
then ((a -reflection) . b) + b = (2 * a) - (b - b) by RLVECT_1:29
.= (2 * a) - (0. E) by RLVECT_1:15
.= 2 * a by RLVECT_1:13 ;
hence  a = b by A1, RLVECT_1:36; ::_thesis: verum
end;

theorem Th19: :: MAZURULM:19
for E being RealNormSpace
for a, b being Point of E holds ((a -reflection) . b) - a = a - b
proof
let E be RealNormSpace; ::_thesis: for a, b being Point of E holds ((a -reflection) . b) - a = a - b
let a, b be Point of E; ::_thesis: ((a -reflection) . b) - a = a - b
set R = a -reflection ;
A1: 1 * a = a by RLVECT_1:def_8;
 (a -reflection) . b = (2 * a) - b by Def4;
hence ((a -reflection) . b) - a = ((2 * a) - a) - b by VECTSP_1:34
.= ((2 - 1) * a) - b by A1, RLVECT_1:35
.= a - b by RLVECT_1:def_8 ;
::_thesis: verum
end;

theorem Th20: :: MAZURULM:20
for E being RealNormSpace
for a, b being Point of E holds ||.(((a -reflection) . b) - a).|| = ||.(b - a).||
proof
let E be RealNormSpace; ::_thesis: for a, b being Point of E holds ||.(((a -reflection) . b) - a).|| = ||.(b - a).||
let a, b be Point of E; ::_thesis: ||.(((a -reflection) . b) - a).|| = ||.(b - a).||
 ((a -reflection) . b) - a = a - b by Th19;
hence  ||.(((a -reflection) . b) - a).|| = ||.(b - a).|| by NORMSP_1:7; ::_thesis: verum
end;

theorem Th21: :: MAZURULM:21
for E being RealNormSpace
for a, b being Point of E holds ((a -reflection) . b) - b = 2 * (a - b)
proof
let E be RealNormSpace; ::_thesis: for a, b being Point of E holds ((a -reflection) . b) - b = 2 * (a - b)
let a, b be Point of E; ::_thesis: ((a -reflection) . b) - b = 2 * (a - b)
((2 * a) - b) - b = (2 * a) - (b + b) by RLVECT_1:27
.= (2 * a) - (2 * b) by Th3
.= 2 * (a - b) by RLVECT_1:34 ;
hence  ((a -reflection) . b) - b = 2 * (a - b) by Def4; ::_thesis: verum
end;

theorem Th22: :: MAZURULM:22
for E being RealNormSpace
for a, b being Point of E holds ||.(((a -reflection) . b) - b).|| = 2 * ||.(b - a).||
proof
let E be RealNormSpace; ::_thesis: for a, b being Point of E holds ||.(((a -reflection) . b) - b).|| = 2 * ||.(b - a).||
let a, b be Point of E; ::_thesis: ||.(((a -reflection) . b) - b).|| = 2 * ||.(b - a).||
A1: ((a -reflection) . b) - b = 2 * (a - b) by Th21;
A2: abs 2 = 2 by COMPLEX1:43;
 ||.(a - b).|| = ||.(b - a).|| by NORMSP_1:7;
hence  ||.(((a -reflection) . b) - b).|| = 2 * ||.(b - a).|| by A1, A2, NORMSP_1:def_1; ::_thesis: verum
end;

theorem Th23: :: MAZURULM:23
for E being RealNormSpace
for a being Point of E holds (a -reflection) /" = a -reflection
proof
let E be RealNormSpace; ::_thesis: for a being Point of E holds (a -reflection) /" = a -reflection
let a be Point of E; ::_thesis: (a -reflection) /" = a -reflection
set R = a -reflection ;
A1: rng (a -reflection) = [#] E by FUNCT_2:def_3;
A2: (a -reflection) /" = (a -reflection) " by TOPS_2:def_4;
 (a -reflection) * (a -reflection) = id E by Th17;
hence  (a -reflection) /" = a -reflection by A1, A2, FUNCT_2:30; ::_thesis: verum
end;

registration
let E be RealNormSpace;
let a be Point of E;
clustera -reflection  ->  isometric ;
coherence
 a -reflection is isometric
proof
set R = a -reflection ;
let b be Point of E; :: according to MAZURULM:def_1 ::_thesis: for b being Point of E holds ||.(((a -reflection) . b) - ((a -reflection) . b)).|| = ||.(b - b).||
let c be Point of E; ::_thesis: ||.(((a -reflection) . b) - ((a -reflection) . c)).|| = ||.(b - c).||
 ( (a -reflection) . b = (2 * a) - b & (a -reflection) . c = (2 * a) - c ) by Def4;
then ((a -reflection) . b) - ((a -reflection) . c) = (((2 * a) - b) - (2 * a)) + c by RLVECT_1:29
.= (((2 * a) - (2 * a)) - b) + c by VECTSP_1:34
.= ((0. E) - b) + c by RLVECT_1:15
.= c - b by RLVECT_1:14 ;
hence  ||.(((a -reflection) . b) - ((a -reflection) . c)).|| = ||.(b - c).|| by NORMSP_1:7; ::_thesis: verum
end;
end;

deffunc H1( RealNormSpace, Point of $1, Point of $1) ->  set =  {  g where g is UnOp of $1 : ( g is bijective & g is isometric & g . $2 = $2 & g . $3 = $3 )  }  ;

deffunc H2( RealNormSpace, Point of $1, Point of $1) ->  set =  {  ||.((g . ((1 / 2) * ($2 + $3))) - ((1 / 2) * ($2 + $3))).|| where g is UnOp of $1 : g in H1($1,$2,$3)  }  ;

Lm4: now__::_thesis:_for_E_being_RealNormSpace
for_a,_b_being_Point_of_E
for_l_being_real-membered_set_st_l_=_H2(E,a,b)_holds_
2_*_||.(a_-_((1_/_2)_*_(a_+_b))).||_is_UpperBound_of_l
let E be RealNormSpace; ::_thesis: for a, b being Point of E
for l being real-membered set st l = H2(E,a,b) holds
2 * ||.(a - ((1 / 2) * (a + b))).|| is UpperBound of l
let a, b be Point of E; ::_thesis: for l being real-membered set st l = H2(E,a,b) holds
2 * ||.(a - ((1 / 2) * (a + b))).|| is UpperBound of l
let l be real-membered set ; ::_thesis: ( l = H2(E,a,b) implies 2 * ||.(a - ((1 / 2) * (a + b))).|| is UpperBound of l )
assume A1: l = H2(E,a,b) ; ::_thesis: 2 * ||.(a - ((1 / 2) * (a + b))).|| is UpperBound of l
set z = (1 / 2) * (a + b);
thus  2 * ||.(a - ((1 / 2) * (a + b))).|| is UpperBound of l ::_thesis: verum
proof
let x be ext-real number ; :: according to XXREAL_2:def_1 ::_thesis: ( not x in l or x <= 2 * ||.(a - ((1 / 2) * (a + b))).|| )
assume  x in l ; ::_thesis: x <= 2 * ||.(a - ((1 / 2) * (a + b))).||
then consider g1 being UnOp of E such that
A2: x = ||.((g1 . ((1 / 2) * (a + b))) - ((1 / 2) * (a + b))).|| and
A3: g1 in H1(E,a,b) by A1;
consider g being UnOp of E such that
A4: g1 = g and
 g is bijective and
A5: g is isometric and
A6: g . a = a and
 g . b = b by A3;
A7: ||.((g . ((1 / 2) * (a + b))) - a).|| = ||.(((1 / 2) * (a + b)) - a).|| by A5, A6, Def1
.= ||.(a - ((1 / 2) * (a + b))).|| by NORMSP_1:7 ;
 ||.((g . ((1 / 2) * (a + b))) - ((1 / 2) * (a + b))).|| <= ||.((g . ((1 / 2) * (a + b))) - a).|| + ||.(a - ((1 / 2) * (a + b))).|| by NORMSP_1:10;
hence  x <= 2 * ||.(a - ((1 / 2) * (a + b))).|| by A2, A4, A7; ::_thesis: verum
end;
end;

Lm5: now__::_thesis:_for_E_being_RealNormSpace
for_a,_b_being_Point_of_E
for_h_being_UnOp_of_E_st_h_in_H1(E,a,b)_holds_
(((((1_/_2)_*_(a_+_b))_-reflection)_*_(h_/"))_*_(((1_/_2)_*_(a_+_b))_-reflection))_*_h_in_H1(E,a,b)
let E be RealNormSpace; ::_thesis: for a, b being Point of E
for h being UnOp of E st h in H1(E,a,b) holds
(((((1 / 2) * (a + b)) -reflection) * (h /")) * (((1 / 2) * (a + b)) -reflection)) * h in H1(E,a,b)
let a, b be Point of E; ::_thesis: for h being UnOp of E st h in H1(E,a,b) holds
(((((1 / 2) * (a + b)) -reflection) * (h /")) * (((1 / 2) * (a + b)) -reflection)) * h in H1(E,a,b)
let h be UnOp of E; ::_thesis: ( h in H1(E,a,b) implies (((((1 / 2) * (a + b)) -reflection) * (h /")) * (((1 / 2) * (a + b)) -reflection)) * h in H1(E,a,b) )
assume A1: h in H1(E,a,b) ; ::_thesis: (((((1 / 2) * (a + b)) -reflection) * (h /")) * (((1 / 2) * (a + b)) -reflection)) * h in H1(E,a,b)
set z = (1 / 2) * (a + b);
set R = ((1 / 2) * (a + b)) -reflection ;
set gs = (((((1 / 2) * (a + b)) -reflection) * (h /")) * (((1 / 2) * (a + b)) -reflection)) * h;
consider g being UnOp of E such that
A2: g = h and
A3: g is bijective and
A4: g is isometric and
A5: g . a = a and
A6: g . b = b by A1;
A7: g /" = g " by A3, TOPS_2:def_4;
then A8: g /" is bijective by A3, GROUP_6:63;
A9: 2 * ((1 / 2) * (a + b)) = (2 * (1 / 2)) * (a + b) by RLVECT_1:def_7
.= a + b by RLVECT_1:def_8 ;
then A10: (2 * ((1 / 2) * (a + b))) - a = b by Th4;
A11: (2 * ((1 / 2) * (a + b))) - b = a by A9, Th4;
A12: dom g = [#] E by FUNCT_2:def_1;
A13: (g /") . b = b by A7, A6, A3, A12, FUNCT_1:32;
A14: (g /") . a = a by A7, A5, A3, A12, FUNCT_1:32;
A15: ((((((1 / 2) * (a + b)) -reflection) * (h /")) * (((1 / 2) * (a + b)) -reflection)) * h) . a = (((((1 / 2) * (a + b)) -reflection) * (g /")) * (((1 / 2) * (a + b)) -reflection)) . a by A5, A2, FUNCT_2:15
.= ((((1 / 2) * (a + b)) -reflection) * (g /")) . ((((1 / 2) * (a + b)) -reflection) . a) by FUNCT_2:15
.= ((((1 / 2) * (a + b)) -reflection) * (g /")) . b by A10, Def4
.= (((1 / 2) * (a + b)) -reflection) . ((g /") . b) by FUNCT_2:15
.= (2 * ((1 / 2) * (a + b))) - b by A13, Def4
.= a by A9, Th4 ;
((((((1 / 2) * (a + b)) -reflection) * (h /")) * (((1 / 2) * (a + b)) -reflection)) * h) . b = (((((1 / 2) * (a + b)) -reflection) * (g /")) * (((1 / 2) * (a + b)) -reflection)) . b by A6, A2, FUNCT_2:15
.= ((((1 / 2) * (a + b)) -reflection) * (g /")) . ((((1 / 2) * (a + b)) -reflection) . b) by FUNCT_2:15
.= ((((1 / 2) * (a + b)) -reflection) * (g /")) . a by A11, Def4
.= (((1 / 2) * (a + b)) -reflection) . ((g /") . a) by FUNCT_2:15
.= (2 * ((1 / 2) * (a + b))) - a by A14, Def4
.= b by A9, Th4 ;
hence  (((((1 / 2) * (a + b)) -reflection) * (h /")) * (((1 / 2) * (a + b)) -reflection)) * h in H1(E,a,b) by A2, A3, A4, A8, A15; ::_thesis: verum
end;

Lm6: now__::_thesis:_for_E_being_RealNormSpace
for_a,_b_being_Point_of_E
for_l_being_non_empty_bounded_above_Subset_of_REAL_st_l_=_H2(E,a,b)_holds_
sup_l_is_UpperBound_of_2_**_l
let E be RealNormSpace; ::_thesis: for a, b being Point of E
for l being non empty bounded_above Subset of REAL st l = H2(E,a,b) holds
sup l is UpperBound of 2 ** l
let a, b be Point of E; ::_thesis: for l being non empty bounded_above Subset of REAL st l = H2(E,a,b) holds
sup l is UpperBound of 2 ** l
let l be non empty bounded_above Subset of REAL; ::_thesis: ( l = H2(E,a,b) implies sup l is UpperBound of 2 ** l )
assume A1: l = H2(E,a,b) ; ::_thesis: sup l is UpperBound of 2 ** l
thus  sup l is UpperBound of 2 ** l ::_thesis: verum
proof
set z = (1 / 2) * (a + b);
set R = ((1 / 2) * (a + b)) -reflection ;
let x be ext-real number ; :: according to XXREAL_2:def_1 ::_thesis: ( not x in 2 ** l or x <= sup l )
assume  x in 2 ** l ; ::_thesis: x <= sup l
then consider w being Element of ExtREAL  such that
A2: x = 2 * w and
A3: w in l by MEMBER_1:188;
consider h being UnOp of E such that
A4: w = ||.((h . ((1 / 2) * (a + b))) - ((1 / 2) * (a + b))).|| and
A5: h in H1(E,a,b) by A3, A1;
consider g being UnOp of E such that
A6: g = h and
A7: g is bijective and
A8: g is isometric and
 ( g . a = a & g . b = b ) by A5;
A9: (((1 / 2) * (a + b)) -reflection) * ((g /") * ((((1 / 2) * (a + b)) -reflection) * g)) = ((((1 / 2) * (a + b)) -reflection) * (g /")) * ((((1 / 2) * (a + b)) -reflection) * g) by RELAT_1:36
.= (((((1 / 2) * (a + b)) -reflection) * (g /")) * (((1 / 2) * (a + b)) -reflection)) * g by RELAT_1:36 ;
A10: (((1 / 2) * (a + b)) -reflection) . ((g /") . ((((1 / 2) * (a + b)) -reflection) . (g . ((1 / 2) * (a + b))))) = (((1 / 2) * (a + b)) -reflection) . ((g /") . (((((1 / 2) * (a + b)) -reflection) * g) . ((1 / 2) * (a + b)))) by FUNCT_2:15
.= (((1 / 2) * (a + b)) -reflection) . (((g /") * ((((1 / 2) * (a + b)) -reflection) * g)) . ((1 / 2) * (a + b))) by FUNCT_2:15
.= ((((1 / 2) * (a + b)) -reflection) * ((g /") * ((((1 / 2) * (a + b)) -reflection) * g))) . ((1 / 2) * (a + b)) by FUNCT_2:15 ;
A11: g /" = g " by A7, TOPS_2:def_4;
 (((((1 / 2) * (a + b)) -reflection) * (g /")) * (((1 / 2) * (a + b)) -reflection)) * g in H1(E,a,b) by A5, A6, Lm5;
then A12: ||.((((((((1 / 2) * (a + b)) -reflection) * (g /")) * (((1 / 2) * (a + b)) -reflection)) * g) . ((1 / 2) * (a + b))) - ((1 / 2) * (a + b))).|| in l by A1;
reconsider d = 2 as R_eal by XXREAL_0:def_1;
 ||.((g . ((1 / 2) * (a + b))) - ((1 / 2) * (a + b))).|| in ExtREAL by XXREAL_0:def_1;
then A13: d * ||.((g . ((1 / 2) * (a + b))) - ((1 / 2) * (a + b))).|| = 2 * ||.((g . ((1 / 2) * (a + b))) - ((1 / 2) * (a + b))).|| by EXTREAL1:1;
A14: (g /") . (g . ((1 / 2) * (a + b))) = (1 / 2) * (a + b) by A7, A11, FUNCT_2:26;
2 * ||.((g . ((1 / 2) * (a + b))) - ((1 / 2) * (a + b))).|| = ||.(((((1 / 2) * (a + b)) -reflection) . (g . ((1 / 2) * (a + b)))) - (g . ((1 / 2) * (a + b)))).|| by Th22
.= ||.(((g /") . ((((1 / 2) * (a + b)) -reflection) . (g . ((1 / 2) * (a + b))))) - ((g /") . (g . ((1 / 2) * (a + b))))).|| by A7, A8, Def1
.= ||.(((((1 / 2) * (a + b)) -reflection) . ((g /") . ((((1 / 2) * (a + b)) -reflection) . (g . ((1 / 2) * (a + b)))))) - ((1 / 2) * (a + b))).|| by A14, Th20 ;
hence  x <= sup l by A2, A4, A9, A10, A12, A6, A13, XXREAL_2:4; ::_thesis: verum
end;
end;

Lm7: now__::_thesis:_for_E_being_RealNormSpace
for_a,_b_being_Point_of_E
for_l_being_real-membered_set_st_l_=_H2(E,a,b)_holds_
for_g_being_UnOp_of_E_st_g_in_H1(E,a,b)_holds_
g_._((1_/_2)_*_(a_+_b))_=_(1_/_2)_*_(a_+_b)
let E be RealNormSpace; ::_thesis: for a, b being Point of E
for l being real-membered set st l = H2(E,a,b) holds
for g being UnOp of E st g in H1(E,a,b) holds
g . ((1 / 2) * (a + b)) = (1 / 2) * (a + b)
let a, b be Point of E; ::_thesis: for l being real-membered set st l = H2(E,a,b) holds
for g being UnOp of E st g in H1(E,a,b) holds
g . ((1 / 2) * (a + b)) = (1 / 2) * (a + b)
let l be real-membered set ; ::_thesis: ( l = H2(E,a,b) implies for g being UnOp of E st g in H1(E,a,b) holds
g . ((1 / 2) * (a + b)) = (1 / 2) * (a + b) )
assume A1: l = H2(E,a,b) ; ::_thesis: for g being UnOp of E st g in H1(E,a,b) holds
g . ((1 / 2) * (a + b)) = (1 / 2) * (a + b)
let g be UnOp of E; ::_thesis: ( g in H1(E,a,b) implies g . ((1 / 2) * (a + b)) = (1 / 2) * (a + b) )
assume A2: g in H1(E,a,b) ; ::_thesis: g . ((1 / 2) * (a + b)) = (1 / 2) * (a + b)
set z = (1 / 2) * (a + b);
set R = ((1 / 2) * (a + b)) -reflection ;
A3: l c= REAL
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in l or x in REAL )
assume  x in l ; ::_thesis: x in REAL
then  ex g being UnOp of E st
( x = ||.((g . ((1 / 2) * (a + b))) - ((1 / 2) * (a + b))).|| & g in H1(E,a,b) ) by A1;
hence  x in REAL ; ::_thesis: verum
end;
 ( (id E) . a = a & (id E) . b = b ) by FUNCT_1:18;
then  id E in H1(E,a,b) ;
then A4: ||.(((id E) . ((1 / 2) * (a + b))) - ((1 / 2) * (a + b))).|| in l by A1;
 2 * ||.(a - ((1 / 2) * (a + b))).|| is UpperBound of l by A1, Lm4;
then reconsider A = l as non empty bounded_above Subset of REAL by A3, A4, XXREAL_2:def_10;
set lambda = sup A;
reconsider d = 2 as R_eal by XXREAL_0:def_1;
A5: d * (sup A) = sup (2 ** A) by URYSOHN2:18;
A6: ||.((g . ((1 / 2) * (a + b))) - ((1 / 2) * (a + b))).|| in A by A1, A2;
A7: d * (sup A) = 2 * (sup A) by XXREAL_3:def_5;
 sup A is UpperBound of 2 ** A by A1, Lm6;
then  sup (2 ** A) <= sup A by XXREAL_2:def_3;
then  (2 * (sup A)) - (sup A) <= (sup A) - (sup A) by A7, A5, XREAL_1:9;
then  ||.((g . ((1 / 2) * (a + b))) - ((1 / 2) * (a + b))).|| = 0 by A6, XXREAL_2:4;
hence  g . ((1 / 2) * (a + b)) = (1 / 2) * (a + b) by NORMSP_1:6; ::_thesis: verum
end;

theorem Th24: :: MAZURULM:24
for E, F being RealNormSpace
for f being Function of E,F st f is isometric holds
f is_continuous_on dom f
proof
let E, F be RealNormSpace; ::_thesis: for f being Function of E,F st f is isometric holds
f is_continuous_on dom f
let f be Function of E,F; ::_thesis: ( f is isometric implies f is_continuous_on dom f )
assume A1: f is isometric ; ::_thesis: f is_continuous_on dom f
set X = dom f;
 for s1 being sequence of E st rng s1 c= dom f & s1 is convergent & lim s1 in dom f holds
( f /* s1 is convergent & f /. (lim s1) = lim (f /* s1) )
proof
let s1 be sequence of E; ::_thesis: ( rng s1 c= dom f & s1 is convergent & lim s1 in dom f implies ( f /* s1 is convergent & f /. (lim s1) = lim (f /* s1) ) )
assume that
A2: rng s1 c= dom f and
A3: s1 is convergent and
 lim s1 in dom f ; ::_thesis: ( f /* s1 is convergent & f /. (lim s1) = lim (f /* s1) )
consider a being Point of E such that
A4: for r being Real st 0 < r holds
ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.((s1 . n) - a).|| < r by A3, NORMSP_1:def_6;
A5: a = lim s1 by A3, A4, NORMSP_1:def_7;
A6: for r being Real st 0 < r holds
ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.(((f /* s1) . n) - (f . a)).|| < r
proof
let r be Real; ::_thesis: ( 0 < r implies ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.(((f /* s1) . n) - (f . a)).|| < r )
assume  0 < r ; ::_thesis: ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.(((f /* s1) . n) - (f . a)).|| < r
then consider m being Element of NAT  such that
A7: for n being Element of NAT st m <= n holds
||.((s1 . n) - a).|| < r by A4;
take  m ; ::_thesis: for n being Element of NAT st m <= n holds
||.(((f /* s1) . n) - (f . a)).|| < r
let n be Element of NAT ; ::_thesis: ( m <= n implies ||.(((f /* s1) . n) - (f . a)).|| < r )
assume  m <= n ; ::_thesis: ||.(((f /* s1) . n) - (f . a)).|| < r
then A8: ||.((s1 . n) - a).|| < r by A7;
A9: ||.((f . (s1 . n)) - (f . a)).|| = ||.((s1 . n) - a).|| by A1, Def1;
 f /* s1 = f * s1 by A2, FUNCT_2:def_11;
hence  ||.(((f /* s1) . n) - (f . a)).|| < r by A8, A9, FUNCT_2:15; ::_thesis: verum
end;
thus  f /* s1 is convergent ::_thesis: f /. (lim s1) = lim (f /* s1)
proof
take  f . a ; :: according to NORMSP_1:def_6 ::_thesis: for b1 being Element of REAL holds
( b1 <= 0 or ex b2 being Element of NAT st
for b3 being Element of NAT holds
( not b2 <= b3 or not b1 <= ||.(((f /* s1) . b3) - (f . a)).|| ) )
thus  for b1 being Element of REAL holds
( b1 <= 0 or ex b2 being Element of NAT st
for b3 being Element of NAT holds
( not b2 <= b3 or not b1 <= ||.(((f /* s1) . b3) - (f . a)).|| ) ) by A6; ::_thesis: verum
end;
hence  f /. (lim s1) = lim (f /* s1) by A5, A6, NORMSP_1:def_7; ::_thesis: verum
end;
hence  f is_continuous_on dom f by NFCONT_1:18; ::_thesis: verum
end;

Lm8:  for E being RealNormSpace
for a, b being Point of E
for t being real number holds ((1 - t) * a) + (t * b) = a + (t * (b - a))
proof
let E be RealNormSpace; ::_thesis: for a, b being Point of E
for t being real number holds ((1 - t) * a) + (t * b) = a + (t * (b - a))
let a, b be Point of E; ::_thesis: for t being real number holds ((1 - t) * a) + (t * b) = a + (t * (b - a))
let t be real number ; ::_thesis: ((1 - t) * a) + (t * b) = a + (t * (b - a))
thus ((1 - t) * a) + (t * b) = ((1 * a) - (t * a)) + (t * b) by RLVECT_1:35
.= (a - (t * a)) + (t * b) by RLVECT_1:def_8
.= (a + (t * b)) - (t * a) by RLVECT_1:def_3
.= a + ((t * b) - (t * a)) by RLVECT_1:28
.= a + (t * (b - a)) by RLVECT_1:34 ; ::_thesis: verum
end;

Lm9: now__::_thesis:_for_E,_F_being_RealNormSpace
for_f_being_Function_of_E,F
for_a,_b_being_Point_of_E
for_n,_j_being_Nat_st_f_is_midpoints-preserving_&_j_<=_2_|^_n_holds_
ex_x_being_Nat_st_
(_x_=_(2_|^_n)_-_j_&_f_._(a_+_((j_/_(2_|^_(n_+_1)))_*_(b_-_a)))_=_(1_/_2)_*_((f_._a)_+_(f_._((1_/_(2_|^_n))_*_((x_*_a)_+_(j_*_b)))))_)
let E, F be RealNormSpace; ::_thesis: for f being Function of E,F
for a, b being Point of E
for n, j being Nat st f is midpoints-preserving & j <= 2 |^ n holds
ex x being Nat st
( x = (2 |^ n) - j & f . (a + ((j / (2 |^ (n + 1))) * (b - a))) = (1 / 2) * ((f . a) + (f . ((1 / (2 |^ n)) * ((x * a) + (j * b))))) )
let f be Function of E,F; ::_thesis: for a, b being Point of E
for n, j being Nat st f is midpoints-preserving & j <= 2 |^ n holds
ex x being Nat st
( x = (2 |^ n) - j & f . (a + ((j / (2 |^ (n + 1))) * (b - a))) = (1 / 2) * ((f . a) + (f . ((1 / (2 |^ n)) * ((x * a) + (j * b))))) )
let a, b be Point of E; ::_thesis: for n, j being Nat st f is midpoints-preserving & j <= 2 |^ n holds
ex x being Nat st
( x = (2 |^ n) - j & f . (a + ((j / (2 |^ (n + 1))) * (b - a))) = (1 / 2) * ((f . a) + (f . ((1 / (2 |^ n)) * ((x * a) + (j * b))))) )
let n, j be Nat; ::_thesis: ( f is midpoints-preserving & j <= 2 |^ n implies ex x being Nat st
( x = (2 |^ n) - j & f . (a + ((j / (2 |^ (n + 1))) * (b - a))) = (1 / 2) * ((f . a) + (f . ((1 / (2 |^ n)) * ((x * a) + (j * b))))) ) )
set m = 2 |^ (n + 1);
set k = 2 |^ n;
set x = (2 |^ n) - j;
assume A1: f is midpoints-preserving ; ::_thesis: ( j <= 2 |^ n implies ex x being Nat st
( x = (2 |^ n) - j & f . (a + ((j / (2 |^ (n + 1))) * (b - a))) = (1 / 2) * ((f . a) + (f . ((1 / (2 |^ n)) * ((x * a) + (j * b))))) ) )
assume  j <= 2 |^ n ; ::_thesis: ex x being Nat st
( x = (2 |^ n) - j & f . (a + ((j / (2 |^ (n + 1))) * (b - a))) = (1 / 2) * ((f . a) + (f . ((1 / (2 |^ n)) * ((x * a) + (j * b))))) )
then  (2 |^ n) - j in NAT by INT_1:5;
then reconsider x = (2 |^ n) - j as Nat ;
take x = x; ::_thesis: ( x = (2 |^ n) - j & f . (a + ((j / (2 |^ (n + 1))) * (b - a))) = (1 / 2) * ((f . a) + (f . ((1 / (2 |^ n)) * ((x * a) + (j * b))))) )
thus  x = (2 |^ n) - j ; ::_thesis: f . (a + ((j / (2 |^ (n + 1))) * (b - a))) = (1 / 2) * ((f . a) + (f . ((1 / (2 |^ n)) * ((x * a) + (j * b)))))
set z = (1 - (j / (2 |^ (n + 1)))) - (1 / 2);
A2: 2 |^ n <> 0 by NEWTON:83;
A3: 2 * (2 |^ n) = 2 |^ (n + 1) by NEWTON:6;
A4: (1 / 2) * (1 / (2 |^ n)) = 1 / (2 * (2 |^ n)) by XCMPLX_1:102;
x / (2 |^ (n + 1)) = ((1 * (2 |^ n)) / (2 |^ (n + 1))) - (j / (2 |^ (n + 1)))
.= (1 / 2) - (j / (2 |^ (n + 1))) by A2, A3, XCMPLX_1:91
.= (1 - (j / (2 |^ (n + 1)))) - (1 / 2) ;
then A5: (((1 - (j / (2 |^ (n + 1)))) - (1 / 2)) * a) + ((j / (2 |^ (n + 1))) * b) = ((1 / (2 |^ (n + 1))) * (x * a)) + (((1 / (2 |^ (n + 1))) * j) * b) by RLVECT_1:def_7
.= ((1 / (2 |^ (n + 1))) * (x * a)) + ((1 / (2 |^ (n + 1))) * (j * b)) by RLVECT_1:def_7
.= (1 / (2 |^ (n + 1))) * ((x * a) + (j * b)) by RLVECT_1:def_5
.= (1 / 2) * ((1 / (2 |^ n)) * ((x * a) + (j * b))) by A4, A3, RLVECT_1:def_7 ;
a + ((j / (2 |^ (n + 1))) * (b - a)) = a + (((j / (2 |^ (n + 1))) * b) - ((j / (2 |^ (n + 1))) * a)) by RLVECT_1:34
.= (a + ((j / (2 |^ (n + 1))) * b)) - ((j / (2 |^ (n + 1))) * a) by RLVECT_1:def_3
.= (a - ((j / (2 |^ (n + 1))) * a)) + ((j / (2 |^ (n + 1))) * b) by RLVECT_1:def_3
.= ((1 * a) - ((j / (2 |^ (n + 1))) * a)) + ((j / (2 |^ (n + 1))) * b) by RLVECT_1:def_8
.= ((1 - (j / (2 |^ (n + 1)))) * a) + ((j / (2 |^ (n + 1))) * b) by RLVECT_1:35
.= ((((1 - (j / (2 |^ (n + 1)))) * a) + (((1 - (j / (2 |^ (n + 1)))) - (1 / 2)) * a)) - (((1 - (j / (2 |^ (n + 1)))) - (1 / 2)) * a)) + ((j / (2 |^ (n + 1))) * b) by Th4
.= ((((1 - (j / (2 |^ (n + 1)))) * a) - (((1 - (j / (2 |^ (n + 1)))) - (1 / 2)) * a)) + (((1 - (j / (2 |^ (n + 1)))) - (1 / 2)) * a)) + ((j / (2 |^ (n + 1))) * b) by RLVECT_1:def_3
.= ((((1 - (j / (2 |^ (n + 1)))) - ((1 - (j / (2 |^ (n + 1)))) - (1 / 2))) * a) + (((1 - (j / (2 |^ (n + 1)))) - (1 / 2)) * a)) + ((j / (2 |^ (n + 1))) * b) by RLVECT_1:35
.= ((1 / 2) * a) + ((((1 - (j / (2 |^ (n + 1)))) - (1 / 2)) * a) + ((j / (2 |^ (n + 1))) * b)) by RLVECT_1:def_3
.= (1 / 2) * (a + ((1 / (2 |^ n)) * ((x * a) + (j * b)))) by A5, RLVECT_1:def_5 ;
hence  f . (a + ((j / (2 |^ (n + 1))) * (b - a))) = (1 / 2) * ((f . a) + (f . ((1 / (2 |^ n)) * ((x * a) + (j * b))))) by A1, Def3; ::_thesis: verum
end;

Lm10: now__::_thesis:_for_E,_F_being_RealNormSpace
for_f_being_Function_of_E,F
for_a,_b_being_Point_of_E
for_n,_j_being_Nat_st_f_is_midpoints-preserving_&_j_>=_2_|^_n_holds_
ex_x_being_Nat_st_
(_x_=_((2_|^_n)_+_j)_-_(2_|^_(n_+_1))_&_f_._(a_+_((j_/_(2_|^_(n_+_1)))_*_(b_-_a)))_=_(1_/_2)_*_((f_._b)_+_(f_._((1_/_(2_|^_n))_*_((((2_|^_(n_+_1))_-_j)_*_a)_+_(x_*_b)))))_)
let E, F be RealNormSpace; ::_thesis: for f being Function of E,F
for a, b being Point of E
for n, j being Nat st f is midpoints-preserving & j >= 2 |^ n holds
ex x being Nat st
( x = ((2 |^ n) + j) - (2 |^ (n + 1)) & f . (a + ((j / (2 |^ (n + 1))) * (b - a))) = (1 / 2) * ((f . b) + (f . ((1 / (2 |^ n)) * ((((2 |^ (n + 1)) - j) * a) + (x * b))))) )
let f be Function of E,F; ::_thesis: for a, b being Point of E
for n, j being Nat st f is midpoints-preserving & j >= 2 |^ n holds
ex x being Nat st
( x = ((2 |^ n) + j) - (2 |^ (n + 1)) & f . (a + ((j / (2 |^ (n + 1))) * (b - a))) = (1 / 2) * ((f . b) + (f . ((1 / (2 |^ n)) * ((((2 |^ (n + 1)) - j) * a) + (x * b))))) )
let a, b be Point of E; ::_thesis: for n, j being Nat st f is midpoints-preserving & j >= 2 |^ n holds
ex x being Nat st
( x = ((2 |^ n) + j) - (2 |^ (n + 1)) & f . (a + ((j / (2 |^ (n + 1))) * (b - a))) = (1 / 2) * ((f . b) + (f . ((1 / (2 |^ n)) * ((((2 |^ (n + 1)) - j) * a) + (x * b))))) )
let n, j be Nat; ::_thesis: ( f is midpoints-preserving & j >= 2 |^ n implies ex x being Nat st
( x = ((2 |^ n) + j) - (2 |^ (n + 1)) & f . (a + ((j / (2 |^ (n + 1))) * (b - a))) = (1 / 2) * ((f . b) + (f . ((1 / (2 |^ n)) * ((((2 |^ (n + 1)) - j) * a) + (x * b))))) ) )
set m = 2 |^ (n + 1);
set k = 2 |^ n;
set x = ((2 |^ n) + j) - (2 |^ (n + 1));
assume A1: f is midpoints-preserving ; ::_thesis: ( j >= 2 |^ n implies ex x being Nat st
( x = ((2 |^ n) + j) - (2 |^ (n + 1)) & f . (a + ((j / (2 |^ (n + 1))) * (b - a))) = (1 / 2) * ((f . b) + (f . ((1 / (2 |^ n)) * ((((2 |^ (n + 1)) - j) * a) + (x * b))))) ) )
A2: 2 * (2 |^ n) = 2 |^ (n + 1) by NEWTON:6;
assume  j >= 2 |^ n ; ::_thesis: ex x being Nat st
( x = ((2 |^ n) + j) - (2 |^ (n + 1)) & f . (a + ((j / (2 |^ (n + 1))) * (b - a))) = (1 / 2) * ((f . b) + (f . ((1 / (2 |^ n)) * ((((2 |^ (n + 1)) - j) * a) + (x * b))))) )
then  (2 |^ n) + (2 |^ n) <= (2 |^ n) + j by XREAL_1:6;
then  ((2 |^ n) + j) - (2 |^ (n + 1)) in NAT by A2, INT_1:5;
then reconsider x = ((2 |^ n) + j) - (2 |^ (n + 1)) as Nat ;
take x = x; ::_thesis: ( x = ((2 |^ n) + j) - (2 |^ (n + 1)) & f . (a + ((j / (2 |^ (n + 1))) * (b - a))) = (1 / 2) * ((f . b) + (f . ((1 / (2 |^ n)) * ((((2 |^ (n + 1)) - j) * a) + (x * b))))) )
thus  x = ((2 |^ n) + j) - (2 |^ (n + 1)) ; ::_thesis: f . (a + ((j / (2 |^ (n + 1))) * (b - a))) = (1 / 2) * ((f . b) + (f . ((1 / (2 |^ n)) * ((((2 |^ (n + 1)) - j) * a) + (x * b)))))
set z = (j / (2 |^ (n + 1))) - (1 / 2);
A3: 2 |^ n <> 0 by NEWTON:83;
A4: 2 |^ (n + 1) <> 0 by NEWTON:83;
A5: (2 |^ (n + 1)) / (2 |^ (n + 1)) = 1 by A4, XCMPLX_1:60;
then A6: 1 - (j / (2 |^ (n + 1))) = (1 / (2 |^ (n + 1))) * ((2 |^ (n + 1)) - j) ;
A7: (2 |^ n) / (2 |^ (n + 1)) = (1 * (2 |^ n)) / (2 * (2 |^ n)) by NEWTON:6
.= 1 / 2 by A3, XCMPLX_1:91 ;
A8: (1 / 2) * (1 / (2 |^ n)) = 1 / (2 * (2 |^ n)) by XCMPLX_1:102;
x / (2 |^ (n + 1)) = (((2 |^ n) + j) / (2 |^ (n + 1))) - ((2 |^ (n + 1)) / (2 |^ (n + 1)))
.= (j / (2 |^ (n + 1))) - (1 / 2) by A5, A7 ;
then A9: (((j / (2 |^ (n + 1))) - (1 / 2)) * b) + ((1 - (j / (2 |^ (n + 1)))) * a) = ((1 / (2 |^ (n + 1))) * (((2 |^ (n + 1)) - j) * a)) + (((1 / (2 |^ (n + 1))) * x) * b) by A6, RLVECT_1:def_7
.= ((1 / (2 |^ (n + 1))) * (((2 |^ (n + 1)) - j) * a)) + ((1 / (2 |^ (n + 1))) * (x * b)) by RLVECT_1:def_7
.= (1 / (2 |^ (n + 1))) * ((((2 |^ (n + 1)) - j) * a) + (x * b)) by RLVECT_1:def_5
.= (1 / 2) * ((1 / (2 |^ n)) * ((((2 |^ (n + 1)) - j) * a) + (x * b))) by A8, A2, RLVECT_1:def_7 ;
a + ((j / (2 |^ (n + 1))) * (b - a)) = a + (((j / (2 |^ (n + 1))) * b) - ((j / (2 |^ (n + 1))) * a)) by RLVECT_1:34
.= (a + ((j / (2 |^ (n + 1))) * b)) - ((j / (2 |^ (n + 1))) * a) by RLVECT_1:def_3
.= (a - ((j / (2 |^ (n + 1))) * a)) + ((j / (2 |^ (n + 1))) * b) by RLVECT_1:def_3
.= ((1 * a) - ((j / (2 |^ (n + 1))) * a)) + ((j / (2 |^ (n + 1))) * b) by RLVECT_1:def_8
.= ((1 - (j / (2 |^ (n + 1)))) * a) + ((j / (2 |^ (n + 1))) * b) by RLVECT_1:35
.= ((((j / (2 |^ (n + 1))) * b) + (((j / (2 |^ (n + 1))) - (1 / 2)) * b)) - (((j / (2 |^ (n + 1))) - (1 / 2)) * b)) + ((1 - (j / (2 |^ (n + 1)))) * a) by Th4
.= ((((j / (2 |^ (n + 1))) * b) - (((j / (2 |^ (n + 1))) - (1 / 2)) * b)) + (((j / (2 |^ (n + 1))) - (1 / 2)) * b)) + ((1 - (j / (2 |^ (n + 1)))) * a) by RLVECT_1:def_3
.= ((((j / (2 |^ (n + 1))) - ((j / (2 |^ (n + 1))) - (1 / 2))) * b) + (((j / (2 |^ (n + 1))) - (1 / 2)) * b)) + ((1 - (j / (2 |^ (n + 1)))) * a) by RLVECT_1:35
.= ((1 / 2) * b) + ((((j / (2 |^ (n + 1))) - (1 / 2)) * b) + ((1 - (j / (2 |^ (n + 1)))) * a)) by RLVECT_1:def_3
.= (1 / 2) * (b + ((1 / (2 |^ n)) * ((((2 |^ (n + 1)) - j) * a) + (x * b)))) by A9, RLVECT_1:def_5 ;
hence  f . (a + ((j / (2 |^ (n + 1))) * (b - a))) = (1 / 2) * ((f . b) + (f . ((1 / (2 |^ n)) * ((((2 |^ (n + 1)) - j) * a) + (x * b))))) by A1, Def3; ::_thesis: verum
end;

Lm11: now__::_thesis:_for_E,_F_being_RealNormSpace
for_f_being_Function_of_E,F
for_a,_b_being_Point_of_E
for_t_being_Nat_st_f_is_midpoints-preserving_holds_
for_n_being_Nat_st_t_<=_2_|^_n_holds_
f_._(((1_-_(t_/_(2_|^_n)))_*_a)_+_((t_/_(2_|^_n))_*_b))_=_((1_-_(t_/_(2_|^_n)))_*_(f_._a))_+_((t_/_(2_|^_n))_*_(f_._b))
let E, F be RealNormSpace; ::_thesis: for f being Function of E,F
for a, b being Point of E
for t being Nat st f is midpoints-preserving holds
for n being Nat st t <= 2 |^ n holds
f . (((1 - (t / (2 |^ n))) * a) + ((t / (2 |^ n)) * b)) = ((1 - (t / (2 |^ n))) * (f . a)) + ((t / (2 |^ n)) * (f . b))
let f be Function of E,F; ::_thesis: for a, b being Point of E
for t being Nat st f is midpoints-preserving holds
for n being Nat st t <= 2 |^ n holds
f . (((1 - (t / (2 |^ n))) * a) + ((t / (2 |^ n)) * b)) = ((1 - (t / (2 |^ n))) * (f . a)) + ((t / (2 |^ n)) * (f . b))
let a, b be Point of E; ::_thesis: for t being Nat st f is midpoints-preserving holds
for n being Nat st t <= 2 |^ n holds
f . (((1 - (t / (2 |^ n))) * a) + ((t / (2 |^ n)) * b)) = ((1 - (t / (2 |^ n))) * (f . a)) + ((t / (2 |^ n)) * (f . b))
let t be Nat; ::_thesis: ( f is midpoints-preserving implies for n being Nat st t <= 2 |^ n holds
f . (((1 - (t / (2 |^ n))) * a) + ((t / (2 |^ n)) * b)) = ((1 - (t / (2 |^ n))) * (f . a)) + ((t / (2 |^ n)) * (f . b)) )
assume A1: f is midpoints-preserving ; ::_thesis: for n being Nat st t <= 2 |^ n holds
f . (((1 - (t / (2 |^ n))) * a) + ((t / (2 |^ n)) * b)) = ((1 - (t / (2 |^ n))) * (f . a)) + ((t / (2 |^ n)) * (f . b))
thus  for n being Nat st t <= 2 |^ n holds
f . (((1 - (t / (2 |^ n))) * a) + ((t / (2 |^ n)) * b)) = ((1 - (t / (2 |^ n))) * (f . a)) + ((t / (2 |^ n)) * (f . b)) ::_thesis: verum
proof
defpred S1[ Nat] means  for w being Nat st w <= 2 |^ $1 holds
f . (((1 - (w / (2 |^ $1))) * a) + ((w / (2 |^ $1)) * b)) = ((1 - (w / (2 |^ $1))) * (f . a)) + ((w / (2 |^ $1)) * (f . b));
A2: S1[ 0 ]
proof
let t be Nat; ::_thesis: ( t <= 2 |^ 0 implies f . (((1 - (t / (2 |^ 0))) * a) + ((t / (2 |^ 0)) * b)) = ((1 - (t / (2 |^ 0))) * (f . a)) + ((t / (2 |^ 0)) * (f . b)) )
assume A3: t <= 2 |^ 0 ; ::_thesis: f . (((1 - (t / (2 |^ 0))) * a) + ((t / (2 |^ 0)) * b)) = ((1 - (t / (2 |^ 0))) * (f . a)) + ((t / (2 |^ 0)) * (f . b))
A4: 2 |^ 0 = 1 by NEWTON:4;
percases ( t = 1 or t = 0 ) by A3, A4, NAT_1:25;
supposeA5: t = 1 ; ::_thesis: f . (((1 - (t / (2 |^ 0))) * a) + ((t / (2 |^ 0)) * b)) = ((1 - (t / (2 |^ 0))) * (f . a)) + ((t / (2 |^ 0)) * (f . b))
then f . (((1 - t) * a) + (t * b)) = f . ((0. E) + (t * b)) by RLVECT_1:10
.= f . (t * b) by RLVECT_1:4
.= f . b by A5, RLVECT_1:def_8
.= t * (f . b) by A5, RLVECT_1:def_8
.= (0. F) + (t * (f . b)) by RLVECT_1:4
.= ((1 - t) * (f . a)) + (t * (f . b)) by A5, RLVECT_1:10 ;
hence  f . (((1 - (t / (2 |^ 0))) * a) + ((t / (2 |^ 0)) * b)) = ((1 - (t / (2 |^ 0))) * (f . a)) + ((t / (2 |^ 0)) * (f . b)) by A4; ::_thesis: verum
end;
supposeA6: t = 0 ; ::_thesis: f . (((1 - (t / (2 |^ 0))) * a) + ((t / (2 |^ 0)) * b)) = ((1 - (t / (2 |^ 0))) * (f . a)) + ((t / (2 |^ 0)) * (f . b))
then f . (((1 - t) * a) + (t * b)) = f . ((1 * a) + (0. E)) by RLVECT_1:10
.= f . (1 * a) by RLVECT_1:4
.= f . a by RLVECT_1:def_8
.= (1 - t) * (f . a) by A6, RLVECT_1:def_8
.= ((1 - t) * (f . a)) + (0. F) by RLVECT_1:4
.= ((1 - t) * (f . a)) + (t * (f . b)) by A6, RLVECT_1:10 ;
hence  f . (((1 - (t / (2 |^ 0))) * a) + ((t / (2 |^ 0)) * b)) = ((1 - (t / (2 |^ 0))) * (f . a)) + ((t / (2 |^ 0)) * (f . b)) by A4; ::_thesis: verum
end;
end;
end;
A7: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] )
set m = 2 |^ n;
set k = 2 |^ (n + 1);
assume A8: S1[n] ; ::_thesis: S1[n + 1]
let t be Nat; ::_thesis: ( t <= 2 |^ (n + 1) implies f . (((1 - (t / (2 |^ (n + 1)))) * a) + ((t / (2 |^ (n + 1))) * b)) = ((1 - (t / (2 |^ (n + 1)))) * (f . a)) + ((t / (2 |^ (n + 1))) * (f . b)) )
assume A9: t <= 2 |^ (n + 1) ; ::_thesis: f . (((1 - (t / (2 |^ (n + 1)))) * a) + ((t / (2 |^ (n + 1))) * b)) = ((1 - (t / (2 |^ (n + 1)))) * (f . a)) + ((t / (2 |^ (n + 1))) * (f . b))
A10: 2 |^ (n + 1) = (2 |^ n) * 2 by NEWTON:6;
A11: 2 |^ n <> 0 by NEWTON:83;
A12: (1 / 2) * (t / (2 |^ n)) = (1 * t) / (2 * (2 |^ n)) by XCMPLX_1:76
.= t / (2 |^ (n + 1)) by NEWTON:6 ;
percases ( t <= 2 |^ n or t >= 2 |^ n ) ;
supposeA13: t <= 2 |^ n ; ::_thesis: f . (((1 - (t / (2 |^ (n + 1)))) * a) + ((t / (2 |^ (n + 1))) * b)) = ((1 - (t / (2 |^ (n + 1)))) * (f . a)) + ((t / (2 |^ (n + 1))) * (f . b))
then consider x being Nat such that
A14: x = (2 |^ n) - t and
A15: f . (a + ((t / (2 |^ (n + 1))) * (b - a))) = (1 / 2) * ((f . a) + (f . ((1 / (2 |^ n)) * ((x * a) + (t * b))))) by A1, Lm9;
A16: x / (2 |^ n) = ((2 |^ n) / (2 |^ n)) - (t / (2 |^ n)) by A14
.= 1 - (t / (2 |^ n)) by A11, XCMPLX_1:60 ;
A17: (1 / (2 |^ n)) * ((x * a) + (t * b)) = ((1 / (2 |^ n)) * (x * a)) + ((1 / (2 |^ n)) * (t * b)) by RLVECT_1:def_5
.= ((1 / (2 |^ n)) * (x * a)) + ((t / (2 |^ n)) * b) by RLVECT_1:def_7
.= ((x / (2 |^ n)) * a) + ((t / (2 |^ n)) * b) by RLVECT_1:def_7 ;
thus f . (((1 - (t / (2 |^ (n + 1)))) * a) + ((t / (2 |^ (n + 1))) * b)) = f . (a + ((t / (2 |^ (n + 1))) * (b - a))) by Lm8
.= ((1 / 2) * (f . a)) + ((1 / 2) * (f . ((1 / (2 |^ n)) * ((x * a) + (t * b))))) by A15, RLVECT_1:def_5
.= ((1 / 2) * (f . a)) + ((1 / 2) * (((1 - (t / (2 |^ n))) * (f . a)) + ((t / (2 |^ n)) * (f . b)))) by A16, A13, A17, A8
.= ((1 / 2) * (f . a)) + (((1 / 2) * ((1 - (t / (2 |^ n))) * (f . a))) + ((1 / 2) * ((t / (2 |^ n)) * (f . b)))) by RLVECT_1:def_5
.= (((1 / 2) * (f . a)) + ((1 / 2) * ((1 - (t / (2 |^ n))) * (f . a)))) + ((1 / 2) * ((t / (2 |^ n)) * (f . b))) by RLVECT_1:def_3
.= (((1 / 2) * (f . a)) + (((1 / 2) * (1 - (t / (2 |^ n)))) * (f . a))) + ((1 / 2) * ((t / (2 |^ n)) * (f . b))) by RLVECT_1:def_7
.= (((1 / 2) + ((1 / 2) * (1 - (t / (2 |^ n))))) * (f . a)) + ((1 / 2) * ((t / (2 |^ n)) * (f . b))) by RLVECT_1:def_6
.= ((1 - (t / (2 |^ (n + 1)))) * (f . a)) + ((t / (2 |^ (n + 1))) * (f . b)) by A12, RLVECT_1:def_7 ; ::_thesis: verum
end;
suppose t >= 2 |^ n ; ::_thesis: f . (((1 - (t / (2 |^ (n + 1)))) * a) + ((t / (2 |^ (n + 1))) * b)) = ((1 - (t / (2 |^ (n + 1)))) * (f . a)) + ((t / (2 |^ (n + 1))) * (f . b))
then consider x being Nat such that
A18: x = ((2 |^ n) + t) - (2 |^ (n + 1)) and
A19: f . (a + ((t / (2 |^ (n + 1))) * (b - a))) = (1 / 2) * ((f . b) + (f . ((1 / (2 |^ n)) * ((((2 |^ (n + 1)) - t) * a) + (x * b))))) by A1, Lm10;
set w = t - (2 |^ n);
A20: t - (2 |^ n) <= (2 * (2 |^ n)) - (2 |^ n) by A9, A10, XREAL_1:9;
A21: (2 |^ n) / (2 |^ n) = 1 by A11, XCMPLX_1:60;
A22: (2 |^ (n + 1)) / (2 |^ n) = (2 * (2 |^ n)) / (1 * (2 |^ n)) by NEWTON:6
.= 2 / 1 by A11, XCMPLX_1:91 ;
A23: (1 / 2) * (1 - ((t - (2 |^ n)) / (2 |^ n))) = 1 - ((1 / 2) * (t / (2 |^ n))) by A21
.= 1 - ((1 * t) / (2 * (2 |^ n))) by XCMPLX_1:76
.= 1 - (t / (2 |^ (n + 1))) by NEWTON:6 ;
thus f . (((1 - (t / (2 |^ (n + 1)))) * a) + ((t / (2 |^ (n + 1))) * b)) = f . (a + ((t / (2 |^ (n + 1))) * (b - a))) by Lm8
.= ((1 / 2) * (f . b)) + ((1 / 2) * (f . ((1 / (2 |^ n)) * ((((2 |^ (n + 1)) - t) * a) + (x * b))))) by A19, RLVECT_1:def_5
.= ((1 / 2) * (f . b)) + ((1 / 2) * (f . (((1 / (2 |^ n)) * (((2 |^ (n + 1)) - t) * a)) + ((1 / (2 |^ n)) * (x * b))))) by RLVECT_1:def_5
.= ((1 / 2) * (f . b)) + ((1 / 2) * (f . ((((1 / (2 |^ n)) * ((2 |^ (n + 1)) - t)) * a) + ((1 / (2 |^ n)) * (x * b))))) by RLVECT_1:def_7
.= ((1 / 2) * (f . b)) + ((1 / 2) * (f . ((((1 / (2 |^ n)) * ((2 |^ (n + 1)) - t)) * a) + (((1 / (2 |^ n)) * x) * b)))) by RLVECT_1:def_7
.= ((1 / 2) * (f . b)) + ((1 / 2) * (((1 - ((t - (2 |^ n)) / (2 |^ n))) * (f . a)) + (((t - (2 |^ n)) / (2 |^ n)) * (f . b)))) by A20, A21, A22, A18, A10, A8
.= ((1 / 2) * (f . b)) + (((1 / 2) * ((1 - ((t - (2 |^ n)) / (2 |^ n))) * (f . a))) + ((1 / 2) * (((t - (2 |^ n)) / (2 |^ n)) * (f . b)))) by RLVECT_1:def_5
.= ((1 / 2) * ((1 - ((t - (2 |^ n)) / (2 |^ n))) * (f . a))) + (((1 / 2) * (f . b)) + ((1 / 2) * (((t - (2 |^ n)) / (2 |^ n)) * (f . b)))) by RLVECT_1:def_3
.= ((1 / 2) * ((1 - ((t - (2 |^ n)) / (2 |^ n))) * (f . a))) + ((1 / 2) * ((f . b) + (((t - (2 |^ n)) / (2 |^ n)) * (f . b)))) by RLVECT_1:def_5
.= ((1 / 2) * ((1 - ((t - (2 |^ n)) / (2 |^ n))) * (f . a))) + ((1 / 2) * ((1 * (f . b)) + (((t - (2 |^ n)) / (2 |^ n)) * (f . b)))) by RLVECT_1:def_8
.= ((1 / 2) * ((1 - ((t - (2 |^ n)) / (2 |^ n))) * (f . a))) + ((1 / 2) * ((1 + ((t - (2 |^ n)) / (2 |^ n))) * (f . b))) by RLVECT_1:def_6
.= ((1 / 2) * ((1 - ((t - (2 |^ n)) / (2 |^ n))) * (f . a))) + (((1 / 2) * (1 + ((t - (2 |^ n)) / (2 |^ n)))) * (f . b)) by RLVECT_1:def_7
.= ((1 - (t / (2 |^ (n + 1)))) * (f . a)) + ((t / (2 |^ (n + 1))) * (f . b)) by A23, RLVECT_1:def_7 ; ::_thesis: verum
end;
end;
end;
 for n being Nat holds S1[n] from NAT_1:sch_2(A2, A7);
hence  for n being Nat st t <= 2 |^ n holds
f . (((1 - (t / (2 |^ n))) * a) + ((t / (2 |^ n)) * b)) = ((1 - (t / (2 |^ n))) * (f . a)) + ((t / (2 |^ n)) * (f . b)) ; ::_thesis: verum
end;
end;

registration
let E, F be RealNormSpace;
cluster Function-like quasi_total bijective isometric  ->  midpoints-preserving for Element of K10(K11( the carrier of E, the carrier of F));
coherence
 for b1 being Function of E,F st b1 is bijective & b1 is isometric holds
b1 is midpoints-preserving
proof
let f be Function of E,F; ::_thesis: ( f is bijective & f is isometric implies f is midpoints-preserving )
assume that
A1: f is bijective and
A2: f is isometric ; ::_thesis: f is midpoints-preserving
let a, b be Point of E; :: according to MAZURULM:def_3 ::_thesis: f . ((1 / 2) * (a + b)) = (1 / 2) * ((f . a) + (f . b))
set W = H1(E,a,b);
set l = H2(E,a,b);
set z = (1 / 2) * (a + b);
set z1 = (1 / 2) * ((f . a) + (f . b));
set R = ((1 / 2) * (a + b)) -reflection ;
set R1 = ((1 / 2) * ((f . a) + (f . b))) -reflection ;
set h = (((((1 / 2) * (a + b)) -reflection) * (f /")) * (((1 / 2) * ((f . a) + (f . b))) -reflection)) * f;
now__::_thesis:_for_x_being_set_st_x_in_H2(E,a,b)_holds_
x_is_real
let x be set ; ::_thesis: ( x in H2(E,a,b) implies x is real )
assume  x in H2(E,a,b) ; ::_thesis: x is real
then  ex g being UnOp of E st
( x = ||.((g . ((1 / 2) * (a + b))) - ((1 / 2) * (a + b))).|| & g in H1(E,a,b) ) ;
hence  x is real ; ::_thesis: verum
end;
then reconsider l = H2(E,a,b) as real-membered set by MEMBERED:def_3;
A3: rng f = [#] F by A1, FUNCT_2:def_3;
A4: f /" = f " by A1, TOPS_2:def_4;
then A5: f /" is bijective by A1, GROUP_6:63;
 (((1 / 2) * (a + b)) -reflection) * (f /") is onto by A5, FUNCT_2:27;
then  ((((1 / 2) * (a + b)) -reflection) * (f /")) * (((1 / 2) * ((f . a) + (f . b))) -reflection) is onto by FUNCT_2:27;
then A6: (((((1 / 2) * (a + b)) -reflection) * (f /")) * (((1 / 2) * ((f . a) + (f . b))) -reflection)) * f is onto by A1, FUNCT_2:27;
 f /" is isometric by A1, A2, Th12;
then  (((1 / 2) * (a + b)) -reflection) * (f /") is isometric by Th11;
then  ((((1 / 2) * (a + b)) -reflection) * (f /")) * (((1 / 2) * ((f . a) + (f . b))) -reflection) is isometric by Th11;
then A7: (((((1 / 2) * (a + b)) -reflection) * (f /")) * (((1 / 2) * ((f . a) + (f . b))) -reflection)) * f is isometric by A2, Th11;
A8: 2 * ((1 / 2) * (a + b)) = (2 * (1 / 2)) * (a + b) by RLVECT_1:def_7
.= a + b by RLVECT_1:def_8 ;
then A9: (2 * ((1 / 2) * (a + b))) - a = b by Th4;
A10: (2 * ((1 / 2) * (a + b))) - b = a by A8, Th4;
A11: 2 * ((1 / 2) * ((f . a) + (f . b))) = (2 * (1 / 2)) * ((f . a) + (f . b)) by RLVECT_1:def_7
.= (f . a) + (f . b) by RLVECT_1:def_8 ;
then A12: (2 * ((1 / 2) * ((f . a) + (f . b)))) - (f . a) = f . b by Th4;
A13: (2 * ((1 / 2) * ((f . a) + (f . b)))) - (f . b) = f . a by A11, Th4;
A14: ((((((1 / 2) * (a + b)) -reflection) * (f /")) * (((1 / 2) * ((f . a) + (f . b))) -reflection)) * f) . a = (((((1 / 2) * (a + b)) -reflection) * (f /")) * (((1 / 2) * ((f . a) + (f . b))) -reflection)) . (f . a) by FUNCT_2:15
.= ((((1 / 2) * (a + b)) -reflection) * (f /")) . ((((1 / 2) * ((f . a) + (f . b))) -reflection) . (f . a)) by FUNCT_2:15
.= ((((1 / 2) * (a + b)) -reflection) * (f /")) . (f . b) by A12, Def4
.= (((1 / 2) * (a + b)) -reflection) . ((f /") . (f . b)) by FUNCT_2:15
.= (((1 / 2) * (a + b)) -reflection) . b by A4, A1, FUNCT_2:26
.= a by A10, Def4 ;
((((((1 / 2) * (a + b)) -reflection) * (f /")) * (((1 / 2) * ((f . a) + (f . b))) -reflection)) * f) . b = (((((1 / 2) * (a + b)) -reflection) * (f /")) * (((1 / 2) * ((f . a) + (f . b))) -reflection)) . (f . b) by FUNCT_2:15
.= ((((1 / 2) * (a + b)) -reflection) * (f /")) . ((((1 / 2) * ((f . a) + (f . b))) -reflection) . (f . b)) by FUNCT_2:15
.= ((((1 / 2) * (a + b)) -reflection) * (f /")) . (f . a) by A13, Def4
.= (((1 / 2) * (a + b)) -reflection) . ((f /") . (f . a)) by FUNCT_2:15
.= (((1 / 2) * (a + b)) -reflection) . a by A4, A1, FUNCT_2:26
.= b by A9, Def4 ;
then A15: (((((1 / 2) * (a + b)) -reflection) * (f /")) * (((1 / 2) * ((f . a) + (f . b))) -reflection)) * f in H1(E,a,b) by A4, A1, A6, A7, A14;
 rng (((1 / 2) * (a + b)) -reflection) = [#] E by FUNCT_2:def_3;
then A16: ((((1 / 2) * (a + b)) -reflection) /") * (((1 / 2) * (a + b)) -reflection) = id (dom (((1 / 2) * (a + b)) -reflection)) by TOPS_2:52
.= id E by FUNCT_2:def_1 ;
A17: f * (f /") = id F by A1, A3, TOPS_2:52;
A18: ((((1 / 2) * (a + b)) -reflection) /") * ((((((1 / 2) * (a + b)) -reflection) * (f /")) * (((1 / 2) * ((f . a) + (f . b))) -reflection)) * f) = ((((1 / 2) * (a + b)) -reflection) /") * (((((1 / 2) * (a + b)) -reflection) * (f /")) * ((((1 / 2) * ((f . a) + (f . b))) -reflection) * f)) by RELAT_1:36
.= ((((1 / 2) * (a + b)) -reflection) /") * ((((1 / 2) * (a + b)) -reflection) * ((f /") * ((((1 / 2) * ((f . a) + (f . b))) -reflection) * f))) by RELAT_1:36
.= (((((1 / 2) * (a + b)) -reflection) /") * (((1 / 2) * (a + b)) -reflection)) * ((f /") * ((((1 / 2) * ((f . a) + (f . b))) -reflection) * f)) by RELAT_1:36
.= ((((((1 / 2) * (a + b)) -reflection) /") * (((1 / 2) * (a + b)) -reflection)) * (f /")) * ((((1 / 2) * ((f . a) + (f . b))) -reflection) * f) by RELAT_1:36
.= (((((((1 / 2) * (a + b)) -reflection) /") * (((1 / 2) * (a + b)) -reflection)) * (f /")) * (((1 / 2) * ((f . a) + (f . b))) -reflection)) * f by RELAT_1:36
.= ((f /") * (((1 / 2) * ((f . a) + (f . b))) -reflection)) * f by A16, FUNCT_2:17 ;
A19: f * (((f /") * (((1 / 2) * ((f . a) + (f . b))) -reflection)) * f) = f * ((f /") * ((((1 / 2) * ((f . a) + (f . b))) -reflection) * f)) by RELAT_1:36
.= (f * (f /")) * ((((1 / 2) * ((f . a) + (f . b))) -reflection) * f) by RELAT_1:36
.= (((1 / 2) * ((f . a) + (f . b))) -reflection) * f by A17, FUNCT_2:17 ;
 l = H2(E,a,b) ;
then  ((((((1 / 2) * (a + b)) -reflection) * (f /")) * (((1 / 2) * ((f . a) + (f . b))) -reflection)) * f) . ((1 / 2) * (a + b)) = (1 / 2) * (a + b) by A15, Lm7;
then  (((((1 / 2) * (a + b)) -reflection) /") * ((((((1 / 2) * (a + b)) -reflection) * (f /")) * (((1 / 2) * ((f . a) + (f . b))) -reflection)) * f)) . ((1 / 2) * (a + b)) = ((((1 / 2) * (a + b)) -reflection) /") . ((1 / 2) * (a + b)) by FUNCT_2:15;
then A20: (f * (((f /") * (((1 / 2) * ((f . a) + (f . b))) -reflection)) * f)) . ((1 / 2) * (a + b)) = f . (((((1 / 2) * (a + b)) -reflection) /") . ((1 / 2) * (a + b))) by A18, FUNCT_2:15
.= (f * ((((1 / 2) * (a + b)) -reflection) /")) . ((1 / 2) * (a + b)) by FUNCT_2:15 ;
(((1 / 2) * ((f . a) + (f . b))) -reflection) . (f . ((1 / 2) * (a + b))) = ((((1 / 2) * ((f . a) + (f . b))) -reflection) * f) . ((1 / 2) * (a + b)) by FUNCT_2:15
.= (f * (((1 / 2) * (a + b)) -reflection)) . ((1 / 2) * (a + b)) by A20, A19, Th23
.= f . ((((1 / 2) * (a + b)) -reflection) . ((1 / 2) * (a + b))) by FUNCT_2:15
.= f . ((1 / 2) * (a + b)) by Th18 ;
hence  f . ((1 / 2) * (a + b)) = (1 / 2) * ((f . a) + (f . b)) by Th18; ::_thesis: verum
end;
end;

registration
let E, F be RealNormSpace;
cluster Function-like quasi_total isometric midpoints-preserving  ->  Affine for Element of K10(K11( the carrier of E, the carrier of F));
coherence
 for b1 being Function of E,F st b1 is isometric & b1 is midpoints-preserving holds
b1 is Affine
proof
let f be Function of E,F; ::_thesis: ( f is isometric & f is midpoints-preserving implies f is Affine )
assume that
A1: f is isometric and
A2: f is midpoints-preserving ; ::_thesis: f is Affine
let a be Point of E; :: according to MAZURULM:def_2 ::_thesis: for b being Point of E
for t being real number 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; ::_thesis: for t being real number st 0 <= t & t <= 1 holds
f . (((1 - t) * a) + (t * b)) = ((1 - t) * (f . a)) + (t * (f . b))
let t be real number ; ::_thesis: ( 0 <= t & t <= 1 implies f . (((1 - t) * a) + (t * b)) = ((1 - t) * (f . a)) + (t * (f . b)) )
assume  ( 0 <= t & t <= 1 ) ; ::_thesis: 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, SEQ_2:9;
then 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 - t by A5, A11, A8, Th7;
 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, A8, 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))
proof
let n be Element of NAT ; :: according to FUNCT_2:def_8 ::_thesis: (f /* (((1 + (- s)) * a) + (s * b))) . n = (((1 + (- s)) * (f . a)) + (s * (f . b))) . n
A17: (1 + (- s)) . n = 1 + ((- s) . n) by VALUED_1:2
.= 1 + (- (s . n)) by VALUED_1:8 ;
 dom s = NAT by FUNCT_2:def_1;
then  s . n in rng s by FUNCT_1:3;
then consider m being Element of NAT  such that
A18: s . n in dyadic m by A3, URYSOHN1:def_2;
A19: ex i being Element of NAT st
( i <= 2 |^ m & s . n = i / (2 |^ m) ) by A18, URYSOHN1:def_1;
 rng (((1 + (- s)) * a) + (s * b)) c= dom f by A6;
hence (f /* (((1 + (- s)) * a) + (s * b))) . n = f . ((((1 + (- s)) * a) + (s * b)) . n) by FUNCT_2:108
.= f . ((((1 + (- s)) * a) . n) + ((s * b) . n)) by NORMSP_1:def_2
.= f . (((1 - (s . n)) * a) + ((s * b) . n)) by A17, NDIFF_1:def_3
.= f . (((1 - (s . n)) * a) + ((s . n) * b)) by NDIFF_1:def_3
.= ((1 - (s . n)) * (f . a)) + ((s . n) * (f . b)) by A2, A19, Lm11
.= (((1 + (- s)) . n) * (f . a)) + ((s * (f . b)) . n) by A17, NDIFF_1:def_3
.= (((1 + (- s)) * (f . a)) . n) + ((s * (f . b)) . n) by NDIFF_1:def_3
.= (((1 + (- s)) * (f . a)) + (s * (f . b))) . n by NORMSP_1:def_2 ;
::_thesis: verum
end;
A20: 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, A20, A9, A13, NFCONT_1:18
.= ((1 - t) * (f . a)) + (t * (f . b)) by A14, A15, A8, A4, A16, NORMSP_1:25 ; ::_thesis: verum
end;
end;