JORDAN2B

:: JORDAN2B semantic presentation

begin

registration

let n be ( ( natural ) ( natural V11() real ext-real ) Nat) ;

cluster -> REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) -valued for ( ( ) ( ) Element of the carrier of (TOP-REAL n : ( ( ) ( ) MetrStruct ) ) : ( ( V190() ) ( V190() ) L15()) : ( ( ) ( ) set ) ) ;

end;

theorem :: JORDAN2B:1

for i being ( ( ) ( natural V11() real ext-real V51() V129() V130() V131() V132() V133() V134() V135() ) Element of NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) )
for n being ( ( natural ) ( natural V11() real ext-real ) Nat) ex f being ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of (TOP-REAL b₂ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) : ( ( V190() ) ( non empty TopSpace-like V153() V178() V179() V180() V181() V182() V183() V184() V190() V219() V220() ) L15()) : ( ( ) ( non empty ) set ) -defined the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V118() ) TopStruct ) : ( ( ) ( non empty V130() V131() V132() ) set ) -valued Function-like total quasi_total complex-yielding V120() V121() ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty V130() V131() V132() ) set ) ) st
for p being ( ( ) ( Relation-like NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) -valued Function-like V35() V42(b₂ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-yielding V120() V121() ) Element of ( ( ) ( non empty ) set ) ) holds f : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of (TOP-REAL b₂ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) : ( ( V190() ) ( non empty TopSpace-like V153() V178() V179() V180() V181() V182() V183() V184() V190() V219() V220() ) L15()) : ( ( ) ( non empty ) set ) -defined the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V118() ) TopStruct ) : ( ( ) ( non empty V130() V131() V132() ) set ) -valued Function-like total quasi_total complex-yielding V120() V121() ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty V130() V131() V132() ) set ) ) . p : ( ( ) ( Relation-like NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) -valued Function-like V35() V42(b₂ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-yielding V120() V121() ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( V11() real ext-real ) Element of the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V118() ) TopStruct ) : ( ( ) ( non empty V130() V131() V132() ) set ) ) = p : ( ( ) ( Relation-like NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) -valued Function-like V35() V42(b₂ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-yielding V120() V121() ) Element of ( ( ) ( non empty ) set ) ) /. i : ( ( ) ( natural V11() real ext-real V51() V129() V130() V131() V132() V133() V134() V135() ) Element of NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) ;

theorem :: JORDAN2B:2

for n, i being ( ( ) ( natural V11() real ext-real V51() V129() V130() V131() V132() V133() V134() V135() ) Element of NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) ) st i : ( ( ) ( natural V11() real ext-real V51() V129() V130() V131() V132() V133() V134() V135() ) Element of NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) ) in Seg n : ( ( ) ( natural V11() real ext-real V51() V129() V130() V131() V132() V133() V134() V135() ) Element of NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V35() V42(b₁ : ( ( ) ( natural V11() real ext-real V51() V129() V130() V131() V132() V133() V134() V135() ) Element of NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) ) ) V130() V131() V132() V133() V134() V135() ) Element of K6(NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) holds
(0. (TOP-REAL n : ( ( ) ( natural V11() real ext-real V51() V129() V130() V131() V132() V133() V134() V135() ) Element of NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V190() ) ( non empty TopSpace-like V153() V178() V179() V180() V181() V182() V183() V184() V190() V219() V220() ) L15()) ) : ( ( ) ( Relation-like NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) -valued Function-like V35() V42(b₁ : ( ( ) ( natural V11() real ext-real V51() V129() V130() V131() V132() V133() V134() V135() ) Element of NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like V62( TOP-REAL b₁ : ( ( ) ( natural V11() real ext-real V51() V129() V130() V131() V132() V133() V134() V135() ) Element of NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V190() ) ( non empty TopSpace-like V153() V178() V179() V180() V181() V182() V183() V184() V190() V219() V220() ) L15()) ) complex-yielding V120() V121() ) Element of the carrier of (TOP-REAL b₁ : ( ( ) ( natural V11() real ext-real V51() V129() V130() V131() V132() V133() V134() V135() ) Element of NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V190() ) ( non empty TopSpace-like V153() V178() V179() V180() V181() V182() V183() V184() V190() V219() V220() ) L15()) : ( ( ) ( non empty ) set ) ) /. i : ( ( ) ( natural V11() real ext-real V51() V129() V130() V131() V132() V133() V134() V135() ) Element of NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) = 0 : ( ( ) ( empty natural V11() real ext-real non positive non negative functional FinSequence-membered V51() V129() V130() V131() V132() V133() V134() V135() V136() ) Element of NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) ) ;

theorem :: JORDAN2B:3

theorem :: JORDAN2B:4

theorem :: JORDAN2B:5

theorem :: JORDAN2B:6

theorem :: JORDAN2B:7

for i, n being ( ( ) ( natural V11() real ext-real V51() V129() V130() V131() V132() V133() V134() V135() ) Element of NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) ) st i : ( ( ) ( natural V11() real ext-real V51() V129() V130() V131() V132() V133() V134() V135() ) Element of NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) ) <= n : ( ( ) ( natural V11() real ext-real V51() V129() V130() V131() V132() V133() V134() V135() ) Element of NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) ) holds
(0* n : ( ( ) ( natural V11() real ext-real V51() V129() V130() V131() V132() V133() V134() V135() ) Element of NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) -valued Function-like V35() V42(b₂ : ( ( ) ( natural V11() real ext-real V51() V129() V130() V131() V132() V133() V134() V135() ) Element of NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like complex-yielding V120() V121() ) Element of REAL b₂ : ( ( ) ( natural V11() real ext-real V51() V129() V130() V131() V132() V133() V134() V135() ) Element of NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non empty functional FinSequence-membered ) FinSequenceSet of REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) ) | i : ( ( ) ( natural V11() real ext-real V51() V129() V130() V131() V132() V133() V134() V135() ) Element of NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) -valued Function-like V35() FinSequence-like FinSubsequence-like complex-yielding V120() V121() ) FinSequence of REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) = 0* i : ( ( ) ( natural V11() real ext-real V51() V129() V130() V131() V132() V133() V134() V135() ) Element of NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) -valued Function-like V35() V42(b₁ : ( ( ) ( natural V11() real ext-real V51() V129() V130() V131() V132() V133() V134() V135() ) Element of NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like complex-yielding V120() V121() ) Element of REAL b₁ : ( ( ) ( natural V11() real ext-real V51() V129() V130() V131() V132() V133() V134() V135() ) Element of NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non empty functional FinSequence-membered ) FinSequenceSet of REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) ) ;

theorem :: JORDAN2B:8

for n, i being ( ( ) ( natural V11() real ext-real V51() V129() V130() V131() V132() V133() V134() V135() ) Element of NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) ) holds (0* n : ( ( ) ( natural V11() real ext-real V51() V129() V130() V131() V132() V133() V134() V135() ) Element of NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) -valued Function-like V35() V42(b₁ : ( ( ) ( natural V11() real ext-real V51() V129() V130() V131() V132() V133() V134() V135() ) Element of NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like complex-yielding V120() V121() ) Element of REAL b₁ : ( ( ) ( natural V11() real ext-real V51() V129() V130() V131() V132() V133() V134() V135() ) Element of NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non empty functional FinSequence-membered ) FinSequenceSet of REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) ) /^ i : ( ( ) ( natural V11() real ext-real V51() V129() V130() V131() V132() V133() V134() V135() ) Element of NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) -valued Function-like V35() FinSequence-like FinSubsequence-like complex-yielding V120() V121() ) FinSequence of REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) = 0* (n : ( ( ) ( natural V11() real ext-real V51() V129() V130() V131() V132() V133() V134() V135() ) Element of NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) ) -' i : ( ( ) ( natural V11() real ext-real V51() V129() V130() V131() V132() V133() V134() V135() ) Element of NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( natural V11() real ext-real non negative V51() V129() V130() V131() V132() V133() V134() V135() ) Element of NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) -valued Function-like V35() V42(b₁ : ( ( ) ( natural V11() real ext-real V51() V129() V130() V131() V132() V133() V134() V135() ) Element of NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) ) -' b₂ : ( ( ) ( natural V11() real ext-real V51() V129() V130() V131() V132() V133() V134() V135() ) Element of NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( natural V11() real ext-real non negative V51() V129() V130() V131() V132() V133() V134() V135() ) Element of NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like complex-yielding V120() V121() ) Element of REAL (b₁ : ( ( ) ( natural V11() real ext-real V51() V129() V130() V131() V132() V133() V134() V135() ) Element of NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) ) -' b₂ : ( ( ) ( natural V11() real ext-real V51() V129() V130() V131() V132() V133() V134() V135() ) Element of NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( natural V11() real ext-real non negative V51() V129() V130() V131() V132() V133() V134() V135() ) Element of NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non empty functional FinSequence-membered ) FinSequenceSet of REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) ) ;

theorem :: JORDAN2B:9

theorem :: JORDAN2B:10

for i, n being ( ( ) ( natural V11() real ext-real V51() V129() V130() V131() V132() V133() V134() V135() ) Element of NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) )
for r being ( ( ) ( V11() real ext-real ) Real) st i : ( ( ) ( natural V11() real ext-real V51() V129() V130() V131() V132() V133() V134() V135() ) Element of NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) ) in Seg n : ( ( ) ( natural V11() real ext-real V51() V129() V130() V131() V132() V133() V134() V135() ) Element of NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V35() V42(b₂ : ( ( ) ( natural V11() real ext-real V51() V129() V130() V131() V132() V133() V134() V135() ) Element of NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) ) ) V130() V131() V132() V133() V134() V135() ) Element of K6(NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) holds
Sum ((0* n : ( ( ) ( natural V11() real ext-real V51() V129() V130() V131() V132() V133() V134() V135() ) Element of NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) -valued Function-like V35() V42(b₂ : ( ( ) ( natural V11() real ext-real V51() V129() V130() V131() V132() V133() V134() V135() ) Element of NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like complex-yielding V120() V121() ) Element of REAL b₂ : ( ( ) ( natural V11() real ext-real V51() V129() V130() V131() V132() V133() V134() V135() ) Element of NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non empty functional FinSequence-membered ) FinSequenceSet of REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) ) +* (i : ( ( ) ( natural V11() real ext-real V51() V129() V130() V131() V132() V133() V134() V135() ) Element of NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) ) ,r : ( ( ) ( V11() real ext-real ) Real) )) : ( ( ) ( Relation-like NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) -valued Function-like V35() FinSequence-like FinSubsequence-like complex-yielding V120() V121() ) FinSequence of REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) = r : ( ( ) ( V11() real ext-real ) Real) ;

theorem :: JORDAN2B:11

for n being ( ( ) ( natural V11() real ext-real V51() V129() V130() V131() V132() V133() V134() V135() ) Element of NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) )
for q being ( ( ) ( Relation-like NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) -valued Function-like V35() V42(b₁ : ( ( ) ( natural V11() real ext-real V51() V129() V130() V131() V132() V133() V134() V135() ) Element of NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like complex-yielding V120() V121() ) Element of REAL n : ( ( ) ( natural V11() real ext-real V51() V129() V130() V131() V132() V133() V134() V135() ) Element of NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non empty functional FinSequence-membered ) FinSequenceSet of REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) )
for p being ( ( ) ( Relation-like NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like V35() V42(b₁ : ( ( ) ( natural V11() real ext-real V51() V129() V130() V131() V132() V133() V134() V135() ) Element of NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like complex-yielding V120() V121() ) Point of ( ( ) ( non empty ) set ) )
for i being ( ( ) ( natural V11() real ext-real V51() V129() V130() V131() V132() V133() V134() V135() ) Element of NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) ) st i : ( ( ) ( natural V11() real ext-real V51() V129() V130() V131() V132() V133() V134() V135() ) Element of NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) ) in Seg n : ( ( ) ( natural V11() real ext-real V51() V129() V130() V131() V132() V133() V134() V135() ) Element of NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V35() V42(b₁ : ( ( ) ( natural V11() real ext-real V51() V129() V130() V131() V132() V133() V134() V135() ) Element of NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) ) ) V130() V131() V132() V133() V134() V135() ) Element of K6(NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) ) & q : ( ( ) ( Relation-like NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) -valued Function-like V35() V42(b₁ : ( ( ) ( natural V11() real ext-real V51() V129() V130() V131() V132() V133() V134() V135() ) Element of NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like complex-yielding V120() V121() ) Element of REAL b₁ : ( ( ) ( natural V11() real ext-real V51() V129() V130() V131() V132() V133() V134() V135() ) Element of NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non empty functional FinSequence-membered ) FinSequenceSet of REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) ) = p : ( ( ) ( Relation-like NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) -valued Function-like V35() V42(b₁ : ( ( ) ( natural V11() real ext-real V51() V129() V130() V131() V132() V133() V134() V135() ) Element of NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like complex-yielding V120() V121() ) Point of ( ( ) ( non empty ) set ) ) holds
( p : ( ( ) ( Relation-like NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) -valued Function-like V35() V42(b₁ : ( ( ) ( natural V11() real ext-real V51() V129() V130() V131() V132() V133() V134() V135() ) Element of NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like complex-yielding V120() V121() ) Point of ( ( ) ( non empty ) set ) ) /. i : ( ( ) ( natural V11() real ext-real V51() V129() V130() V131() V132() V133() V134() V135() ) Element of NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) <= |.q : ( ( ) ( Relation-like NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) -valued Function-like V35() V42(b₁ : ( ( ) ( natural V11() real ext-real V51() V129() V130() V131() V132() V133() V134() V135() ) Element of NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like complex-yielding V120() V121() ) Element of REAL b₁ : ( ( ) ( natural V11() real ext-real V51() V129() V130() V131() V132() V133() V134() V135() ) Element of NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non empty functional FinSequence-membered ) FinSequenceSet of REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) ) .| : ( ( ) ( V11() real ext-real non negative ) Element of REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) & (p : ( ( ) ( Relation-like NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) -valued Function-like V35() V42(b₁ : ( ( ) ( natural V11() real ext-real V51() V129() V130() V131() V132() V133() V134() V135() ) Element of NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like complex-yielding V120() V121() ) Point of ( ( ) ( non empty ) set ) ) /. i : ( ( ) ( natural V11() real ext-real V51() V129() V130() V131() V132() V133() V134() V135() ) Element of NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) ^2 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) <= |.q : ( ( ) ( Relation-like NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) -valued Function-like V35() V42(b₁ : ( ( ) ( natural V11() real ext-real V51() V129() V130() V131() V132() V133() V134() V135() ) Element of NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like complex-yielding V120() V121() ) Element of REAL b₁ : ( ( ) ( natural V11() real ext-real V51() V129() V130() V131() V132() V133() V134() V135() ) Element of NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non empty functional FinSequence-membered ) FinSequenceSet of REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) ) .| : ( ( ) ( V11() real ext-real non negative ) Element of REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) ^2 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) ) ;

begin

theorem :: JORDAN2B:12

theorem :: JORDAN2B:13

theorem :: JORDAN2B:14

theorem :: JORDAN2B:15

for n being ( ( ) ( natural V11() real ext-real V51() V129() V130() V131() V132() V133() V134() V135() ) Element of NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) )
for a, b being ( ( real ) ( V11() real ext-real ) number )
for f being ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of (TOP-REAL b₁ : ( ( ) ( natural V11() real ext-real V51() V129() V130() V131() V132() V133() V134() V135() ) Element of NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V190() ) ( non empty TopSpace-like V153() V178() V179() V180() V181() V182() V183() V184() V190() V219() V220() ) L15()) : ( ( ) ( non empty ) set ) -defined the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V118() ) TopStruct ) : ( ( ) ( non empty V130() V131() V132() ) set ) -valued Function-like total quasi_total complex-yielding V120() V121() ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty V130() V131() V132() ) set ) )
for i being ( ( ) ( natural V11() real ext-real V51() V129() V130() V131() V132() V133() V134() V135() ) Element of NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) ) st ( for p being ( ( ) ( Relation-like NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) -valued Function-like V35() V42(b₁ : ( ( ) ( natural V11() real ext-real V51() V129() V130() V131() V132() V133() V134() V135() ) Element of NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like complex-yielding V120() V121() ) Element of ( ( ) ( non empty ) set ) ) holds f : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of (TOP-REAL b₁ : ( ( ) ( natural V11() real ext-real V51() V129() V130() V131() V132() V133() V134() V135() ) Element of NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V190() ) ( non empty TopSpace-like V153() V178() V179() V180() V181() V182() V183() V184() V190() V219() V220() ) L15()) : ( ( ) ( non empty ) set ) -defined the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V118() ) TopStruct ) : ( ( ) ( non empty V130() V131() V132() ) set ) -valued Function-like total quasi_total complex-yielding V120() V121() ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty V130() V131() V132() ) set ) ) . p : ( ( ) ( Relation-like NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) -valued Function-like V35() V42(b₁ : ( ( ) ( natural V11() real ext-real V51() V129() V130() V131() V132() V133() V134() V135() ) Element of NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like complex-yielding V120() V121() ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( V11() real ext-real ) Element of the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V118() ) TopStruct ) : ( ( ) ( non empty V130() V131() V132() ) set ) ) = p : ( ( ) ( Relation-like NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) -valued Function-like V35() V42(b₁ : ( ( ) ( natural V11() real ext-real V51() V129() V130() V131() V132() V133() V134() V135() ) Element of NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like complex-yielding V120() V121() ) Element of ( ( ) ( non empty ) set ) ) /. i : ( ( ) ( natural V11() real ext-real V51() V129() V130() V131() V132() V133() V134() V135() ) Element of NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) ) holds
f : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of (TOP-REAL b₁ : ( ( ) ( natural V11() real ext-real V51() V129() V130() V131() V132() V133() V134() V135() ) Element of NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V190() ) ( non empty TopSpace-like V153() V178() V179() V180() V181() V182() V183() V184() V190() V219() V220() ) L15()) : ( ( ) ( non empty ) set ) -defined the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V118() ) TopStruct ) : ( ( ) ( non empty V130() V131() V132() ) set ) -valued Function-like total quasi_total complex-yielding V120() V121() ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty V130() V131() V132() ) set ) ) " { s : ( ( ) ( Relation-like NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) -valued Function-like V35() V42(b₁ : ( ( ) ( natural V11() real ext-real V51() V129() V130() V131() V132() V133() V134() V135() ) Element of NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like complex-yielding V120() V121() ) Element of ( ( ) ( non empty ) set ) ) where s is ( ( ) ( V11() real ext-real ) Real) : ( a : ( ( real ) ( V11() real ext-real ) number ) < s : ( ( ) ( Relation-like NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) -valued Function-like V35() V42(b₁ : ( ( ) ( natural V11() real ext-real V51() V129() V130() V131() V132() V133() V134() V135() ) Element of NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like complex-yielding V120() V121() ) Element of ( ( ) ( non empty ) set ) ) & s : ( ( ) ( Relation-like NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) -valued Function-like V35() V42(b₁ : ( ( ) ( natural V11() real ext-real V51() V129() V130() V131() V132() V133() V134() V135() ) Element of NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like complex-yielding V120() V121() ) Element of ( ( ) ( non empty ) set ) ) < b : ( ( real ) ( V11() real ext-real ) number ) ) } : ( ( ) ( ) Element of K6( the carrier of (TOP-REAL b₁ : ( ( ) ( natural V11() real ext-real V51() V129() V130() V131() V132() V133() V134() V135() ) Element of NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V190() ) ( non empty TopSpace-like V153() V178() V179() V180() V181() V182() V183() V184() V190() V219() V220() ) L15()) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) = { p : ( ( ) ( Relation-like NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) -valued Function-like V35() V42(b₁ : ( ( ) ( natural V11() real ext-real V51() V129() V130() V131() V132() V133() V134() V135() ) Element of NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like complex-yielding V120() V121() ) Element of ( ( ) ( non empty ) set ) ) where p is ( ( ) ( Relation-like NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) -valued Function-like V35() V42(b₁ : ( ( ) ( natural V11() real ext-real V51() V129() V130() V131() V132() V133() V134() V135() ) Element of NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like complex-yielding V120() V121() ) Element of ( ( ) ( non empty ) set ) ) : ( a : ( ( real ) ( V11() real ext-real ) number ) < p : ( ( ) ( Relation-like NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) -valued Function-like V35() V42(b₁ : ( ( ) ( natural V11() real ext-real V51() V129() V130() V131() V132() V133() V134() V135() ) Element of NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like complex-yielding V120() V121() ) Element of ( ( ) ( non empty ) set ) ) /. i : ( ( ) ( natural V11() real ext-real V51() V129() V130() V131() V132() V133() V134() V135() ) Element of NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) & p : ( ( ) ( Relation-like NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) -valued Function-like V35() V42(b₁ : ( ( ) ( natural V11() real ext-real V51() V129() V130() V131() V132() V133() V134() V135() ) Element of NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like complex-yielding V120() V121() ) Element of ( ( ) ( non empty ) set ) ) /. i : ( ( ) ( natural V11() real ext-real V51() V129() V130() V131() V132() V133() V134() V135() ) Element of NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) < b : ( ( real ) ( V11() real ext-real ) number ) ) } ;

theorem :: JORDAN2B:16

for X being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for M being ( ( non empty Reflexive discerning V111() triangle ) ( non empty Reflexive discerning V111() triangle Discerning ) MetrSpace)
for f being ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of (TopSpaceMetr b₂ : ( ( non empty Reflexive discerning V111() triangle ) ( non empty Reflexive discerning V111() triangle Discerning ) MetrSpace) ) : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) st ( for r being ( ( real ) ( V11() real ext-real ) number )
for u being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) )
for P being ( ( ) ( ) Subset of ) st r : ( ( real ) ( V11() real ext-real ) number ) > 0 : ( ( ) ( empty natural V11() real ext-real non positive non negative functional FinSequence-membered V51() V129() V130() V131() V132() V133() V134() V135() V136() ) Element of NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) ) & P : ( ( ) ( ) Subset of ) = Ball (u : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,r : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( ) Element of K6( the carrier of b₂ : ( ( non empty Reflexive discerning V111() triangle ) ( non empty Reflexive discerning V111() triangle Discerning ) MetrSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) holds
f : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of (TopSpaceMetr b₂ : ( ( non empty Reflexive discerning V111() triangle ) ( non empty Reflexive discerning V111() triangle Discerning ) MetrSpace) ) : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) " P : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of K6( the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) is open ) holds
f : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -defined the carrier of (TopSpaceMetr b₂ : ( ( non empty Reflexive discerning V111() triangle ) ( non empty Reflexive discerning V111() triangle Discerning ) MetrSpace) ) : ( ( ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) -valued Function-like total quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is continuous ;

theorem :: JORDAN2B:17

for u being ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V130() V131() V132() ) set ) )
for r, u1 being ( ( real ) ( V11() real ext-real ) number ) st u1 : ( ( real ) ( V11() real ext-real ) number ) = u : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V130() V131() V132() ) set ) ) holds
Ball (u : ( ( ) ( V11() real ext-real ) Point of ( ( ) ( non empty V130() V131() V132() ) set ) ) ,r : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V130() V131() V132() ) Element of K6( the carrier of RealSpace : ( ( strict ) ( non empty strict Reflexive discerning V111() triangle Discerning V118() ) MetrStruct ) : ( ( ) ( non empty V130() V131() V132() ) set ) ) : ( ( ) ( ) set ) ) = { s : ( ( ) ( V11() real ext-real ) Real) where s is ( ( ) ( V11() real ext-real ) Real) : ( u1 : ( ( real ) ( V11() real ext-real ) number ) - r : ( ( real ) ( V11() real ext-real ) number ) : ( ( ) ( V11() real ext-real ) set ) < s : ( ( ) ( V11() real ext-real ) Real) & s : ( ( ) ( V11() real ext-real ) Real) < u1 : ( ( real ) ( V11() real ext-real ) number ) + r : ( ( real ) ( V11() real ext-real ) number ) : ( ( ) ( V11() real ext-real ) set ) ) } ;

theorem :: JORDAN2B:18

begin

theorem :: JORDAN2B:19

for s being ( ( ) ( V11() real ext-real ) Real) holds abs <*s : ( ( ) ( V11() real ext-real ) Real) *> : ( ( ) ( non empty Relation-like NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) -valued Function-like V35() V42(1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V51() V129() V130() V131() V132() V133() V134() V135() ) Element of NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like complex-yielding V120() V121() ) FinSequence of REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) -valued Function-like V35() FinSequence-like FinSubsequence-like complex-yielding V120() V121() ) FinSequence of REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) = <*(abs s : ( ( ) ( V11() real ext-real ) Real) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) *> : ( ( ) ( non empty Relation-like NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) -valued Function-like V35() V42(1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V51() V129() V130() V131() V132() V133() V134() V135() ) Element of NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like complex-yielding V120() V121() ) FinSequence of REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) ;

theorem :: JORDAN2B:20

notation

let r be ( ( real ) ( V11() real ext-real ) number ) ;
synonym |[r]| for <*r*>;

end;

definition

let r be ( ( real ) ( V11() real ext-real ) number ) ;
:: original: |[
redefine func |[r]| -> ( ( ) ( Relation-like NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) -valued Function-like V35() V42(1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V51() V129() V130() V131() V132() V133() V134() V135() ) Element of NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like complex-yielding V120() V121() ) Point of ( ( ) ( non empty ) set ) ) ;

end;

theorem :: JORDAN2B:21

for r being ( ( real ) ( V11() real ext-real ) number )
for s being ( ( ) ( V11() real ext-real ) Real) holds s : ( ( ) ( V11() real ext-real ) Real) * |[r : ( ( real ) ( V11() real ext-real ) number ) ]| : ( ( ) ( non empty Relation-like NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) -valued Function-like V35() V42(1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V51() V129() V130() V131() V132() V133() V134() V135() ) Element of NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like complex-yielding V120() V121() ) Point of ( ( ) ( non empty ) set ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) -valued Function-like V35() V42(1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V51() V129() V130() V131() V132() V133() V134() V135() ) Element of NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like complex-yielding V120() V121() ) Element of the carrier of (TOP-REAL 1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V51() V129() V130() V131() V132() V133() V134() V135() ) Element of NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V190() ) ( non empty TopSpace-like V153() V178() V179() V180() V181() V182() V183() V184() V190() V219() V220() ) L15()) : ( ( ) ( non empty ) set ) ) = |[(s : ( ( ) ( V11() real ext-real ) Real) * r : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) ]| : ( ( ) ( non empty Relation-like NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) -valued Function-like V35() V42(1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V51() V129() V130() V131() V132() V133() V134() V135() ) Element of NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like complex-yielding V120() V121() ) Point of ( ( ) ( non empty ) set ) ) ;

theorem :: JORDAN2B:22

for r1, r2 being ( ( real ) ( V11() real ext-real ) number ) holds |[(r1 : ( ( real ) ( V11() real ext-real ) number ) + r2 : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( V11() real ext-real ) set ) ]| : ( ( ) ( non empty Relation-like NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) -valued Function-like V35() V42(1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V51() V129() V130() V131() V132() V133() V134() V135() ) Element of NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like complex-yielding V120() V121() ) Point of ( ( ) ( non empty ) set ) ) = |[r1 : ( ( real ) ( V11() real ext-real ) number ) ]| : ( ( ) ( non empty Relation-like NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) -valued Function-like V35() V42(1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V51() V129() V130() V131() V132() V133() V134() V135() ) Element of NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like complex-yielding V120() V121() ) Point of ( ( ) ( non empty ) set ) ) + |[r2 : ( ( real ) ( V11() real ext-real ) number ) ]| : ( ( ) ( non empty Relation-like NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) -valued Function-like V35() V42(1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V51() V129() V130() V131() V132() V133() V134() V135() ) Element of NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like complex-yielding V120() V121() ) Point of ( ( ) ( non empty ) set ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) -valued Function-like V35() V42(1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V51() V129() V130() V131() V132() V133() V134() V135() ) Element of NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like complex-yielding V120() V121() ) Element of the carrier of (TOP-REAL 1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V51() V129() V130() V131() V132() V133() V134() V135() ) Element of NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V190() ) ( non empty TopSpace-like V153() V178() V179() V180() V181() V182() V183() V184() V190() V219() V220() ) L15()) : ( ( ) ( non empty ) set ) ) ;

theorem :: JORDAN2B:23

for r1, r2 being ( ( real ) ( V11() real ext-real ) number ) st |[r1 : ( ( real ) ( V11() real ext-real ) number ) ]| : ( ( ) ( non empty Relation-like NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) -valued Function-like V35() V42(1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V51() V129() V130() V131() V132() V133() V134() V135() ) Element of NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like complex-yielding V120() V121() ) Point of ( ( ) ( non empty ) set ) ) = |[r2 : ( ( real ) ( V11() real ext-real ) number ) ]| : ( ( ) ( non empty Relation-like NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) -valued Function-like V35() V42(1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V51() V129() V130() V131() V132() V133() V134() V135() ) Element of NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like complex-yielding V120() V121() ) Point of ( ( ) ( non empty ) set ) ) holds
r1 : ( ( real ) ( V11() real ext-real ) number ) = r2 : ( ( real ) ( V11() real ext-real ) number ) ;

theorem :: JORDAN2B:24

for P being ( ( ) ( V130() V131() V132() ) Subset of )
for b being ( ( real ) ( V11() real ext-real ) number ) st P : ( ( ) ( V130() V131() V132() ) Subset of ) = { s : ( ( ) ( V11() real ext-real ) Real) where s is ( ( ) ( V11() real ext-real ) Real) : s : ( ( ) ( V11() real ext-real ) Real) < b : ( ( real ) ( V11() real ext-real ) number ) } holds
P : ( ( ) ( V130() V131() V132() ) Subset of ) is open ;

theorem :: JORDAN2B:25

for P being ( ( ) ( V130() V131() V132() ) Subset of )
for a being ( ( real ) ( V11() real ext-real ) number ) st P : ( ( ) ( V130() V131() V132() ) Subset of ) = { s : ( ( ) ( V11() real ext-real ) Real) where s is ( ( ) ( V11() real ext-real ) Real) : a : ( ( real ) ( V11() real ext-real ) number ) < s : ( ( ) ( V11() real ext-real ) Real) } holds
P : ( ( ) ( V130() V131() V132() ) Subset of ) is open ;

theorem :: JORDAN2B:26

for P being ( ( ) ( V130() V131() V132() ) Subset of )
for a, b being ( ( real ) ( V11() real ext-real ) number ) st P : ( ( ) ( V130() V131() V132() ) Subset of ) = { s : ( ( ) ( V11() real ext-real ) Real) where s is ( ( ) ( V11() real ext-real ) Real) : ( a : ( ( real ) ( V11() real ext-real ) number ) < s : ( ( ) ( V11() real ext-real ) Real) & s : ( ( ) ( V11() real ext-real ) Real) < b : ( ( real ) ( V11() real ext-real ) number ) ) } holds
P : ( ( ) ( V130() V131() V132() ) Subset of ) is open ;

theorem :: JORDAN2B:27

for u being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) )
for r, u1 being ( ( real ) ( V11() real ext-real ) number ) st <*u1 : ( ( real ) ( V11() real ext-real ) number ) *> : ( ( Relation-like Function-like ) ( non empty Relation-like NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) -defined Function-like V35() V42(1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V51() V129() V130() V131() V132() V133() V134() V135() ) Element of NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like ) set ) = u : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) holds
Ball (u : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,r : ( ( real ) ( V11() real ext-real ) number ) ) : ( ( ) ( ) Element of K6( the carrier of (Euclid 1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V51() V129() V130() V131() V132() V133() V134() V135() ) Element of NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict Reflexive discerning V111() triangle ) ( non empty strict Reflexive discerning V111() triangle Discerning ) MetrStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) = { <*s : ( ( ) ( V11() real ext-real ) Real) *> : ( ( ) ( non empty Relation-like NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) -valued Function-like V35() V42(1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V51() V129() V130() V131() V132() V133() V134() V135() ) Element of NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like complex-yielding V120() V121() ) FinSequence of REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) where s is ( ( ) ( V11() real ext-real ) Real) : ( u1 : ( ( real ) ( V11() real ext-real ) number ) - r : ( ( real ) ( V11() real ext-real ) number ) : ( ( ) ( V11() real ext-real ) set ) < s : ( ( ) ( V11() real ext-real ) Real) & s : ( ( ) ( V11() real ext-real ) Real) < u1 : ( ( real ) ( V11() real ext-real ) number ) + r : ( ( real ) ( V11() real ext-real ) number ) : ( ( ) ( V11() real ext-real ) set ) ) } ;

theorem :: JORDAN2B:28

for f being ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of (TOP-REAL 1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V51() V129() V130() V131() V132() V133() V134() V135() ) Element of NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V190() ) ( non empty TopSpace-like V153() V178() V179() V180() V181() V182() V183() V184() V190() V219() V220() ) L15()) : ( ( ) ( non empty ) set ) -defined the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V118() ) TopStruct ) : ( ( ) ( non empty V130() V131() V132() ) set ) -valued Function-like total quasi_total complex-yielding V120() V121() ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty V130() V131() V132() ) set ) ) st ( for p being ( ( ) ( Relation-like NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) -valued Function-like V35() V42(1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V51() V129() V130() V131() V132() V133() V134() V135() ) Element of NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like complex-yielding V120() V121() ) Element of ( ( ) ( non empty ) set ) ) holds f : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of (TOP-REAL 1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V51() V129() V130() V131() V132() V133() V134() V135() ) Element of NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V190() ) ( non empty TopSpace-like V153() V178() V179() V180() V181() V182() V183() V184() V190() V219() V220() ) L15()) : ( ( ) ( non empty ) set ) -defined the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V118() ) TopStruct ) : ( ( ) ( non empty V130() V131() V132() ) set ) -valued Function-like total quasi_total complex-yielding V120() V121() ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty V130() V131() V132() ) set ) ) . p : ( ( ) ( Relation-like NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) -valued Function-like V35() V42(1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V51() V129() V130() V131() V132() V133() V134() V135() ) Element of NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like complex-yielding V120() V121() ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( V11() real ext-real ) Element of the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V118() ) TopStruct ) : ( ( ) ( non empty V130() V131() V132() ) set ) ) = p : ( ( ) ( Relation-like NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) -valued Function-like V35() V42(1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V51() V129() V130() V131() V132() V133() V134() V135() ) Element of NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like complex-yielding V120() V121() ) Element of ( ( ) ( non empty ) set ) ) /. 1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V51() V129() V130() V131() V132() V133() V134() V135() ) Element of NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) ) holds
f : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of (TOP-REAL 1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V51() V129() V130() V131() V132() V133() V134() V135() ) Element of NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V190() ) ( non empty TopSpace-like V153() V178() V179() V180() V181() V182() V183() V184() V190() V219() V220() ) L15()) : ( ( ) ( non empty ) set ) -defined the carrier of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like V118() ) TopStruct ) : ( ( ) ( non empty V130() V131() V132() ) set ) -valued Function-like total quasi_total complex-yielding V120() V121() ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty V130() V131() V132() ) set ) ) is being_homeomorphism ;

theorem :: JORDAN2B:29

theorem :: JORDAN2B:30

for p being ( ( ) ( Relation-like NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) -valued Function-like V35() V42(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V51() V129() V130() V131() V132() V133() V134() V135() ) Element of NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like complex-yielding V120() V121() ) Element of ( ( ) ( non empty ) set ) ) holds
( p : ( ( ) ( Relation-like NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) -valued Function-like V35() V42(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V51() V129() V130() V131() V132() V133() V134() V135() ) Element of NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like complex-yielding V120() V121() ) Element of ( ( ) ( non empty ) set ) ) /. 1 : ( ( ) ( non empty natural V11() real ext-real positive non negative V51() V129() V130() V131() V132() V133() V134() V135() ) Element of NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) = proj1 : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V51() V129() V130() V131() V132() V133() V134() V135() ) Element of NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V190() ) ( non empty TopSpace-like V153() V178() V179() V180() V181() V182() V183() V184() V190() V219() V220() ) L15()) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) -valued Function-like total quasi_total complex-yielding V120() V121() ) Element of K6(K7( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V51() V129() V130() V131() V132() V133() V134() V135() ) Element of NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V190() ) ( non empty TopSpace-like V153() V178() V179() V180() V181() V182() V183() V184() V190() V219() V220() ) L15()) : ( ( ) ( non empty ) set ) ,REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( complex-yielding V120() V121() ) set ) ) : ( ( ) ( ) set ) ) . p : ( ( ) ( Relation-like NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) -valued Function-like V35() V42(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V51() V129() V130() V131() V132() V133() V134() V135() ) Element of NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like complex-yielding V120() V121() ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) & p : ( ( ) ( Relation-like NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) -valued Function-like V35() V42(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V51() V129() V130() V131() V132() V133() V134() V135() ) Element of NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like complex-yielding V120() V121() ) Element of ( ( ) ( non empty ) set ) ) /. 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V51() V129() V130() V131() V132() V133() V134() V135() ) Element of NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) = proj2 : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V51() V129() V130() V131() V132() V133() V134() V135() ) Element of NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V190() ) ( non empty TopSpace-like V153() V178() V179() V180() V181() V182() V183() V184() V190() V219() V220() ) L15()) : ( ( ) ( non empty ) set ) -defined REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) -valued Function-like total quasi_total complex-yielding V120() V121() ) Element of K6(K7( the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V51() V129() V130() V131() V132() V133() V134() V135() ) Element of NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V190() ) ( non empty TopSpace-like V153() V178() V179() V180() V181() V182() V183() V184() V190() V219() V220() ) L15()) : ( ( ) ( non empty ) set ) ,REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( complex-yielding V120() V121() ) set ) ) : ( ( ) ( ) set ) ) . p : ( ( ) ( Relation-like NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) -defined REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) -valued Function-like V35() V42(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V51() V129() V130() V131() V132() V133() V134() V135() ) Element of NAT : ( ( ) ( V130() V131() V132() V133() V134() V135() V136() ) Element of K6(REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like FinSubsequence-like complex-yielding V120() V121() ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V35() V130() V131() V132() V136() ) set ) ) ) ;