EUCLID

:: EUCLID_2 semantic presentation

begin

for n, i being ( ( natural ) ( natural V11() real ext-real ) Nat)
for v being ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) V20( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Element of n : ( ( natural ) ( natural V11() real ext-real ) Nat) -tuples_on REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) : ( ( ) ( V1() functional FinSequence-membered ) FinSequenceSet of REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) ) holds (mlt (v : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) V20( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Element of b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) -tuples_on REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) : ( ( ) ( V1() functional FinSequence-membered ) FinSequenceSet of REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) ) ,(0* n : ( ( natural ) ( natural V11() real ext-real ) Nat) ) : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) V20( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Element of REAL b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) : ( ( ) ( V1() functional FinSequence-membered ) FinSequenceSet of REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) ) )) : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) V20( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) FinSequence of REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) . i : ( ( natural ) ( natural V11() real ext-real ) Nat) : ( ( ) ( V11() real ext-real ) set ) = 0 : ( ( ) ( natural V11() real ext-real V33() V34() V129() V130() V131() V132() V133() V134() ) M3( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) , NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) )) ;

theorem :: EUCLID_2:2

for n being ( ( natural ) ( natural V11() real ext-real ) Nat)
for v being ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) V20( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Element of n : ( ( natural ) ( natural V11() real ext-real ) Nat) -tuples_on REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) : ( ( ) ( V1() functional FinSequence-membered ) FinSequenceSet of REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) ) holds mlt (v : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) V20( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Element of b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) -tuples_on REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) : ( ( ) ( V1() functional FinSequence-membered ) FinSequenceSet of REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) ) ,(0* n : ( ( natural ) ( natural V11() real ext-real ) Nat) ) : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) V20( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Element of REAL b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) : ( ( ) ( V1() functional FinSequence-membered ) FinSequenceSet of REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) ) ) : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) V20( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) FinSequence of REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) = 0* n : ( ( natural ) ( natural V11() real ext-real ) Nat) : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) V20( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Element of REAL b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) : ( ( ) ( V1() functional FinSequence-membered ) FinSequenceSet of REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) ) ;

begin

theorem :: EUCLID_2:3

for n being ( ( natural ) ( natural V11() real ext-real ) Nat)
for y1, y2 being ( ( V16() Function-like FinSequence-like real-valued ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) FinSequence)
for x1, x2 being ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) V20( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Element of REAL n : ( ( natural ) ( natural V11() real ext-real ) Nat) : ( ( ) ( V1() functional FinSequence-membered ) FinSequenceSet of REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) ) st x1 : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) V20( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Element of REAL b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) : ( ( ) ( V1() functional FinSequence-membered ) FinSequenceSet of REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) ) = y1 : ( ( V16() Function-like FinSequence-like real-valued ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) FinSequence) & x2 : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) V20( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Element of REAL b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) : ( ( ) ( V1() functional FinSequence-membered ) FinSequenceSet of REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) ) = y2 : ( ( V16() Function-like FinSequence-like real-valued ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) FinSequence) holds
|(y1 : ( ( V16() Function-like FinSequence-like real-valued ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) FinSequence) ,y2 : ( ( V16() Function-like FinSequence-like real-valued ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) FinSequence) )| : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) )) = (1 : ( ( ) ( V1() natural V11() real ext-real positive V33() V34() V129() V130() V131() V132() V133() V134() ) M3( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) , NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) )) / 4 : ( ( ) ( V1() natural V11() real ext-real positive V33() V34() V129() V130() V131() V132() V133() V134() ) M3( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) , NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) )) ) : ( ( ) ( V11() real ext-real V34() ) M2( RAT : ( ( ) ( V1() V37() V129() V130() V131() V132() V135() ) set ) )) * ((|.(x1 : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) V20( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Element of REAL b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) : ( ( ) ( V1() functional FinSequence-membered ) FinSequenceSet of REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) ) + x2 : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) V20( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Element of REAL b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) : ( ( ) ( V1() functional FinSequence-membered ) FinSequenceSet of REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) ) ) : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) V20( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Element of REAL b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) : ( ( ) ( V1() functional FinSequence-membered ) FinSequenceSet of REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) ) .| : ( ( ) ( V11() real ext-real non negative ) M2( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) )) ^2) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) )) - (|.(x1 : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) V20( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Element of REAL b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) : ( ( ) ( V1() functional FinSequence-membered ) FinSequenceSet of REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) ) - x2 : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) V20( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Element of REAL b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) : ( ( ) ( V1() functional FinSequence-membered ) FinSequenceSet of REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) ) ) : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) V20( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Element of REAL b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) : ( ( ) ( V1() functional FinSequence-membered ) FinSequenceSet of REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) ) .| : ( ( ) ( V11() real ext-real non negative ) M2( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) )) ^2) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) )) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) )) ;

theorem :: EUCLID_2:4

theorem :: EUCLID_2:5

theorem :: EUCLID_2:6

theorem :: EUCLID_2:7

theorem :: EUCLID_2:8

theorem :: EUCLID_2:9

for x being ( ( V16() Function-like FinSequence-like real-valued ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) FinSequence) holds |(x : ( ( V16() Function-like FinSequence-like real-valued ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) FinSequence) ,(0* (len x : ( ( V16() Function-like FinSequence-like real-valued ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) FinSequence) ) : ( ( ) ( natural V11() real ext-real V33() V34() V129() V130() V131() V132() V133() V134() ) M3( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) , NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) )) ) : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) V20( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) Function-like V37() V44( len b₁ : ( ( V16() Function-like FinSequence-like real-valued ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) FinSequence) : ( ( ) ( natural V11() real ext-real V33() V34() V129() V130() V131() V132() V133() V134() ) M3( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) , NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) )) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Element of REAL (len b₁ : ( ( V16() Function-like FinSequence-like real-valued ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) FinSequence) ) : ( ( ) ( natural V11() real ext-real V33() V34() V129() V130() V131() V132() V133() V134() ) M3( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) , NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) )) : ( ( ) ( V1() functional FinSequence-membered ) FinSequenceSet of REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) ) )| : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) )) = 0 : ( ( ) ( natural V11() real ext-real V33() V34() V129() V130() V131() V132() V133() V134() ) M3( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) , NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) )) ;

theorem :: EUCLID_2:10

for x being ( ( V16() Function-like FinSequence-like real-valued ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) FinSequence) holds |((0* (len x : ( ( V16() Function-like FinSequence-like real-valued ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) FinSequence) ) : ( ( ) ( natural V11() real ext-real V33() V34() V129() V130() V131() V132() V133() V134() ) M3( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) , NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) )) ) : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) V20( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) Function-like V37() V44( len b₁ : ( ( V16() Function-like FinSequence-like real-valued ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) FinSequence) : ( ( ) ( natural V11() real ext-real V33() V34() V129() V130() V131() V132() V133() V134() ) M3( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) , NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) )) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Element of REAL (len b₁ : ( ( V16() Function-like FinSequence-like real-valued ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) FinSequence) ) : ( ( ) ( natural V11() real ext-real V33() V34() V129() V130() V131() V132() V133() V134() ) M3( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) , NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) )) : ( ( ) ( V1() functional FinSequence-membered ) FinSequenceSet of REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) ) ,x : ( ( V16() Function-like FinSequence-like real-valued ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) FinSequence) )| : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) )) = 0 : ( ( ) ( natural V11() real ext-real V33() V34() V129() V130() V131() V132() V133() V134() ) M3( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) , NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) )) ;

theorem :: EUCLID_2:11

theorem :: EUCLID_2:12

theorem :: EUCLID_2:13

for x, y being ( ( V16() Function-like FinSequence-like real-valued ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) FinSequence) st len x : ( ( V16() Function-like FinSequence-like real-valued ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) FinSequence) : ( ( ) ( natural V11() real ext-real V33() V34() V129() V130() V131() V132() V133() V134() ) M3( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) , NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) )) = len y : ( ( V16() Function-like FinSequence-like real-valued ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) FinSequence) : ( ( ) ( natural V11() real ext-real V33() V34() V129() V130() V131() V132() V133() V134() ) M3( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) , NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) )) holds
(|.(x : ( ( V16() Function-like FinSequence-like real-valued ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) FinSequence) + y : ( ( V16() Function-like FinSequence-like real-valued ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) FinSequence) ) : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) V20( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) FinSequence of REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) .| : ( ( ) ( V11() real ext-real non negative ) M2( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) )) ^2) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) )) + (|.(x : ( ( V16() Function-like FinSequence-like real-valued ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) FinSequence) - y : ( ( V16() Function-like FinSequence-like real-valued ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) FinSequence) ) : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) V20( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) FinSequence of REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) .| : ( ( ) ( V11() real ext-real non negative ) M2( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) )) ^2) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) )) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) )) = 2 : ( ( ) ( V1() natural V11() real ext-real positive V33() V34() V129() V130() V131() V132() V133() V134() ) M3( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) , NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) )) * ((|.x : ( ( V16() Function-like FinSequence-like real-valued ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) FinSequence) .| : ( ( ) ( V11() real ext-real non negative ) M2( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) )) ^2) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) )) + (|.y : ( ( V16() Function-like FinSequence-like real-valued ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) FinSequence) .| : ( ( ) ( V11() real ext-real non negative ) M2( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) )) ^2) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) )) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) )) ;

theorem :: EUCLID_2:14

theorem :: EUCLID_2:15

theorem :: EUCLID_2:16

begin

theorem :: EUCLID_2:17

for n being ( ( natural ) ( natural V11() real ext-real ) Nat)
for p1, p2 being ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) holds |(p1 : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) ,p2 : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) )| : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) )) = (1 : ( ( ) ( V1() natural V11() real ext-real positive V33() V34() V129() V130() V131() V132() V133() V134() ) M3( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) , NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) )) / 4 : ( ( ) ( V1() natural V11() real ext-real positive V33() V34() V129() V130() V131() V132() V133() V134() ) M3( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) , NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) )) ) : ( ( ) ( V11() real ext-real V34() ) M2( RAT : ( ( ) ( V1() V37() V129() V130() V131() V132() V135() ) set ) )) * ((|.(p1 : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) + p2 : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) ) : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) M2( the U1 of (TOP-REAL b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) : ( ( V198() ) ( V50() V76() V141() V142() TopSpace-like V186() V187() V188() V189() V190() V191() V192() V198() ) L16()) : ( ( ) ( ) set ) )) .| : ( ( ) ( V11() real ext-real non negative ) M2( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) )) ^2) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) )) - (|.(p1 : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) - p2 : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) ) : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) M2( the U1 of (TOP-REAL b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) : ( ( V198() ) ( V50() V76() V141() V142() TopSpace-like V186() V187() V188() V189() V190() V191() V192() V198() ) L16()) : ( ( ) ( ) set ) )) .| : ( ( ) ( V11() real ext-real non negative ) M2( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) )) ^2) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) )) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) )) ;

theorem :: EUCLID_2:18

for n being ( ( natural ) ( natural V11() real ext-real ) Nat)
for p1, p2, p3 being ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) holds |((p1 : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) + p2 : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) ) : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) M2( the U1 of (TOP-REAL b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) : ( ( V198() ) ( V50() V76() V141() V142() TopSpace-like V186() V187() V188() V189() V190() V191() V192() V198() ) L16()) : ( ( ) ( ) set ) )) ,p3 : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) )| : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) )) = |(p1 : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) ,p3 : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) )| : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) )) + |(p2 : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) ,p3 : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) )| : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) )) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) )) ;

theorem :: EUCLID_2:19

theorem :: EUCLID_2:20

theorem :: EUCLID_2:21

theorem :: EUCLID_2:22

theorem :: EUCLID_2:23

theorem :: EUCLID_2:24

for n being ( ( natural ) ( natural V11() real ext-real ) Nat)
for p1, p2, p3 being ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) holds |((p1 : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) - p2 : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) ) : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) M2( the U1 of (TOP-REAL b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) : ( ( V198() ) ( V50() V76() V141() V142() TopSpace-like V186() V187() V188() V189() V190() V191() V192() V198() ) L16()) : ( ( ) ( ) set ) )) ,p3 : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) )| : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) )) = |(p1 : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) ,p3 : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) )| : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) )) - |(p2 : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) ,p3 : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) )| : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) )) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) )) ;

theorem :: EUCLID_2:25

for n being ( ( natural ) ( natural V11() real ext-real ) Nat)
for x, y being ( ( real ) ( V11() real ext-real ) number )
for p1, p2, p3 being ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) holds |(((x : ( ( real ) ( V11() real ext-real ) number ) * p1 : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) ) : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) M2( the U1 of (TOP-REAL b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) : ( ( V198() ) ( V50() V76() V141() V142() TopSpace-like V186() V187() V188() V189() V190() V191() V192() V198() ) L16()) : ( ( ) ( ) set ) )) + (y : ( ( real ) ( V11() real ext-real ) number ) * p2 : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) ) : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) M2( the U1 of (TOP-REAL b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) : ( ( V198() ) ( V50() V76() V141() V142() TopSpace-like V186() V187() V188() V189() V190() V191() V192() V198() ) L16()) : ( ( ) ( ) set ) )) ) : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) M2( the U1 of (TOP-REAL b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) : ( ( V198() ) ( V50() V76() V141() V142() TopSpace-like V186() V187() V188() V189() V190() V191() V192() V198() ) L16()) : ( ( ) ( ) set ) )) ,p3 : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) )| : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) )) = (x : ( ( real ) ( V11() real ext-real ) number ) * |(p1 : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) ,p3 : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) )| : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) )) + (y : ( ( real ) ( V11() real ext-real ) number ) * |(p2 : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) ,p3 : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) )| : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) )) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) )) ;

theorem :: EUCLID_2:26

for n being ( ( natural ) ( natural V11() real ext-real ) Nat)
for p, q1, q2 being ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) holds |(p : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) ,(q1 : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) + q2 : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) ) : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) M2( the U1 of (TOP-REAL b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) : ( ( V198() ) ( V50() V76() V141() V142() TopSpace-like V186() V187() V188() V189() V190() V191() V192() V198() ) L16()) : ( ( ) ( ) set ) )) )| : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) )) = |(p : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) ,q1 : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) )| : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) )) + |(p : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) ,q2 : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) )| : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) )) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) )) ;

theorem :: EUCLID_2:27

for n being ( ( natural ) ( natural V11() real ext-real ) Nat)
for p, q1, q2 being ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) holds |(p : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) ,(q1 : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) - q2 : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) ) : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) M2( the U1 of (TOP-REAL b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) : ( ( V198() ) ( V50() V76() V141() V142() TopSpace-like V186() V187() V188() V189() V190() V191() V192() V198() ) L16()) : ( ( ) ( ) set ) )) )| : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) )) = |(p : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) ,q1 : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) )| : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) )) - |(p : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) ,q2 : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) )| : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) )) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) )) ;

theorem :: EUCLID_2:28

for n being ( ( natural ) ( natural V11() real ext-real ) Nat)
for p1, p2, q1, q2 being ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) holds |((p1 : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) + p2 : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) ) : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) M2( the U1 of (TOP-REAL b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) : ( ( V198() ) ( V50() V76() V141() V142() TopSpace-like V186() V187() V188() V189() V190() V191() V192() V198() ) L16()) : ( ( ) ( ) set ) )) ,(q1 : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) + q2 : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) ) : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) M2( the U1 of (TOP-REAL b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) : ( ( V198() ) ( V50() V76() V141() V142() TopSpace-like V186() V187() V188() V189() V190() V191() V192() V198() ) L16()) : ( ( ) ( ) set ) )) )| : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) )) = ((|(p1 : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) ,q1 : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) )| : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) )) + |(p1 : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) ,q2 : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) )| : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) )) + |(p2 : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) ,q1 : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) )| : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) )) + |(p2 : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) ,q2 : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) )| : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) )) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) )) ;

theorem :: EUCLID_2:29

for n being ( ( natural ) ( natural V11() real ext-real ) Nat)
for p1, p2, q1, q2 being ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) holds |((p1 : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) - p2 : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) ) : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) M2( the U1 of (TOP-REAL b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) : ( ( V198() ) ( V50() V76() V141() V142() TopSpace-like V186() V187() V188() V189() V190() V191() V192() V198() ) L16()) : ( ( ) ( ) set ) )) ,(q1 : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) - q2 : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) ) : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) M2( the U1 of (TOP-REAL b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) : ( ( V198() ) ( V50() V76() V141() V142() TopSpace-like V186() V187() V188() V189() V190() V191() V192() V198() ) L16()) : ( ( ) ( ) set ) )) )| : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) )) = ((|(p1 : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) ,q1 : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) )| : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) )) - |(p1 : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) ,q2 : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) )| : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) )) - |(p2 : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) ,q1 : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) )| : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) )) + |(p2 : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) ,q2 : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) )| : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) )) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) )) ;

theorem :: EUCLID_2:30

for n being ( ( natural ) ( natural V11() real ext-real ) Nat)
for p, q being ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) holds |((p : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) + q : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) ) : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) M2( the U1 of (TOP-REAL b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) : ( ( V198() ) ( V50() V76() V141() V142() TopSpace-like V186() V187() V188() V189() V190() V191() V192() V198() ) L16()) : ( ( ) ( ) set ) )) ,(p : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) + q : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) ) : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) M2( the U1 of (TOP-REAL b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) : ( ( V198() ) ( V50() V76() V141() V142() TopSpace-like V186() V187() V188() V189() V190() V191() V192() V198() ) L16()) : ( ( ) ( ) set ) )) )| : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) )) = (|(p : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) ,p : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) )| : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) )) + (2 : ( ( ) ( V1() natural V11() real ext-real positive V33() V34() V129() V130() V131() V132() V133() V134() ) M3( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) , NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) )) * |(p : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) ,q : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) )| : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) )) + |(q : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) ,q : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) )| : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) )) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) )) ;

theorem :: EUCLID_2:31

for n being ( ( natural ) ( natural V11() real ext-real ) Nat)
for p, q being ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) holds |((p : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) - q : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) ) : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) M2( the U1 of (TOP-REAL b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) : ( ( V198() ) ( V50() V76() V141() V142() TopSpace-like V186() V187() V188() V189() V190() V191() V192() V198() ) L16()) : ( ( ) ( ) set ) )) ,(p : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) - q : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) ) : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) M2( the U1 of (TOP-REAL b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) : ( ( V198() ) ( V50() V76() V141() V142() TopSpace-like V186() V187() V188() V189() V190() V191() V192() V198() ) L16()) : ( ( ) ( ) set ) )) )| : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) )) = (|(p : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) ,p : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) )| : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) )) - (2 : ( ( ) ( V1() natural V11() real ext-real positive V33() V34() V129() V130() V131() V132() V133() V134() ) M3( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) , NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) )) * |(p : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) ,q : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) )| : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) )) + |(q : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) ,q : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) )| : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) )) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) )) ;

theorem :: EUCLID_2:32

for n being ( ( natural ) ( natural V11() real ext-real ) Nat)
for p being ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) holds |(p : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) ,(0. (TOP-REAL n : ( ( natural ) ( natural V11() real ext-real ) Nat) ) : ( ( V198() ) ( V50() V76() V141() V142() TopSpace-like V186() V187() V188() V189() V190() V191() V192() V198() ) L16()) ) : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) M2( the U1 of (TOP-REAL b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) : ( ( V198() ) ( V50() V76() V141() V142() TopSpace-like V186() V187() V188() V189() V190() V191() V192() V198() ) L16()) : ( ( ) ( ) set ) )) )| : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) )) = 0 : ( ( ) ( natural V11() real ext-real V33() V34() V129() V130() V131() V132() V133() V134() ) M3( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) , NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) )) ;

theorem :: EUCLID_2:33

for n being ( ( natural ) ( natural V11() real ext-real ) Nat)
for p being ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) holds |((0. (TOP-REAL n : ( ( natural ) ( natural V11() real ext-real ) Nat) ) : ( ( V198() ) ( V50() V76() V141() V142() TopSpace-like V186() V187() V188() V189() V190() V191() V192() V198() ) L16()) ) : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) M2( the U1 of (TOP-REAL b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) : ( ( V198() ) ( V50() V76() V141() V142() TopSpace-like V186() V187() V188() V189() V190() V191() V192() V198() ) L16()) : ( ( ) ( ) set ) )) ,p : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) )| : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) )) = 0 : ( ( ) ( natural V11() real ext-real V33() V34() V129() V130() V131() V132() V133() V134() ) M3( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) , NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) )) ;

theorem :: EUCLID_2:34

for n being ( ( natural ) ( natural V11() real ext-real ) Nat) holds |((0. (TOP-REAL n : ( ( natural ) ( natural V11() real ext-real ) Nat) ) : ( ( V198() ) ( V50() V76() V141() V142() TopSpace-like V186() V187() V188() V189() V190() V191() V192() V198() ) L16()) ) : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) M2( the U1 of (TOP-REAL b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) : ( ( V198() ) ( V50() V76() V141() V142() TopSpace-like V186() V187() V188() V189() V190() V191() V192() V198() ) L16()) : ( ( ) ( ) set ) )) ,(0. (TOP-REAL n : ( ( natural ) ( natural V11() real ext-real ) Nat) ) : ( ( V198() ) ( V50() V76() V141() V142() TopSpace-like V186() V187() V188() V189() V190() V191() V192() V198() ) L16()) ) : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) M2( the U1 of (TOP-REAL b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) : ( ( V198() ) ( V50() V76() V141() V142() TopSpace-like V186() V187() V188() V189() V190() V191() V192() V198() ) L16()) : ( ( ) ( ) set ) )) )| : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) )) = 0 : ( ( ) ( natural V11() real ext-real V33() V34() V129() V130() V131() V132() V133() V134() ) M3( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) , NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) )) ;

theorem :: EUCLID_2:35

theorem :: EUCLID_2:36

theorem :: EUCLID_2:37

theorem :: EUCLID_2:38

theorem :: EUCLID_2:39

for n being ( ( natural ) ( natural V11() real ext-real ) Nat) holds |.(0. (TOP-REAL n : ( ( natural ) ( natural V11() real ext-real ) Nat) ) : ( ( V198() ) ( V50() V76() V141() V142() TopSpace-like V186() V187() V188() V189() V190() V191() V192() V198() ) L16()) ) : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) M2( the U1 of (TOP-REAL b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) : ( ( V198() ) ( V50() V76() V141() V142() TopSpace-like V186() V187() V188() V189() V190() V191() V192() V198() ) L16()) : ( ( ) ( ) set ) )) .| : ( ( ) ( V11() real ext-real non negative ) M2( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) )) = 0 : ( ( ) ( natural V11() real ext-real V33() V34() V129() V130() V131() V132() V133() V134() ) M3( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) , NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) )) ;

theorem :: EUCLID_2:40

for n being ( ( natural ) ( natural V11() real ext-real ) Nat)
for p being ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) holds
( |(p : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) ,p : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) )| : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) )) = 0 : ( ( ) ( natural V11() real ext-real V33() V34() V129() V130() V131() V132() V133() V134() ) M3( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) , NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) )) iff |.p : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) .| : ( ( ) ( V11() real ext-real non negative ) M2( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) )) = 0 : ( ( ) ( natural V11() real ext-real V33() V34() V129() V130() V131() V132() V133() V134() ) M3( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) , NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) )) ) ;

theorem :: EUCLID_2:41

for n being ( ( natural ) ( natural V11() real ext-real ) Nat)
for p being ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) holds
( |(p : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) ,p : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) )| : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) )) = 0 : ( ( ) ( natural V11() real ext-real V33() V34() V129() V130() V131() V132() V133() V134() ) M3( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) , NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) )) iff p : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) = 0. (TOP-REAL n : ( ( natural ) ( natural V11() real ext-real ) Nat) ) : ( ( V198() ) ( V50() V76() V141() V142() TopSpace-like V186() V187() V188() V189() V190() V191() V192() V198() ) L16()) : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) M2( the U1 of (TOP-REAL b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) : ( ( V198() ) ( V50() V76() V141() V142() TopSpace-like V186() V187() V188() V189() V190() V191() V192() V198() ) L16()) : ( ( ) ( ) set ) )) ) ;

theorem :: EUCLID_2:42

for n being ( ( natural ) ( natural V11() real ext-real ) Nat)
for p being ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) holds
( |.p : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) .| : ( ( ) ( V11() real ext-real non negative ) M2( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) )) = 0 : ( ( ) ( natural V11() real ext-real V33() V34() V129() V130() V131() V132() V133() V134() ) M3( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) , NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) )) iff p : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) = 0. (TOP-REAL n : ( ( natural ) ( natural V11() real ext-real ) Nat) ) : ( ( V198() ) ( V50() V76() V141() V142() TopSpace-like V186() V187() V188() V189() V190() V191() V192() V198() ) L16()) : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) M2( the U1 of (TOP-REAL b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) : ( ( V198() ) ( V50() V76() V141() V142() TopSpace-like V186() V187() V188() V189() V190() V191() V192() V198() ) L16()) : ( ( ) ( ) set ) )) ) ;

theorem :: EUCLID_2:43

for n being ( ( natural ) ( natural V11() real ext-real ) Nat)
for p being ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) holds
( p : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) <> 0. (TOP-REAL n : ( ( natural ) ( natural V11() real ext-real ) Nat) ) : ( ( V198() ) ( V50() V76() V141() V142() TopSpace-like V186() V187() V188() V189() V190() V191() V192() V198() ) L16()) : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) M2( the U1 of (TOP-REAL b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) : ( ( V198() ) ( V50() V76() V141() V142() TopSpace-like V186() V187() V188() V189() V190() V191() V192() V198() ) L16()) : ( ( ) ( ) set ) )) iff |(p : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) ,p : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) )| : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) )) > 0 : ( ( ) ( natural V11() real ext-real V33() V34() V129() V130() V131() V132() V133() V134() ) M3( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) , NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) )) ) ;

theorem :: EUCLID_2:44

for n being ( ( natural ) ( natural V11() real ext-real ) Nat)
for p being ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) holds
( p : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) <> 0. (TOP-REAL n : ( ( natural ) ( natural V11() real ext-real ) Nat) ) : ( ( V198() ) ( V50() V76() V141() V142() TopSpace-like V186() V187() V188() V189() V190() V191() V192() V198() ) L16()) : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) M2( the U1 of (TOP-REAL b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) : ( ( V198() ) ( V50() V76() V141() V142() TopSpace-like V186() V187() V188() V189() V190() V191() V192() V198() ) L16()) : ( ( ) ( ) set ) )) iff |.p : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) .| : ( ( ) ( V11() real ext-real non negative ) M2( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) )) > 0 : ( ( ) ( natural V11() real ext-real V33() V34() V129() V130() V131() V132() V133() V134() ) M3( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) , NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) )) ) ;

theorem :: EUCLID_2:45

for n being ( ( natural ) ( natural V11() real ext-real ) Nat)
for p, q being ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) holds |.(p : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) + q : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) ) : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) M2( the U1 of (TOP-REAL b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) : ( ( V198() ) ( V50() V76() V141() V142() TopSpace-like V186() V187() V188() V189() V190() V191() V192() V198() ) L16()) : ( ( ) ( ) set ) )) .| : ( ( ) ( V11() real ext-real non negative ) M2( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) )) ^2 : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) )) = ((|.p : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) .| : ( ( ) ( V11() real ext-real non negative ) M2( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) )) ^2) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) )) + (2 : ( ( ) ( V1() natural V11() real ext-real positive V33() V34() V129() V130() V131() V132() V133() V134() ) M3( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) , NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) )) * |(q : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) ,p : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) )| : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) )) + (|.q : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) .| : ( ( ) ( V11() real ext-real non negative ) M2( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) )) ^2) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) )) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) )) ;

theorem :: EUCLID_2:46

for n being ( ( natural ) ( natural V11() real ext-real ) Nat)
for p, q being ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) holds |.(p : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) - q : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) ) : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) M2( the U1 of (TOP-REAL b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) : ( ( V198() ) ( V50() V76() V141() V142() TopSpace-like V186() V187() V188() V189() V190() V191() V192() V198() ) L16()) : ( ( ) ( ) set ) )) .| : ( ( ) ( V11() real ext-real non negative ) M2( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) )) ^2 : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) )) = ((|.p : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) .| : ( ( ) ( V11() real ext-real non negative ) M2( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) )) ^2) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) )) - (2 : ( ( ) ( V1() natural V11() real ext-real positive V33() V34() V129() V130() V131() V132() V133() V134() ) M3( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) , NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) )) * |(q : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) ,p : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) )| : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) )) + (|.q : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) .| : ( ( ) ( V11() real ext-real non negative ) M2( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) )) ^2) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) )) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) )) ;

theorem :: EUCLID_2:47

for n being ( ( natural ) ( natural V11() real ext-real ) Nat)
for p, q being ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) holds (|.(p : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) + q : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) ) : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) M2( the U1 of (TOP-REAL b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) : ( ( V198() ) ( V50() V76() V141() V142() TopSpace-like V186() V187() V188() V189() V190() V191() V192() V198() ) L16()) : ( ( ) ( ) set ) )) .| : ( ( ) ( V11() real ext-real non negative ) M2( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) )) ^2) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) )) + (|.(p : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) - q : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) ) : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) M2( the U1 of (TOP-REAL b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) : ( ( V198() ) ( V50() V76() V141() V142() TopSpace-like V186() V187() V188() V189() V190() V191() V192() V198() ) L16()) : ( ( ) ( ) set ) )) .| : ( ( ) ( V11() real ext-real non negative ) M2( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) )) ^2) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) )) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) )) = 2 : ( ( ) ( V1() natural V11() real ext-real positive V33() V34() V129() V130() V131() V132() V133() V134() ) M3( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) , NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) )) * ((|.p : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) .| : ( ( ) ( V11() real ext-real non negative ) M2( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) )) ^2) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) )) + (|.q : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) .| : ( ( ) ( V11() real ext-real non negative ) M2( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) )) ^2) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) )) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) )) ;

theorem :: EUCLID_2:48

for n being ( ( natural ) ( natural V11() real ext-real ) Nat)
for p, q being ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) holds (|.(p : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) + q : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) ) : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) M2( the U1 of (TOP-REAL b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) : ( ( V198() ) ( V50() V76() V141() V142() TopSpace-like V186() V187() V188() V189() V190() V191() V192() V198() ) L16()) : ( ( ) ( ) set ) )) .| : ( ( ) ( V11() real ext-real non negative ) M2( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) )) ^2) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) )) - (|.(p : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) - q : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) ) : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) M2( the U1 of (TOP-REAL b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) : ( ( V198() ) ( V50() V76() V141() V142() TopSpace-like V186() V187() V188() V189() V190() V191() V192() V198() ) L16()) : ( ( ) ( ) set ) )) .| : ( ( ) ( V11() real ext-real non negative ) M2( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) )) ^2) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) )) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) )) = 4 : ( ( ) ( V1() natural V11() real ext-real positive V33() V34() V129() V130() V131() V132() V133() V134() ) M3( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) , NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) )) * |(p : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) ,q : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) )| : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) )) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) )) ;

theorem :: EUCLID_2:49

for n being ( ( natural ) ( natural V11() real ext-real ) Nat)
for p, q being ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) holds |(p : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) ,q : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) )| : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) )) = (1 : ( ( ) ( V1() natural V11() real ext-real positive V33() V34() V129() V130() V131() V132() V133() V134() ) M3( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) , NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) )) / 4 : ( ( ) ( V1() natural V11() real ext-real positive V33() V34() V129() V130() V131() V132() V133() V134() ) M3( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) , NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) )) ) : ( ( ) ( V11() real ext-real V34() ) M2( RAT : ( ( ) ( V1() V37() V129() V130() V131() V132() V135() ) set ) )) * ((|.(p : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) + q : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) ) : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) M2( the U1 of (TOP-REAL b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) : ( ( V198() ) ( V50() V76() V141() V142() TopSpace-like V186() V187() V188() V189() V190() V191() V192() V198() ) L16()) : ( ( ) ( ) set ) )) .| : ( ( ) ( V11() real ext-real non negative ) M2( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) )) ^2) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) )) - (|.(p : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) - q : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) ) : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) M2( the U1 of (TOP-REAL b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) : ( ( V198() ) ( V50() V76() V141() V142() TopSpace-like V186() V187() V188() V189() V190() V191() V192() V198() ) L16()) : ( ( ) ( ) set ) )) .| : ( ( ) ( V11() real ext-real non negative ) M2( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) )) ^2) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) )) ) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) )) : ( ( ) ( V11() real ext-real ) M2( REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) )) ;

theorem :: EUCLID_2:50

theorem :: EUCLID_2:51

theorem :: EUCLID_2:52

theorem :: EUCLID_2:53

theorem :: EUCLID_2:54

theorem :: EUCLID_2:55

for n being ( ( natural ) ( natural V11() real ext-real ) Nat)
for p being ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) holds
( p : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) ,p : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) are_orthogonal iff p : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) = 0. (TOP-REAL n : ( ( natural ) ( natural V11() real ext-real ) Nat) ) : ( ( V198() ) ( V50() V76() V141() V142() TopSpace-like V186() V187() V188() V189() V190() V191() V192() V198() ) L16()) : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) M2( the U1 of (TOP-REAL b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) : ( ( V198() ) ( V50() V76() V141() V142() TopSpace-like V186() V187() V188() V189() V190() V191() V192() V198() ) L16()) : ( ( ) ( ) set ) )) ) ;

theorem :: EUCLID_2:56

for n being ( ( natural ) ( natural V11() real ext-real ) Nat)
for a being ( ( real ) ( V11() real ext-real ) number )
for p, q being ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) st p : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) ,q : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) are_orthogonal holds
a : ( ( real ) ( V11() real ext-real ) number ) * p : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) M2( the U1 of (TOP-REAL b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) : ( ( V198() ) ( V50() V76() V141() V142() TopSpace-like V186() V187() V188() V189() V190() V191() V192() V198() ) L16()) : ( ( ) ( ) set ) )) ,q : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) are_orthogonal ;

theorem :: EUCLID_2:57

for n being ( ( natural ) ( natural V11() real ext-real ) Nat)
for a being ( ( real ) ( V11() real ext-real ) number )
for p, q being ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) st p : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) ,q : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) are_orthogonal holds
p : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) ,a : ( ( real ) ( V11() real ext-real ) number ) * q : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) M2( the U1 of (TOP-REAL b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) : ( ( V198() ) ( V50() V76() V141() V142() TopSpace-like V186() V187() V188() V189() V190() V191() V192() V198() ) L16()) : ( ( ) ( ) set ) )) are_orthogonal ;

theorem :: EUCLID_2:58

for n being ( ( natural ) ( natural V11() real ext-real ) Nat)
for p being ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) st ( for q being ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) holds p : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) ,q : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) are_orthogonal ) holds
p : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) Point of ( ( ) ( ) set ) ) = 0. (TOP-REAL n : ( ( natural ) ( natural V11() real ext-real ) Nat) ) : ( ( V198() ) ( V50() V76() V141() V142() TopSpace-like V186() V187() V188() V189() V190() V191() V192() V198() ) L16()) : ( ( ) ( V16() V19( NAT : ( ( ) ( V129() V130() V131() V132() V133() V134() V135() ) M2(K6(REAL : ( ( ) ( V1() V37() V129() V130() V131() V135() ) set ) ) : ( ( ) ( ) set ) )) ) Function-like V37() V44(b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued ) M2( the U1 of (TOP-REAL b₁ : ( ( natural ) ( natural V11() real ext-real ) Nat) ) : ( ( V198() ) ( V50() V76() V141() V142() TopSpace-like V186() V187() V188() V189() V190() V191() V192() V198() ) L16()) : ( ( ) ( ) set ) )) ;