:: by Agata Darmochwa{\l} and Yatsuka Nakamura

::

:: Received November 21, 1991

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

theorem Th1: :: HEINE:1

for x, y being Real

for A being SubSpace of RealSpace

for p, q being Point of A st x = p & y = q holds

dist (p,q) = |.(x - y).|

for A being SubSpace of RealSpace

for p, q being Point of A st x = p & y = q holds

dist (p,q) = |.(x - y).|

proof end;

definition

let seq be Real_Sequence;

let k be Nat;

ex b_{1} being Real_Sequence st

for n being Nat holds b_{1} . n = k to_power (seq . n)

for b_{1}, b_{2} being Real_Sequence st ( for n being Nat holds b_{1} . n = k to_power (seq . n) ) & ( for n being Nat holds b_{2} . n = k to_power (seq . n) ) holds

b_{1} = b_{2}

end;
let k be Nat;

func k to_power seq -> Real_Sequence means :Def1: :: HEINE:def 1

for n being Nat holds it . n = k to_power (seq . n);

existence for n being Nat holds it . n = k to_power (seq . n);

ex b

for n being Nat holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def1 defines to_power HEINE:def 1 :

for seq being Real_Sequence

for k being Nat

for b_{3} being Real_Sequence holds

( b_{3} = k to_power seq iff for n being Nat holds b_{3} . n = k to_power (seq . n) );

for seq being Real_Sequence

for k being Nat

for b

( b

:: Heine-Borel Theorem for intervals