begin
Lm1:
for x being real number holds (x ^2 ) + 1 > 0
Lm2:
dom proj1 = the carrier of (TOP-REAL 2)
by FUNCT_2:def 1;
Lm3:
dom proj2 = the carrier of (TOP-REAL 2)
by FUNCT_2:def 1;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
theorem
theorem
canceled;
theorem Th13:
begin
definition
func Sq_Circ -> Function of the
carrier of
(TOP-REAL 2),the
carrier of
(TOP-REAL 2) means :
Def1:
for
p being
Point of
(TOP-REAL 2) holds
( (
p = 0. (TOP-REAL 2) implies
it . p = p ) & ( ( (
p `2 <= p `1 &
- (p `1 ) <= p `2 ) or (
p `2 >= p `1 &
p `2 <= - (p `1 ) ) ) &
p <> 0. (TOP-REAL 2) implies
it . p = |[((p `1 ) / (sqrt (1 + (((p `2 ) / (p `1 )) ^2 )))),((p `2 ) / (sqrt (1 + (((p `2 ) / (p `1 )) ^2 ))))]| ) & ( (
p `2 <= p `1 &
- (p `1 ) <= p `2 ) or (
p `2 >= p `1 &
p `2 <= - (p `1 ) ) or not
p <> 0. (TOP-REAL 2) or
it . p = |[((p `1 ) / (sqrt (1 + (((p `1 ) / (p `2 )) ^2 )))),((p `2 ) / (sqrt (1 + (((p `1 ) / (p `2 )) ^2 ))))]| ) );
existence
ex b1 being Function of the carrier of (TOP-REAL 2),the carrier of (TOP-REAL 2) st
for p being Point of (TOP-REAL 2) holds
( ( p = 0. (TOP-REAL 2) implies b1 . p = p ) & ( ( ( p `2 <= p `1 & - (p `1 ) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1 ) ) ) & p <> 0. (TOP-REAL 2) implies b1 . p = |[((p `1 ) / (sqrt (1 + (((p `2 ) / (p `1 )) ^2 )))),((p `2 ) / (sqrt (1 + (((p `2 ) / (p `1 )) ^2 ))))]| ) & ( ( p `2 <= p `1 & - (p `1 ) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1 ) ) or not p <> 0. (TOP-REAL 2) or b1 . p = |[((p `1 ) / (sqrt (1 + (((p `1 ) / (p `2 )) ^2 )))),((p `2 ) / (sqrt (1 + (((p `1 ) / (p `2 )) ^2 ))))]| ) )
uniqueness
for b1, b2 being Function of the carrier of (TOP-REAL 2),the carrier of (TOP-REAL 2) st ( for p being Point of (TOP-REAL 2) holds
( ( p = 0. (TOP-REAL 2) implies b1 . p = p ) & ( ( ( p `2 <= p `1 & - (p `1 ) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1 ) ) ) & p <> 0. (TOP-REAL 2) implies b1 . p = |[((p `1 ) / (sqrt (1 + (((p `2 ) / (p `1 )) ^2 )))),((p `2 ) / (sqrt (1 + (((p `2 ) / (p `1 )) ^2 ))))]| ) & ( ( p `2 <= p `1 & - (p `1 ) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1 ) ) or not p <> 0. (TOP-REAL 2) or b1 . p = |[((p `1 ) / (sqrt (1 + (((p `1 ) / (p `2 )) ^2 )))),((p `2 ) / (sqrt (1 + (((p `1 ) / (p `2 )) ^2 ))))]| ) ) ) & ( for p being Point of (TOP-REAL 2) holds
( ( p = 0. (TOP-REAL 2) implies b2 . p = p ) & ( ( ( p `2 <= p `1 & - (p `1 ) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1 ) ) ) & p <> 0. (TOP-REAL 2) implies b2 . p = |[((p `1 ) / (sqrt (1 + (((p `2 ) / (p `1 )) ^2 )))),((p `2 ) / (sqrt (1 + (((p `2 ) / (p `1 )) ^2 ))))]| ) & ( ( p `2 <= p `1 & - (p `1 ) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1 ) ) or not p <> 0. (TOP-REAL 2) or b2 . p = |[((p `1 ) / (sqrt (1 + (((p `1 ) / (p `2 )) ^2 )))),((p `2 ) / (sqrt (1 + (((p `1 ) / (p `2 )) ^2 ))))]| ) ) ) holds
b1 = b2
end;
:: deftheorem Def1 defines Sq_Circ JGRAPH_3:def 1 :
theorem Th14:
theorem Th15:
theorem Th16:
theorem Th17:
theorem Th18:
theorem Th19:
theorem Th20:
Lm4:
for K1 being non empty Subset of (TOP-REAL 2)
for q being Point of ((TOP-REAL 2) | K1) holds (proj2 | K1) . q = proj2 . q
Lm5:
for K1 being non empty Subset of (TOP-REAL 2) holds proj2 | K1 is continuous Function of ((TOP-REAL 2) | K1),R^1
Lm6:
for K1 being non empty Subset of (TOP-REAL 2)
for q being Point of ((TOP-REAL 2) | K1) holds (proj1 | K1) . q = proj1 . q
Lm7:
for K1 being non empty Subset of (TOP-REAL 2) holds proj1 | K1 is continuous Function of ((TOP-REAL 2) | K1),R^1
theorem Th21:
theorem Th22:
theorem Th23:
theorem Th24:
Lm8:
0.REAL 2 = 0. (TOP-REAL 2)
by EUCLID:70;
Lm9:
( ( (1.REAL 2) `2 <= (1.REAL 2) `1 & - ((1.REAL 2) `1 ) <= (1.REAL 2) `2 ) or ( (1.REAL 2) `2 >= (1.REAL 2) `1 & (1.REAL 2) `2 <= - ((1.REAL 2) `1 ) ) )
by JGRAPH_2:13;
Lm10:
1.REAL 2 <> 0. (TOP-REAL 2)
by Lm8, REVROT_1:19;
Lm11:
for K1 being non empty Subset of (TOP-REAL 2) holds dom (proj2 * (Sq_Circ | K1)) = the carrier of ((TOP-REAL 2) | K1)
Lm12:
for K1 being non empty Subset of (TOP-REAL 2) holds dom (proj1 * (Sq_Circ | K1)) = the carrier of ((TOP-REAL 2) | K1)
Lm13:
NonZero (TOP-REAL 2) <> {}
by JGRAPH_2:19;
theorem Th25:
Lm14:
( ( (1.REAL 2) `1 <= (1.REAL 2) `2 & - ((1.REAL 2) `2 ) <= (1.REAL 2) `1 ) or ( (1.REAL 2) `1 >= (1.REAL 2) `2 & (1.REAL 2) `1 <= - ((1.REAL 2) `2 ) ) )
by JGRAPH_2:13;
Lm15:
1.REAL 2 <> 0. (TOP-REAL 2)
by Lm8, REVROT_1:19;
theorem Th26:
theorem Th27:
theorem Th28:
theorem Th29:
theorem Th30:
Lm16:
TopStruct(# the carrier of (TOP-REAL 2),the topology of (TOP-REAL 2) #) = TopSpaceMetr (Euclid 2)
by EUCLID:def 8;
theorem Th31:
theorem Th32:
theorem Th33:
theorem Th34:
theorem Th35:
theorem
begin
theorem
theorem Th38:
theorem Th39:
theorem Th40:
theorem Th41:
theorem Th42:
theorem Th43:
theorem Th44:
theorem Th45:
theorem Th46:
Lm17:
for K1 being non empty Subset of (TOP-REAL 2) holds proj2 * ((Sq_Circ " ) | K1) is Function of ((TOP-REAL 2) | K1),R^1
Lm18:
for K1 being non empty Subset of (TOP-REAL 2) holds proj1 * ((Sq_Circ " ) | K1) is Function of ((TOP-REAL 2) | K1),R^1
theorem Th47:
theorem Th48:
theorem Th49:
theorem Th50:
theorem Th51:
theorem Th52:
theorem
canceled;
theorem Th54:
theorem