:: by Artur Korni{\l}owicz

::

:: Received December 21, 2010

:: Copyright (c) 2010-2021 Association of Mizar Users

registration

coherence

for b_{1} being SubSpace of R^1 st b_{1} = I[01] holds

b_{1} is closed
by TOPMETR:20, TREAL_1:2;

end;
for b

b

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

Lm1: Cl D = [#] I[01]

proof end;

registration

let A be real-membered bounded_above set ;

let r be non negative Real;

coherence

r ** A is bounded_above

end;
let r be non negative Real;

coherence

r ** A is bounded_above

proof end;

registration

let A be real-membered bounded_above set ;

let r be non positive Real;

coherence

r ** A is bounded_below

end;
let r be non positive Real;

coherence

r ** A is bounded_below

proof end;

registration

let A be real-membered bounded_below set ;

let r be non negative Real;

coherence

r ** A is bounded_below

end;
let r be non negative Real;

coherence

r ** A is bounded_below

proof end;

registration

let A be non empty real-membered bounded_below set ;

let r be non positive Real;

coherence

r ** A is bounded_above

end;
let r be non positive Real;

coherence

r ** A is bounded_above

proof end;

registration

let f be convergent Real_Sequence;

let t be Real;

coherence

for b_{1} being Real_Sequence st b_{1} = t + f holds

b_{1} is convergent

end;
let t be Real;

coherence

for b

b

proof 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

for a being Point of E

for f being Real_Sequence holds f (#) (NAT --> a) = f * a

proof 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

for a being Point of E

for f being convergent Real_Sequence holds lim (f * a) = (lim f) * a

proof end;

registration

let f be convergent Real_Sequence;

let E be RealNormSpace;

let a be Point of E;

coherence

f * a is convergent

end;
let E be RealNormSpace;

let a be Point of E;

coherence

f * a is convergent

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

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;

end;
let f be Function of E,F;

:: deftheorem 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 st 0 <= t & t <= 1 holds

f . (((1 - t) * a) + (t * b)) = ((1 - t) * (f . a)) + (t * (f . b)) );

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 st 0 <= t & t <= 1 holds

f . (((1 - t) * a) + (t * b)) = ((1 - t) * (f . a)) + (t * (f . b)) );

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

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

registration
end;

registration

let E be non empty NORMSTR ;

ex b_{1} being UnOp of E st

( b_{1} is bijective & b_{1} is isometric & b_{1} is midpoints-preserving & b_{1} is Affine )

end;
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 b

( b

proof 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

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

registration

let E be RealNormSpace;

let f, g be isometric UnOp of E;

coherence

for b_{1} being UnOp of E st b_{1} = g * f holds

b_{1} is isometric
by Th11;

end;
let f, g be isometric UnOp of E;

coherence

for b

b

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

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

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

for f being Function of E,F st f is bijective & f is isometric holds

f /" is isometric

proof end;

registration
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

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

registration

let E be RealNormSpace;

let f, g be midpoints-preserving UnOp of E;

coherence

for b_{1} being UnOp of E st b_{1} = g * f holds

b_{1} is midpoints-preserving
by Th13;

end;
let f, g be midpoints-preserving UnOp of E;

coherence

for b

b

Lm3: now :: thesis: for E, F being RealNormSpace

for f being Function of E,F st f is bijective holds

(f /") * f = id E

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

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

for f being Function of E,F st f is bijective & f is midpoints-preserving holds

f /" is midpoints-preserving

proof end;

registration

let E be RealNormSpace;

let f be bijective midpoints-preserving UnOp of E;

coherence

f /" is midpoints-preserving by Th14;

end;
let f be bijective midpoints-preserving UnOp of E;

coherence

f /" is midpoints-preserving by Th14;

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

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

registration

let E be RealNormSpace;

let f, g be Affine UnOp of E;

coherence

for b_{1} being UnOp of E st b_{1} = g * f holds

b_{1} is Affine
by Th15;

end;
let f, g be Affine UnOp of E;

coherence

for b

b

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

for f being Function of E,F st f is bijective & f is Affine holds

f /" is Affine

proof end;

registration
end;

definition

let E be non empty RLSStruct ;

let a be Point of E;

ex b_{1} being UnOp of E st

for b being Point of E holds b_{1} . b = (2 * a) - b

for b_{1}, b_{2} being UnOp of E st ( for b being Point of E holds b_{1} . b = (2 * a) - b ) & ( for b being Point of E holds b_{2} . b = (2 * a) - b ) holds

b_{1} = b_{2}

end;
let a be Point of E;

func a -reflection -> UnOp of E means :Def4: :: MAZURULM:def 4

for b being Point of E holds it . b = (2 * a) - b;

existence for b being Point of E holds it . b = (2 * a) - b;

ex b

for b being Point of E holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def4 defines -reflection MAZURULM:def 4 :

for E being non empty RLSStruct

for a being Point of E

for b_{3} being UnOp of E holds

( b_{3} = a -reflection iff for b being Point of E holds b_{3} . b = (2 * a) - b );

for E being non empty RLSStruct

for a being Point of E

for b

( b

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

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

theorem Th20: :: MAZURULM:20

for E being RealNormSpace

for a, b being Point of E holds ||.(((a -reflection) . b) - a).|| = ||.(b - a).||

for a, b being Point of E holds ||.(((a -reflection) . b) - a).|| = ||.(b - a).||

proof end;

theorem Th22: :: MAZURULM:22

for E being RealNormSpace

for a, b being Point of E holds ||.(((a -reflection) . b) - b).|| = 2 * ||.(b - a).||

for a, b being Point of E holds ||.(((a -reflection) . b) - b).|| = 2 * ||.(b - a).||

proof end;

registration
end;

deffunc H

deffunc H

Lm4: now :: thesis: for E being RealNormSpace

for a, b being Point of E

for l being real-membered set st l = H_{2}(E,a,b) holds

2 * ||.(a - ((1 / 2) * (a + b))).|| is UpperBound of l

for a, b being Point of E

for l being real-membered set st l = H

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 = H_{2}(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 = H_{2}(E,a,b) holds

2 * ||.(a - ((1 / 2) * (a + b))).|| is UpperBound of l

let l be real-membered set ; :: thesis: ( l = H_{2}(E,a,b) implies 2 * ||.(a - ((1 / 2) * (a + b))).|| is UpperBound of l )

assume A1: l = H_{2}(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

end;
for l being real-membered set st l = H

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 = H

2 * ||.(a - ((1 / 2) * (a + b))).|| is UpperBound of l

let l be real-membered set ; :: thesis: ( l = H

assume A1: l = H

set z = (1 / 2) * (a + b);

thus 2 * ||.(a - ((1 / 2) * (a + b))).|| is UpperBound of l :: thesis: verum

proof

let x be ExtReal; :: 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 H_{1}(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

.= ||.(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;
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 H

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

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

Lm5: now :: thesis: for E being RealNormSpace

for a, b being Point of E

for h being UnOp of E st h in H_{1}(E,a,b) holds

(((((1 / 2) * (a + b)) -reflection) * (h /")) * (((1 / 2) * (a + b)) -reflection)) * h in H_{1}(E,a,b)

for a, b being Point of E

for h being UnOp of E st h in H

(((((1 / 2) * (a + b)) -reflection) * (h /")) * (((1 / 2) * (a + b)) -reflection)) * h in H

let E be RealNormSpace; :: thesis: for a, b being Point of E

for h being UnOp of E st h in H_{1}(E,a,b) holds

(((((1 / 2) * (a + b)) -reflection) * (h /")) * (((1 / 2) * (a + b)) -reflection)) * h in H_{1}(E,a,b)

let a, b be Point of E; :: thesis: for h being UnOp of E st h in H_{1}(E,a,b) holds

(((((1 / 2) * (a + b)) -reflection) * (h /")) * (((1 / 2) * (a + b)) -reflection)) * h in H_{1}(E,a,b)

let h be UnOp of E; :: thesis: ( h in H_{1}(E,a,b) implies (((((1 / 2) * (a + b)) -reflection) * (h /")) * (((1 / 2) * (a + b)) -reflection)) * h in H_{1}(E,a,b) )

assume A1: h in H_{1}(E,a,b)
; :: thesis: (((((1 / 2) * (a + b)) -reflection) * (h /")) * (((1 / 2) * (a + b)) -reflection)) * h in H_{1}(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 H_{1}(E,a,b)
by A2, A3, A4, A8, A15; :: thesis: verum

end;
for h being UnOp of E st h in H

(((((1 / 2) * (a + b)) -reflection) * (h /")) * (((1 / 2) * (a + b)) -reflection)) * h in H

let a, b be Point of E; :: thesis: for h being UnOp of E st h in H

(((((1 / 2) * (a + b)) -reflection) * (h /")) * (((1 / 2) * (a + b)) -reflection)) * h in H

let h be UnOp of E; :: thesis: ( h in H

assume A1: h in H

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 H

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 = H_{2}(E,a,b) holds

sup l is UpperBound of 2 ** l

for a, b being Point of E

for l being non empty bounded_above Subset of REAL st l = H

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 = H_{2}(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 = H_{2}(E,a,b) holds

sup l is UpperBound of 2 ** l

let l be non empty bounded_above Subset of REAL; :: thesis: ( l = H_{2}(E,a,b) implies sup l is UpperBound of 2 ** l )

assume A1: l = H_{2}(E,a,b)
; :: thesis: sup l is UpperBound of 2 ** l

thus sup l is UpperBound of 2 ** l :: thesis: verum

end;
for l being non empty bounded_above Subset of REAL st l = H

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 = H

sup l is UpperBound of 2 ** l

let l be non empty bounded_above Subset of REAL; :: thesis: ( l = H

assume A1: l = H

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 ExtReal; :: 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 H_{1}(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 H_{1}(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;

A13: (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 A13, Th20 ;

hence x <= sup l by A2, A4, A9, A10, A12, A6, XXREAL_2:4; :: thesis: verum

end;
set R = ((1 / 2) * (a + b)) -reflection ;

let x be ExtReal; :: 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 H

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 H

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;

A13: (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 A13, Th20 ;

hence x <= sup l by A2, A4, A9, A10, A12, A6, XXREAL_2:4; :: thesis: verum

Lm7: now :: thesis: for E being RealNormSpace

for a, b being Point of E

for l being real-membered set st l = H_{2}(E,a,b) holds

for g being UnOp of E st g in H_{1}(E,a,b) holds

g . ((1 / 2) * (a + b)) = (1 / 2) * (a + b)

for a, b being Point of E

for l being real-membered set st l = H

for g being UnOp of E st g in H

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 = H_{2}(E,a,b) holds

for g being UnOp of E st g in H_{1}(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 = H_{2}(E,a,b) holds

for g being UnOp of E st g in H_{1}(E,a,b) holds

g . ((1 / 2) * (a + b)) = (1 / 2) * (a + b)

let l be real-membered set ; :: thesis: ( l = H_{2}(E,a,b) implies for g being UnOp of E st g in H_{1}(E,a,b) holds

g . ((1 / 2) * (a + b)) = (1 / 2) * (a + b) )

assume A1: l = H_{2}(E,a,b)
; :: thesis: for g being UnOp of E st g in H_{1}(E,a,b) holds

g . ((1 / 2) * (a + b)) = (1 / 2) * (a + b)

let g be UnOp of E; :: thesis: ( g in H_{1}(E,a,b) implies g . ((1 / 2) * (a + b)) = (1 / 2) * (a + b) )

assume A2: g in H_{1}(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 by XREAL_0:def 1;

( (id E) . a = a & (id E) . b = b ) ;

then id E in H_{1}(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;

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 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;
for l being real-membered set st l = H

for g being UnOp of E st g in H

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 = H

for g being UnOp of E st g in H

g . ((1 / 2) * (a + b)) = (1 / 2) * (a + b)

let l be real-membered set ; :: thesis: ( l = H

g . ((1 / 2) * (a + b)) = (1 / 2) * (a + b) )

assume A1: l = H

g . ((1 / 2) * (a + b)) = (1 / 2) * (a + b)

let g be UnOp of E; :: thesis: ( g in H

assume A2: g in H

set z = (1 / 2) * (a + b);

set R = ((1 / 2) * (a + b)) -reflection ;

A3: l c= REAL by XREAL_0:def 1;

( (id E) . a = a & (id E) . b = b ) ;

then id E in H

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;

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

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

for f being Function of E,F st f is isometric holds

f is_continuous_on dom f

proof end;

Lm8: for E being RealNormSpace

for a, b being Point of E

for t being Real holds ((1 - t) * a) + (t * b) = a + (t * (b - a))

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

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; :: thesis: verum

end;
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; :: thesis: verum

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

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))) = ((2 |^ (n + 1)) / (2 |^ (n + 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)))

.= (((2 |^ n) / (2 |^ (n + 1))) + (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; :: thesis: verum

end;
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))) = ((2 |^ (n + 1)) / (2 |^ (n + 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)))

.= (((2 |^ n) / (2 |^ (n + 1))) + (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; :: thesis: verum

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

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

end;
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 S_{1}[ 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: S_{1}[ 0 ]
_{1}[n] holds

S_{1}[n + 1]
_{1}[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;
f . (((1 - (w / (2 |^ $1))) * a) + ((w / (2 |^ $1)) * b)) = ((1 - (w / (2 |^ $1))) * (f . a)) + ((w / (2 |^ $1)) * (f . b));

A2: S

proof

A7:
for n being Nat st S
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;

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

per cases
( t = 1 or t = 0 )
by A3, A4, NAT_1:25;

end;

suppose A5:
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)

.= f . b by A5, RLVECT_1:def 8

.= t * (f . b) by A5, RLVECT_1:def 8

.= (0. F) + (t * (f . b))

.= ((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;
.= f . (t * b)

.= f . b by A5, RLVECT_1:def 8

.= t * (f . b) by A5, RLVECT_1:def 8

.= (0. F) + (t * (f . b))

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

suppose A6:
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)

.= f . a by RLVECT_1:def 8

.= (1 - t) * (f . a) by A6, RLVECT_1:def 8

.= ((1 - t) * (f . a)) + (0. F)

.= ((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;
.= f . (1 * a)

.= f . a by RLVECT_1:def 8

.= (1 - t) * (f . a) by A6, RLVECT_1:def 8

.= ((1 - t) * (f . a)) + (0. F)

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

S

proof

for n being Nat holds S
let n be Nat; :: thesis: ( S_{1}[n] implies S_{1}[n + 1] )

set m = 2 |^ n;

set k = 2 |^ (n + 1);

assume A8: S_{1}[n]
; :: thesis: S_{1}[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 ;

end;
set m = 2 |^ n;

set k = 2 |^ (n + 1);

assume A8: S

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 ;

per cases
( t <= 2 |^ n or t >= 2 |^ n )
;

end;

suppose A13:
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;
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

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 - (t / (2 |^ n)) = ((2 |^ n) / (2 |^ n)) - (t / (2 |^ n)) by A21

.= - ((t / (2 |^ n)) - ((2 |^ n) / (2 |^ n)))

.= - ((t - (2 |^ n)) / (2 |^ n)) ;

A24: (1 / (2 |^ n)) * ((2 |^ (n + 1)) - t) = ((2 |^ (n + 1)) / (2 |^ n)) - (t / (2 |^ n))

.= (1 + 1) - (t / (2 |^ n)) by A22

.= 1 - ((t - (2 |^ n)) / (2 |^ n)) by A23

.= 1 - ((t - (2 |^ n)) / (2 |^ n)) ;

(1 / (2 |^ n)) * x = (t - (2 |^ n)) / (2 |^ n) by A18, A10;

then (((1 / (2 |^ n)) * ((2 |^ (n + 1)) - t)) * a) + (((1 / (2 |^ n)) * x) * b) = ((1 - ((t - (2 |^ n)) / (2 |^ n))) * a) + (((t - (2 |^ n)) / (2 |^ n)) * b) by A24;

then A25: (1 / 2) * (f . ((((1 / (2 |^ n)) * ((2 |^ (n + 1)) - t)) * a) + (((1 / (2 |^ n)) * x) * b))) = (1 / 2) * (((1 - ((t - (2 |^ n)) / (2 |^ n))) * (f . a)) + (((t - (2 |^ n)) / (2 |^ n)) * (f . b))) by A20, A18, A10, A8;

A26: (1 / 2) * (1 - ((t - (2 |^ n)) / (2 |^ n))) = (1 / 2) * (1 - ((t / (2 |^ n)) - ((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 A25

.= ((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 A26, RLVECT_1:def 7 ; :: thesis: verum

end;
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 - (t / (2 |^ n)) = ((2 |^ n) / (2 |^ n)) - (t / (2 |^ n)) by A21

.= - ((t / (2 |^ n)) - ((2 |^ n) / (2 |^ n)))

.= - ((t - (2 |^ n)) / (2 |^ n)) ;

A24: (1 / (2 |^ n)) * ((2 |^ (n + 1)) - t) = ((2 |^ (n + 1)) / (2 |^ n)) - (t / (2 |^ n))

.= (1 + 1) - (t / (2 |^ n)) by A22

.= 1 - ((t - (2 |^ n)) / (2 |^ n)) by A23

.= 1 - ((t - (2 |^ n)) / (2 |^ n)) ;

(1 / (2 |^ n)) * x = (t - (2 |^ n)) / (2 |^ n) by A18, A10;

then (((1 / (2 |^ n)) * ((2 |^ (n + 1)) - t)) * a) + (((1 / (2 |^ n)) * x) * b) = ((1 - ((t - (2 |^ n)) / (2 |^ n))) * a) + (((t - (2 |^ n)) / (2 |^ n)) * b) by A24;

then A25: (1 / 2) * (f . ((((1 / (2 |^ n)) * ((2 |^ (n + 1)) - t)) * a) + (((1 / (2 |^ n)) * x) * b))) = (1 / 2) * (((1 - ((t - (2 |^ n)) / (2 |^ n))) * (f . a)) + (((t - (2 |^ n)) / (2 |^ n)) * (f . b))) by A20, A18, A10, A8;

A26: (1 / 2) * (1 - ((t - (2 |^ n)) / (2 |^ n))) = (1 / 2) * (1 - ((t / (2 |^ n)) - ((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 A25

.= ((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 A26, RLVECT_1:def 7 ; :: thesis: verum

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

registration

let E, F be RealNormSpace;

for b_{1} being Function of E,F st b_{1} is bijective & b_{1} is isometric holds

b_{1} is midpoints-preserving

end;
cluster Function-like quasi_total bijective isometric -> midpoints-preserving for Element of K10(K11( the carrier of E, the carrier of F));

coherence for b

b

proof end;

registration

let E, F be RealNormSpace;

for b_{1} being Function of E,F st b_{1} is isometric & b_{1} is midpoints-preserving holds

b_{1} is Affine

end;
cluster Function-like quasi_total isometric midpoints-preserving -> Affine for Element of K10(K11( the carrier of E, the carrier of F));

coherence for b

b

proof end;