environ
vocabularies HIDDEN, NUMBERS, SQUARE_1, ARYTM_3, XXREAL_0, CARD_1, RELAT_1, STRUCT_0, EUCLID, PRE_TOPC, COMPLEX1, MCART_1, FUNCT_1, XBOOLE_0, TARSKI, SUBSET_1, ORDINAL2, RCOMP_1, SUPINF_2, ARYTM_1, TOPMETR, REAL_1, XXREAL_1, JORDAN2C, FUNCT_4, PARTFUN1, PCOMPS_1, METRIC_1, TOPS_2, TOPREAL2, TOPREAL1, VALUED_1, BORSUK_1, JGRAPH_3, FUNCT_2;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, REAL_1, RLVECT_1, EUCLID, RELAT_1, TOPS_2, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, DOMAIN_1, STRUCT_0, TOPREAL1, TOPMETR, COMPTS_1, METRIC_1, RCOMP_1, SQUARE_1, PCOMPS_1, PSCOMP_1, PRE_TOPC, FUNCT_4, TOPREAL2, XXREAL_0;
definitions TARSKI, FUNCT_1, XBOOLE_0;
theorems TARSKI, RELAT_1, SUBSET_1, FUNCT_1, FUNCT_2, FUNCT_4, TOPS_1, TOPS_2, PARTFUN1, PRE_TOPC, REVROT_1, FRECHET, TOPMETR, JORDAN6, EUCLID, JGRAPH_1, SQUARE_1, TOPREAL3, PSCOMP_1, METRIC_1, SPPOL_2, JGRAPH_2, COMPTS_1, ZFMISC_1, GOBOARD6, TOPREAL1, TOPREAL2, COMPLEX1, XBOOLE_0, XBOOLE_1, XREAL_0, TOPRNS_1, XCMPLX_1, XREAL_1, XXREAL_0, XXREAL_1, RELSET_1;
schemes FUNCT_2, DOMAIN_1, JGRAPH_2, CLASSES1;
registrations FUNCT_1, RELSET_1, FUNCT_2, NUMBERS, XXREAL_0, XREAL_0, SQUARE_1, MEMBERED, STRUCT_0, PRE_TOPC, BORSUK_1, EUCLID, TOPMETR, TOPREAL1, TOPREAL2, BORSUK_3, ORDINAL1;
constructors HIDDEN, FUNCT_4, REAL_1, SQUARE_1, RCOMP_1, TOPS_2, COMPTS_1, TOPMETR, TOPREAL1, TOPREAL2, PSCOMP_1, FUNCSDOM, PCOMPS_1;
requirements HIDDEN, REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
equalities XBOOLE_0, SQUARE_1, STRUCT_0;
expansions TARSKI, FUNCT_1, XBOOLE_0;
Lm1:
for x being Real 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;
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
Lm8:
0.REAL 2 = 0. (TOP-REAL 2)
by EUCLID:66;
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:5;
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:9;
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:5;
Lm15:
1.REAL 2 <> 0. (TOP-REAL 2)
by Lm8, REVROT_1:19;
Lm16:
TopStruct(# the carrier of (TOP-REAL 2), the topology of (TOP-REAL 2) #) = TopSpaceMetr (Euclid 2)
by EUCLID:def 8;
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
Lm20:
now for px1 being Real holds
( not (px1 ^2) - 1 = 0 or px1 = 1 or px1 = - 1 )
let px1 be
Real;
( not (px1 ^2) - 1 = 0 or px1 = 1 or px1 = - 1 )assume
(px1 ^2) - 1
= 0
;
( px1 = 1 or px1 = - 1 )then
(px1 - 1) * (px1 + 1) = 0
;
then
(
px1 - 1
= 0 or
px1 + 1
= 0 )
by XCMPLX_1:6;
hence
(
px1 = 1 or
px1 = - 1 )
;
verum
end;