:: TOPALG_4 semantic presentation begin theorem :: TOPALG_4:1 (Bool "for" (Set (Var "G")) "," (Set (Var "H")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k2_group_7 :::"product"::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "G")) "," (Set (Var "H")) ($#k10_finseq_1 :::"*>"::: ) ) ")" ) (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G"))(Bool "ex" (Set (Var "h")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "H")) "st" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k5_group_7 :::"<*"::: ) (Set (Var "g")) "," (Set (Var "h")) ($#k5_group_7 :::"*>"::: ) )))))) ; definitionlet "G1", "G2", "H1", "H2" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "G1")) "," (Set (Const "H1")); let "g" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "G2")) "," (Set (Const "H2")); func :::"Gr2Iso"::: "(" "f" "," "g" ")" -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k2_group_7 :::"product"::: ) (Set ($#k10_finseq_1 :::"<*"::: ) "G1" "," "G2" ($#k10_finseq_1 :::"*>"::: ) ) ")" ) "," (Set "(" ($#k2_group_7 :::"product"::: ) (Set ($#k10_finseq_1 :::"<*"::: ) "H1" "," "H2" ($#k10_finseq_1 :::"*>"::: ) ) ")" ) means :: TOPALG_4:def 1 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k2_group_7 :::"product"::: ) (Set ($#k10_finseq_1 :::"<*"::: ) "G1" "," "G2" ($#k10_finseq_1 :::"*>"::: ) ) ")" ) (Bool "ex" (Set (Var "x1")) "being" ($#m1_subset_1 :::"Element":::) "of" "G1"(Bool "ex" (Set (Var "x2")) "being" ($#m1_subset_1 :::"Element":::) "of" "G2" "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k5_group_7 :::"<*"::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k5_group_7 :::"*>"::: ) )) & (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k5_group_7 :::"<*"::: ) (Set "(" "f" ($#k3_funct_2 :::"."::: ) (Set (Var "x1")) ")" ) "," (Set "(" "g" ($#k3_funct_2 :::"."::: ) (Set (Var "x2")) ")" ) ($#k5_group_7 :::"*>"::: ) )) ")" )))); end; :: deftheorem defines :::"Gr2Iso"::: TOPALG_4:def 1 : (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "," (Set (Var "H1")) "," (Set (Var "H2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "G1")) "," (Set (Var "H1")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "G2")) "," (Set (Var "H2")) (Bool "for" (Set (Var "b7")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k2_group_7 :::"product"::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "G1")) "," (Set (Var "G2")) ($#k10_finseq_1 :::"*>"::: ) ) ")" ) "," (Set "(" ($#k2_group_7 :::"product"::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "H1")) "," (Set (Var "H2")) ($#k10_finseq_1 :::"*>"::: ) ) ")" ) "holds" (Bool "(" (Bool (Set (Var "b7")) ($#r1_hidden :::"="::: ) (Set ($#k1_topalg_4 :::"Gr2Iso"::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" )) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k2_group_7 :::"product"::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "G1")) "," (Set (Var "G2")) ($#k10_finseq_1 :::"*>"::: ) ) ")" ) (Bool "ex" (Set (Var "x1")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G1"))(Bool "ex" (Set (Var "x2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G2")) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k5_group_7 :::"<*"::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k5_group_7 :::"*>"::: ) )) & (Bool (Set (Set (Var "b7")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k5_group_7 :::"<*"::: ) (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x1")) ")" ) "," (Set "(" (Set (Var "g")) ($#k3_funct_2 :::"."::: ) (Set (Var "x2")) ")" ) ($#k5_group_7 :::"*>"::: ) )) ")" )))) ")" ))))); theorem :: TOPALG_4:2 (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "," (Set (Var "H1")) "," (Set (Var "H2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "G1")) "," (Set (Var "H1")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "G2")) "," (Set (Var "H2")) (Bool "for" (Set (Var "x1")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G1")) (Bool "for" (Set (Var "x2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G2")) "holds" (Bool (Set (Set "(" ($#k1_topalg_4 :::"Gr2Iso"::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set ($#k5_group_7 :::"<*"::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k5_group_7 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k5_group_7 :::"<*"::: ) (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x1")) ")" ) "," (Set "(" (Set (Var "g")) ($#k3_funct_2 :::"."::: ) (Set (Var "x2")) ")" ) ($#k5_group_7 :::"*>"::: ) ))))))) ; registrationlet "G1", "G2", "H1", "H2" be ($#l3_algstr_0 :::"Group":::); let "f" be ($#m1_subset_1 :::"Homomorphism":::) "of" (Set (Const "G1")) "," (Set (Const "H1")); let "g" be ($#m1_subset_1 :::"Homomorphism":::) "of" (Set (Const "G2")) "," (Set (Const "H2")); cluster (Set ($#k1_topalg_4 :::"Gr2Iso"::: ) "(" "f" "," "g" ")" ) -> ($#v1_group_6 :::"multiplicative"::: ) ; end; theorem :: TOPALG_4:3 (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "," (Set (Var "H1")) "," (Set (Var "H2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "G1")) "," (Set (Var "H1")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "G2")) "," (Set (Var "H2")) "st" (Bool (Bool (Set (Var "f")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool (Set (Var "g")) "is" ($#v2_funct_1 :::"one-to-one"::: ) )) "holds" (Bool (Set ($#k1_topalg_4 :::"Gr2Iso"::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ) "is" ($#v2_funct_1 :::"one-to-one"::: ) )))) ; theorem :: TOPALG_4:4 (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "," (Set (Var "H1")) "," (Set (Var "H2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "G1")) "," (Set (Var "H1")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "G2")) "," (Set (Var "H2")) "st" (Bool (Bool (Set (Var "f")) "is" ($#v2_funct_2 :::"onto"::: ) ) & (Bool (Set (Var "g")) "is" ($#v2_funct_2 :::"onto"::: ) )) "holds" (Bool (Set ($#k1_topalg_4 :::"Gr2Iso"::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ) "is" ($#v2_funct_2 :::"onto"::: ) )))) ; theorem :: TOPALG_4:5 (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "," (Set (Var "H1")) "," (Set (Var "H2")) "being" ($#l3_algstr_0 :::"Group":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Homomorphism":::) "of" (Set (Var "G1")) "," (Set (Var "H1")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Homomorphism":::) "of" (Set (Var "G2")) "," (Set (Var "H2")) "st" (Bool (Bool (Set (Var "f")) "is" ($#v3_funct_2 :::"bijective"::: ) ) & (Bool (Set (Var "g")) "is" ($#v3_funct_2 :::"bijective"::: ) )) "holds" (Bool (Set ($#k1_topalg_4 :::"Gr2Iso"::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ) "is" ($#v3_funct_2 :::"bijective"::: ) )))) ; theorem :: TOPALG_4:6 (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "," (Set (Var "H1")) "," (Set (Var "H2")) "being" ($#l3_algstr_0 :::"Group":::) "st" (Bool (Bool (Set (Var "G1")) "," (Set (Var "H1")) ($#r1_group_6 :::"are_isomorphic"::: ) ) & (Bool (Set (Var "G2")) "," (Set (Var "H2")) ($#r1_group_6 :::"are_isomorphic"::: ) )) "holds" (Bool (Set ($#k2_group_7 :::"product"::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "G1")) "," (Set (Var "G2")) ($#k10_finseq_1 :::"*>"::: ) )) "," (Set ($#k2_group_7 :::"product"::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "H1")) "," (Set (Var "H2")) ($#k10_finseq_1 :::"*>"::: ) )) ($#r2_group_6 :::"are_isomorphic"::: ) )) ; begin theorem :: TOPALG_4:7 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "g"))))) "holds" (Bool (Set ($#k11_mcart_1 :::"pr1"::: ) (Set ($#k13_funct_3 :::"<:"::: ) (Set (Var "f")) "," (Set (Var "g")) ($#k13_funct_3 :::":>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "f")))) ; theorem :: TOPALG_4:8 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "g"))))) "holds" (Bool (Set ($#k12_mcart_1 :::"pr2"::: ) (Set ($#k13_funct_3 :::"<:"::: ) (Set (Var "f")) "," (Set (Var "g")) ($#k13_funct_3 :::":>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "g")))) ; definitionlet "S", "T", "Y" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "Y")) "," (Set (Const "S")); let "g" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "Y")) "," (Set (Const "T")); :: original: :::"<:"::: redefine func :::"<:":::"f" "," "g":::":>"::: -> ($#m1_subset_1 :::"Function":::) "of" "Y" "," (Set ($#k2_borsuk_1 :::"[:"::: ) "S" "," "T" ($#k2_borsuk_1 :::":]"::: ) ); end; definitionlet "S", "T", "Y" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "Y")) "," (Set ($#k2_borsuk_1 :::"[:"::: ) (Set (Const "S")) "," (Set (Const "T")) ($#k2_borsuk_1 :::":]"::: ) ); :: original: :::"pr1"::: redefine func :::"pr1"::: "f" -> ($#m1_subset_1 :::"Function":::) "of" "Y" "," "S"; :: original: :::"pr2"::: redefine func :::"pr2"::: "f" -> ($#m1_subset_1 :::"Function":::) "of" "Y" "," "T"; end; theorem :: TOPALG_4:9 (Bool "for" (Set (Var "Y")) "," (Set (Var "S")) "," (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "f")) "being" ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set ($#k2_borsuk_1 :::"[:"::: ) (Set (Var "S")) "," (Set (Var "T")) ($#k2_borsuk_1 :::":]"::: ) ) "holds" (Bool (Set ($#k3_topalg_4 :::"pr1"::: ) (Set (Var "f"))) "is" ($#v5_pre_topc :::"continuous"::: ) ))) ; theorem :: TOPALG_4:10 (Bool "for" (Set (Var "Y")) "," (Set (Var "S")) "," (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "f")) "being" ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set ($#k2_borsuk_1 :::"[:"::: ) (Set (Var "S")) "," (Set (Var "T")) ($#k2_borsuk_1 :::":]"::: ) ) "holds" (Bool (Set ($#k4_topalg_4 :::"pr2"::: ) (Set (Var "f"))) "is" ($#v5_pre_topc :::"continuous"::: ) ))) ; theorem :: TOPALG_4:11 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "s1")) "," (Set (Var "s2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "t1")) "," (Set (Var "t2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set ($#k4_borsuk_1 :::"["::: ) (Set (Var "s1")) "," (Set (Var "t1")) ($#k4_borsuk_1 :::"]"::: ) ) "," (Set ($#k4_borsuk_1 :::"["::: ) (Set (Var "s2")) "," (Set (Var "t2")) ($#k4_borsuk_1 :::"]"::: ) ) ($#r1_borsuk_6 :::"are_connected"::: ) )) "holds" (Bool (Set (Var "s1")) "," (Set (Var "s2")) ($#r1_borsuk_6 :::"are_connected"::: ) )))) ; theorem :: TOPALG_4:12 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "s1")) "," (Set (Var "s2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "t1")) "," (Set (Var "t2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set ($#k4_borsuk_1 :::"["::: ) (Set (Var "s1")) "," (Set (Var "t1")) ($#k4_borsuk_1 :::"]"::: ) ) "," (Set ($#k4_borsuk_1 :::"["::: ) (Set (Var "s2")) "," (Set (Var "t2")) ($#k4_borsuk_1 :::"]"::: ) ) ($#r1_borsuk_6 :::"are_connected"::: ) )) "holds" (Bool (Set (Var "t1")) "," (Set (Var "t2")) ($#r1_borsuk_6 :::"are_connected"::: ) )))) ; theorem :: TOPALG_4:13 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "s1")) "," (Set (Var "s2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "t1")) "," (Set (Var "t2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set ($#k4_borsuk_1 :::"["::: ) (Set (Var "s1")) "," (Set (Var "t1")) ($#k4_borsuk_1 :::"]"::: ) ) "," (Set ($#k4_borsuk_1 :::"["::: ) (Set (Var "s2")) "," (Set (Var "t2")) ($#k4_borsuk_1 :::"]"::: ) ) ($#r1_borsuk_6 :::"are_connected"::: ) )) "holds" (Bool "for" (Set (Var "L")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set ($#k4_borsuk_1 :::"["::: ) (Set (Var "s1")) "," (Set (Var "t1")) ($#k4_borsuk_1 :::"]"::: ) ) "," (Set ($#k4_borsuk_1 :::"["::: ) (Set (Var "s2")) "," (Set (Var "t2")) ($#k4_borsuk_1 :::"]"::: ) ) "holds" (Bool (Set ($#k3_topalg_4 :::"pr1"::: ) (Set (Var "L"))) "is" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "s1")) "," (Set (Var "s2"))))))) ; theorem :: TOPALG_4:14 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "s1")) "," (Set (Var "s2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "t1")) "," (Set (Var "t2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set ($#k4_borsuk_1 :::"["::: ) (Set (Var "s1")) "," (Set (Var "t1")) ($#k4_borsuk_1 :::"]"::: ) ) "," (Set ($#k4_borsuk_1 :::"["::: ) (Set (Var "s2")) "," (Set (Var "t2")) ($#k4_borsuk_1 :::"]"::: ) ) ($#r1_borsuk_6 :::"are_connected"::: ) )) "holds" (Bool "for" (Set (Var "L")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set ($#k4_borsuk_1 :::"["::: ) (Set (Var "s1")) "," (Set (Var "t1")) ($#k4_borsuk_1 :::"]"::: ) ) "," (Set ($#k4_borsuk_1 :::"["::: ) (Set (Var "s2")) "," (Set (Var "t2")) ($#k4_borsuk_1 :::"]"::: ) ) "holds" (Bool (Set ($#k4_topalg_4 :::"pr2"::: ) (Set (Var "L"))) "is" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "t1")) "," (Set (Var "t2"))))))) ; theorem :: TOPALG_4:15 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "s1")) "," (Set (Var "s2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "t1")) "," (Set (Var "t2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "s1")) "," (Set (Var "s2")) ($#r1_borsuk_6 :::"are_connected"::: ) ) & (Bool (Set (Var "t1")) "," (Set (Var "t2")) ($#r1_borsuk_6 :::"are_connected"::: ) )) "holds" (Bool (Set ($#k4_borsuk_1 :::"["::: ) (Set (Var "s1")) "," (Set (Var "t1")) ($#k4_borsuk_1 :::"]"::: ) ) "," (Set ($#k4_borsuk_1 :::"["::: ) (Set (Var "s2")) "," (Set (Var "t2")) ($#k4_borsuk_1 :::"]"::: ) ) ($#r1_borsuk_6 :::"are_connected"::: ) )))) ; theorem :: TOPALG_4:16 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "s1")) "," (Set (Var "s2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "t1")) "," (Set (Var "t2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "s1")) "," (Set (Var "s2")) ($#r1_borsuk_6 :::"are_connected"::: ) ) & (Bool (Set (Var "t1")) "," (Set (Var "t2")) ($#r1_borsuk_6 :::"are_connected"::: ) )) "holds" (Bool "for" (Set (Var "L1")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "s1")) "," (Set (Var "s2")) (Bool "for" (Set (Var "L2")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "t1")) "," (Set (Var "t2")) "holds" (Bool (Set ($#k2_topalg_4 :::"<:"::: ) (Set (Var "L1")) "," (Set (Var "L2")) ($#k2_topalg_4 :::":>"::: ) ) "is" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set ($#k4_borsuk_1 :::"["::: ) (Set (Var "s1")) "," (Set (Var "t1")) ($#k4_borsuk_1 :::"]"::: ) ) "," (Set ($#k4_borsuk_1 :::"["::: ) (Set (Var "s2")) "," (Set (Var "t2")) ($#k4_borsuk_1 :::"]"::: ) ))))))) ; definitionlet "S", "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_borsuk_2 :::"pathwise_connected"::: ) ($#l1_pre_topc :::"TopSpace":::); let "s1", "s2" be ($#m1_subset_1 :::"Point":::) "of" (Set (Const "S")); let "t1", "t2" be ($#m1_subset_1 :::"Point":::) "of" (Set (Const "T")); let "L1" be ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Const "s1")) "," (Set (Const "s2")); let "L2" be ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Const "t1")) "," (Set (Const "t2")); :: original: :::"<:"::: redefine func :::"<:":::"L1" "," "L2":::":>"::: -> ($#m1_borsuk_2 :::"Path"::: ) "of" (Set ($#k4_borsuk_1 :::"["::: ) "s1" "," "t1" ($#k4_borsuk_1 :::"]"::: ) ) "," (Set ($#k4_borsuk_1 :::"["::: ) "s2" "," "t2" ($#k4_borsuk_1 :::"]"::: ) ); end; definitionlet "S", "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); let "s" be ($#m1_subset_1 :::"Point":::) "of" (Set (Const "S")); let "t" be ($#m1_subset_1 :::"Point":::) "of" (Set (Const "T")); let "L1" be ($#m1_borsuk_2 :::"Loop":::) "of" (Set (Const "s")); let "L2" be ($#m1_borsuk_2 :::"Loop":::) "of" (Set (Const "t")); :: original: :::"<:"::: redefine func :::"<:":::"L1" "," "L2":::":>"::: -> ($#m1_borsuk_2 :::"Loop":::) "of" (Set ($#k4_borsuk_1 :::"["::: ) "s" "," "t" ($#k4_borsuk_1 :::"]"::: ) ); end; registrationlet "S", "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_borsuk_2 :::"pathwise_connected"::: ) ($#l1_pre_topc :::"TopSpace":::); cluster (Set ($#k2_borsuk_1 :::"[:"::: ) "S" "," "T" ($#k2_borsuk_1 :::":]"::: ) ) -> ($#v1_borsuk_2 :::"pathwise_connected"::: ) ; end; definitionlet "S", "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_borsuk_2 :::"pathwise_connected"::: ) ($#l1_pre_topc :::"TopSpace":::); let "s1", "s2" be ($#m1_subset_1 :::"Point":::) "of" (Set (Const "S")); let "t1", "t2" be ($#m1_subset_1 :::"Point":::) "of" (Set (Const "T")); let "L" be ($#m1_borsuk_2 :::"Path"::: ) "of" (Set ($#k4_borsuk_1 :::"["::: ) (Set (Const "s1")) "," (Set (Const "t1")) ($#k4_borsuk_1 :::"]"::: ) ) "," (Set ($#k4_borsuk_1 :::"["::: ) (Set (Const "s2")) "," (Set (Const "t2")) ($#k4_borsuk_1 :::"]"::: ) ); :: original: :::"pr1"::: redefine func :::"pr1"::: "L" -> ($#m1_borsuk_2 :::"Path"::: ) "of" "s1" "," "s2"; :: original: :::"pr2"::: redefine func :::"pr2"::: "L" -> ($#m1_borsuk_2 :::"Path"::: ) "of" "t1" "," "t2"; end; definitionlet "S", "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); let "s" be ($#m1_subset_1 :::"Point":::) "of" (Set (Const "S")); let "t" be ($#m1_subset_1 :::"Point":::) "of" (Set (Const "T")); let "L" be ($#m1_borsuk_2 :::"Loop":::) "of" (Set ($#k4_borsuk_1 :::"["::: ) (Set (Const "s")) "," (Set (Const "t")) ($#k4_borsuk_1 :::"]"::: ) ); :: original: :::"pr1"::: redefine func :::"pr1"::: "L" -> ($#m1_borsuk_2 :::"Loop":::) "of" "s"; :: original: :::"pr2"::: redefine func :::"pr2"::: "L" -> ($#m1_borsuk_2 :::"Loop":::) "of" "t"; end; theorem :: TOPALG_4:17 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "s1")) "," (Set (Var "s2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "t1")) "," (Set (Var "t2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "l1")) "," (Set (Var "l2")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set ($#k4_borsuk_1 :::"["::: ) (Set (Var "s1")) "," (Set (Var "t1")) ($#k4_borsuk_1 :::"]"::: ) ) "," (Set ($#k4_borsuk_1 :::"["::: ) (Set (Var "s2")) "," (Set (Var "t2")) ($#k4_borsuk_1 :::"]"::: ) ) (Bool "for" (Set (Var "H")) "being" ($#m1_borsuk_6 :::"Homotopy"::: ) "of" (Set (Var "l1")) "," (Set (Var "l2")) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "s1")) "," (Set (Var "s2")) "st" (Bool (Bool (Set (Var "p")) ($#r2_funct_2 :::"="::: ) (Set ($#k3_topalg_4 :::"pr1"::: ) (Set (Var "l1")))) & (Bool (Set (Var "q")) ($#r2_funct_2 :::"="::: ) (Set ($#k3_topalg_4 :::"pr1"::: ) (Set (Var "l2")))) & (Bool (Set (Var "l1")) "," (Set (Var "l2")) ($#r3_borsuk_2 :::"are_homotopic"::: ) )) "holds" (Bool (Set ($#k3_topalg_4 :::"pr1"::: ) (Set (Var "H"))) "is" ($#m1_borsuk_6 :::"Homotopy"::: ) "of" (Set (Var "p")) "," (Set (Var "q"))))))))) ; theorem :: TOPALG_4:18 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "s1")) "," (Set (Var "s2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "t1")) "," (Set (Var "t2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "l1")) "," (Set (Var "l2")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set ($#k4_borsuk_1 :::"["::: ) (Set (Var "s1")) "," (Set (Var "t1")) ($#k4_borsuk_1 :::"]"::: ) ) "," (Set ($#k4_borsuk_1 :::"["::: ) (Set (Var "s2")) "," (Set (Var "t2")) ($#k4_borsuk_1 :::"]"::: ) ) (Bool "for" (Set (Var "H")) "being" ($#m1_borsuk_6 :::"Homotopy"::: ) "of" (Set (Var "l1")) "," (Set (Var "l2")) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "t1")) "," (Set (Var "t2")) "st" (Bool (Bool (Set (Var "p")) ($#r2_funct_2 :::"="::: ) (Set ($#k4_topalg_4 :::"pr2"::: ) (Set (Var "l1")))) & (Bool (Set (Var "q")) ($#r2_funct_2 :::"="::: ) (Set ($#k4_topalg_4 :::"pr2"::: ) (Set (Var "l2")))) & (Bool (Set (Var "l1")) "," (Set (Var "l2")) ($#r3_borsuk_2 :::"are_homotopic"::: ) )) "holds" (Bool (Set ($#k4_topalg_4 :::"pr2"::: ) (Set (Var "H"))) "is" ($#m1_borsuk_6 :::"Homotopy"::: ) "of" (Set (Var "p")) "," (Set (Var "q"))))))))) ; theorem :: TOPALG_4:19 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "s1")) "," (Set (Var "s2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "t1")) "," (Set (Var "t2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "l1")) "," (Set (Var "l2")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set ($#k4_borsuk_1 :::"["::: ) (Set (Var "s1")) "," (Set (Var "t1")) ($#k4_borsuk_1 :::"]"::: ) ) "," (Set ($#k4_borsuk_1 :::"["::: ) (Set (Var "s2")) "," (Set (Var "t2")) ($#k4_borsuk_1 :::"]"::: ) ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "s1")) "," (Set (Var "s2")) "st" (Bool (Bool (Set (Var "p")) ($#r2_funct_2 :::"="::: ) (Set ($#k3_topalg_4 :::"pr1"::: ) (Set (Var "l1")))) & (Bool (Set (Var "q")) ($#r2_funct_2 :::"="::: ) (Set ($#k3_topalg_4 :::"pr1"::: ) (Set (Var "l2")))) & (Bool (Set (Var "l1")) "," (Set (Var "l2")) ($#r3_borsuk_2 :::"are_homotopic"::: ) )) "holds" (Bool (Set (Var "p")) "," (Set (Var "q")) ($#r3_borsuk_2 :::"are_homotopic"::: ) )))))) ; theorem :: TOPALG_4:20 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "s1")) "," (Set (Var "s2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "t1")) "," (Set (Var "t2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "l1")) "," (Set (Var "l2")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set ($#k4_borsuk_1 :::"["::: ) (Set (Var "s1")) "," (Set (Var "t1")) ($#k4_borsuk_1 :::"]"::: ) ) "," (Set ($#k4_borsuk_1 :::"["::: ) (Set (Var "s2")) "," (Set (Var "t2")) ($#k4_borsuk_1 :::"]"::: ) ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "t1")) "," (Set (Var "t2")) "st" (Bool (Bool (Set (Var "p")) ($#r2_funct_2 :::"="::: ) (Set ($#k4_topalg_4 :::"pr2"::: ) (Set (Var "l1")))) & (Bool (Set (Var "q")) ($#r2_funct_2 :::"="::: ) (Set ($#k4_topalg_4 :::"pr2"::: ) (Set (Var "l2")))) & (Bool (Set (Var "l1")) "," (Set (Var "l2")) ($#r3_borsuk_2 :::"are_homotopic"::: ) )) "holds" (Bool (Set (Var "p")) "," (Set (Var "q")) ($#r3_borsuk_2 :::"are_homotopic"::: ) )))))) ; theorem :: TOPALG_4:21 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "s1")) "," (Set (Var "s2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "t1")) "," (Set (Var "t2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "l1")) "," (Set (Var "l2")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set ($#k4_borsuk_1 :::"["::: ) (Set (Var "s1")) "," (Set (Var "t1")) ($#k4_borsuk_1 :::"]"::: ) ) "," (Set ($#k4_borsuk_1 :::"["::: ) (Set (Var "s2")) "," (Set (Var "t2")) ($#k4_borsuk_1 :::"]"::: ) ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "s1")) "," (Set (Var "s2")) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "t1")) "," (Set (Var "t2")) (Bool "for" (Set (Var "f")) "being" ($#m1_borsuk_6 :::"Homotopy"::: ) "of" (Set (Var "p")) "," (Set (Var "q")) (Bool "for" (Set (Var "g")) "being" ($#m1_borsuk_6 :::"Homotopy"::: ) "of" (Set (Var "x")) "," (Set (Var "y")) "st" (Bool (Bool (Set (Var "p")) ($#r2_funct_2 :::"="::: ) (Set ($#k3_topalg_4 :::"pr1"::: ) (Set (Var "l1")))) & (Bool (Set (Var "q")) ($#r2_funct_2 :::"="::: ) (Set ($#k3_topalg_4 :::"pr1"::: ) (Set (Var "l2")))) & (Bool (Set (Var "x")) ($#r2_funct_2 :::"="::: ) (Set ($#k4_topalg_4 :::"pr2"::: ) (Set (Var "l1")))) & (Bool (Set (Var "y")) ($#r2_funct_2 :::"="::: ) (Set ($#k4_topalg_4 :::"pr2"::: ) (Set (Var "l2")))) & (Bool (Set (Var "p")) "," (Set (Var "q")) ($#r3_borsuk_2 :::"are_homotopic"::: ) ) & (Bool (Set (Var "x")) "," (Set (Var "y")) ($#r3_borsuk_2 :::"are_homotopic"::: ) )) "holds" (Bool (Set ($#k2_topalg_4 :::"<:"::: ) (Set (Var "f")) "," (Set (Var "g")) ($#k2_topalg_4 :::":>"::: ) ) "is" ($#m1_borsuk_6 :::"Homotopy"::: ) "of" (Set (Var "l1")) "," (Set (Var "l2"))))))))))) ; theorem :: TOPALG_4:22 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "s1")) "," (Set (Var "s2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "t1")) "," (Set (Var "t2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "l1")) "," (Set (Var "l2")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set ($#k4_borsuk_1 :::"["::: ) (Set (Var "s1")) "," (Set (Var "t1")) ($#k4_borsuk_1 :::"]"::: ) ) "," (Set ($#k4_borsuk_1 :::"["::: ) (Set (Var "s2")) "," (Set (Var "t2")) ($#k4_borsuk_1 :::"]"::: ) ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "s1")) "," (Set (Var "s2")) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "t1")) "," (Set (Var "t2")) "st" (Bool (Bool (Set (Var "p")) ($#r2_funct_2 :::"="::: ) (Set ($#k3_topalg_4 :::"pr1"::: ) (Set (Var "l1")))) & (Bool (Set (Var "q")) ($#r2_funct_2 :::"="::: ) (Set ($#k3_topalg_4 :::"pr1"::: ) (Set (Var "l2")))) & (Bool (Set (Var "x")) ($#r2_funct_2 :::"="::: ) (Set ($#k4_topalg_4 :::"pr2"::: ) (Set (Var "l1")))) & (Bool (Set (Var "y")) ($#r2_funct_2 :::"="::: ) (Set ($#k4_topalg_4 :::"pr2"::: ) (Set (Var "l2")))) & (Bool (Set (Var "p")) "," (Set (Var "q")) ($#r3_borsuk_2 :::"are_homotopic"::: ) ) & (Bool (Set (Var "x")) "," (Set (Var "y")) ($#r3_borsuk_2 :::"are_homotopic"::: ) )) "holds" (Bool (Set (Var "l1")) "," (Set (Var "l2")) ($#r3_borsuk_2 :::"are_homotopic"::: ) ))))))) ; theorem :: TOPALG_4:23 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "s1")) "," (Set (Var "s2")) "," (Set (Var "s3")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "t1")) "," (Set (Var "t2")) "," (Set (Var "t3")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "l1")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set ($#k4_borsuk_1 :::"["::: ) (Set (Var "s1")) "," (Set (Var "t1")) ($#k4_borsuk_1 :::"]"::: ) ) "," (Set ($#k4_borsuk_1 :::"["::: ) (Set (Var "s2")) "," (Set (Var "t2")) ($#k4_borsuk_1 :::"]"::: ) ) (Bool "for" (Set (Var "l2")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set ($#k4_borsuk_1 :::"["::: ) (Set (Var "s2")) "," (Set (Var "t2")) ($#k4_borsuk_1 :::"]"::: ) ) "," (Set ($#k4_borsuk_1 :::"["::: ) (Set (Var "s3")) "," (Set (Var "t3")) ($#k4_borsuk_1 :::"]"::: ) ) (Bool "for" (Set (Var "p1")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "s1")) "," (Set (Var "s2")) (Bool "for" (Set (Var "p2")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "s2")) "," (Set (Var "s3")) "st" (Bool (Bool (Set ($#k4_borsuk_1 :::"["::: ) (Set (Var "s1")) "," (Set (Var "t1")) ($#k4_borsuk_1 :::"]"::: ) ) "," (Set ($#k4_borsuk_1 :::"["::: ) (Set (Var "s2")) "," (Set (Var "t2")) ($#k4_borsuk_1 :::"]"::: ) ) ($#r1_borsuk_6 :::"are_connected"::: ) ) & (Bool (Set ($#k4_borsuk_1 :::"["::: ) (Set (Var "s2")) "," (Set (Var "t2")) ($#k4_borsuk_1 :::"]"::: ) ) "," (Set ($#k4_borsuk_1 :::"["::: ) (Set (Var "s3")) "," (Set (Var "t3")) ($#k4_borsuk_1 :::"]"::: ) ) ($#r1_borsuk_6 :::"are_connected"::: ) ) & (Bool (Set (Var "p1")) ($#r2_funct_2 :::"="::: ) (Set ($#k3_topalg_4 :::"pr1"::: ) (Set (Var "l1")))) & (Bool (Set (Var "p2")) ($#r2_funct_2 :::"="::: ) (Set ($#k3_topalg_4 :::"pr1"::: ) (Set (Var "l2"))))) "holds" (Bool (Set ($#k3_topalg_4 :::"pr1"::: ) (Set "(" (Set (Var "l1")) ($#k1_borsuk_2 :::"+"::: ) (Set (Var "l2")) ")" )) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "p1")) ($#k1_borsuk_2 :::"+"::: ) (Set (Var "p2"))))))))))) ; theorem :: TOPALG_4:24 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_borsuk_2 :::"pathwise_connected"::: ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "s1")) "," (Set (Var "s2")) "," (Set (Var "s3")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "t1")) "," (Set (Var "t2")) "," (Set (Var "t3")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "l1")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set ($#k4_borsuk_1 :::"["::: ) (Set (Var "s1")) "," (Set (Var "t1")) ($#k4_borsuk_1 :::"]"::: ) ) "," (Set ($#k4_borsuk_1 :::"["::: ) (Set (Var "s2")) "," (Set (Var "t2")) ($#k4_borsuk_1 :::"]"::: ) ) (Bool "for" (Set (Var "l2")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set ($#k4_borsuk_1 :::"["::: ) (Set (Var "s2")) "," (Set (Var "t2")) ($#k4_borsuk_1 :::"]"::: ) ) "," (Set ($#k4_borsuk_1 :::"["::: ) (Set (Var "s3")) "," (Set (Var "t3")) ($#k4_borsuk_1 :::"]"::: ) ) "holds" (Bool (Set ($#k7_topalg_4 :::"pr1"::: ) (Set "(" (Set (Var "l1")) ($#k1_borsuk_2 :::"+"::: ) (Set (Var "l2")) ")" )) ($#r2_funct_2 :::"="::: ) (Set (Set "(" ($#k7_topalg_4 :::"pr1"::: ) (Set (Var "l1")) ")" ) ($#k1_borsuk_2 :::"+"::: ) (Set "(" ($#k7_topalg_4 :::"pr1"::: ) (Set (Var "l2")) ")" )))))))) ; theorem :: TOPALG_4:25 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "s1")) "," (Set (Var "s2")) "," (Set (Var "s3")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "t1")) "," (Set (Var "t2")) "," (Set (Var "t3")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "l1")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set ($#k4_borsuk_1 :::"["::: ) (Set (Var "s1")) "," (Set (Var "t1")) ($#k4_borsuk_1 :::"]"::: ) ) "," (Set ($#k4_borsuk_1 :::"["::: ) (Set (Var "s2")) "," (Set (Var "t2")) ($#k4_borsuk_1 :::"]"::: ) ) (Bool "for" (Set (Var "l2")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set ($#k4_borsuk_1 :::"["::: ) (Set (Var "s2")) "," (Set (Var "t2")) ($#k4_borsuk_1 :::"]"::: ) ) "," (Set ($#k4_borsuk_1 :::"["::: ) (Set (Var "s3")) "," (Set (Var "t3")) ($#k4_borsuk_1 :::"]"::: ) ) (Bool "for" (Set (Var "p1")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "t1")) "," (Set (Var "t2")) (Bool "for" (Set (Var "p2")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "t2")) "," (Set (Var "t3")) "st" (Bool (Bool (Set ($#k4_borsuk_1 :::"["::: ) (Set (Var "s1")) "," (Set (Var "t1")) ($#k4_borsuk_1 :::"]"::: ) ) "," (Set ($#k4_borsuk_1 :::"["::: ) (Set (Var "s2")) "," (Set (Var "t2")) ($#k4_borsuk_1 :::"]"::: ) ) ($#r1_borsuk_6 :::"are_connected"::: ) ) & (Bool (Set ($#k4_borsuk_1 :::"["::: ) (Set (Var "s2")) "," (Set (Var "t2")) ($#k4_borsuk_1 :::"]"::: ) ) "," (Set ($#k4_borsuk_1 :::"["::: ) (Set (Var "s3")) "," (Set (Var "t3")) ($#k4_borsuk_1 :::"]"::: ) ) ($#r1_borsuk_6 :::"are_connected"::: ) ) & (Bool (Set (Var "p1")) ($#r2_funct_2 :::"="::: ) (Set ($#k4_topalg_4 :::"pr2"::: ) (Set (Var "l1")))) & (Bool (Set (Var "p2")) ($#r2_funct_2 :::"="::: ) (Set ($#k4_topalg_4 :::"pr2"::: ) (Set (Var "l2"))))) "holds" (Bool (Set ($#k4_topalg_4 :::"pr2"::: ) (Set "(" (Set (Var "l1")) ($#k1_borsuk_2 :::"+"::: ) (Set (Var "l2")) ")" )) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "p1")) ($#k1_borsuk_2 :::"+"::: ) (Set (Var "p2"))))))))))) ; theorem :: TOPALG_4:26 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_borsuk_2 :::"pathwise_connected"::: ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "s1")) "," (Set (Var "s2")) "," (Set (Var "s3")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "t1")) "," (Set (Var "t2")) "," (Set (Var "t3")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "l1")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set ($#k4_borsuk_1 :::"["::: ) (Set (Var "s1")) "," (Set (Var "t1")) ($#k4_borsuk_1 :::"]"::: ) ) "," (Set ($#k4_borsuk_1 :::"["::: ) (Set (Var "s2")) "," (Set (Var "t2")) ($#k4_borsuk_1 :::"]"::: ) ) (Bool "for" (Set (Var "l2")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set ($#k4_borsuk_1 :::"["::: ) (Set (Var "s2")) "," (Set (Var "t2")) ($#k4_borsuk_1 :::"]"::: ) ) "," (Set ($#k4_borsuk_1 :::"["::: ) (Set (Var "s3")) "," (Set (Var "t3")) ($#k4_borsuk_1 :::"]"::: ) ) "holds" (Bool (Set ($#k8_topalg_4 :::"pr2"::: ) (Set "(" (Set (Var "l1")) ($#k1_borsuk_2 :::"+"::: ) (Set (Var "l2")) ")" )) ($#r2_funct_2 :::"="::: ) (Set (Set "(" ($#k8_topalg_4 :::"pr2"::: ) (Set (Var "l1")) ")" ) ($#k1_borsuk_2 :::"+"::: ) (Set "(" ($#k8_topalg_4 :::"pr2"::: ) (Set (Var "l2")) ")" )))))))) ; definitionlet "S", "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); let "s" be ($#m1_subset_1 :::"Point":::) "of" (Set (Const "S")); let "t" be ($#m1_subset_1 :::"Point":::) "of" (Set (Const "T")); func :::"FGPrIso"::: "(" "s" "," "t" ")" -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k5_topalg_1 :::"pi_1"::: ) "(" (Set ($#k2_borsuk_1 :::"[:"::: ) "S" "," "T" ($#k2_borsuk_1 :::":]"::: ) ) "," (Set ($#k4_borsuk_1 :::"["::: ) "s" "," "t" ($#k4_borsuk_1 :::"]"::: ) ) ")" ")" ) "," (Set "(" ($#k2_group_7 :::"product"::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set "(" ($#k5_topalg_1 :::"pi_1"::: ) "(" "S" "," "s" ")" ")" ) "," (Set "(" ($#k5_topalg_1 :::"pi_1"::: ) "(" "T" "," "t" ")" ")" ) ($#k10_finseq_1 :::"*>"::: ) ) ")" ) means :: TOPALG_4:def 2 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k5_topalg_1 :::"pi_1"::: ) "(" (Set ($#k2_borsuk_1 :::"[:"::: ) "S" "," "T" ($#k2_borsuk_1 :::":]"::: ) ) "," (Set ($#k4_borsuk_1 :::"["::: ) "s" "," "t" ($#k4_borsuk_1 :::"]"::: ) ) ")" ")" ) (Bool "ex" (Set (Var "l")) "being" ($#m1_borsuk_2 :::"Loop":::) "of" (Set ($#k4_borsuk_1 :::"["::: ) "s" "," "t" ($#k4_borsuk_1 :::"]"::: ) ) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set "(" ($#k4_topalg_1 :::"EqRel"::: ) "(" (Set ($#k2_borsuk_1 :::"[:"::: ) "S" "," "T" ($#k2_borsuk_1 :::":]"::: ) ) "," (Set ($#k4_borsuk_1 :::"["::: ) "s" "," "t" ($#k4_borsuk_1 :::"]"::: ) ) ")" ")" ) "," (Set (Var "l")) ")" )) & (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set "(" ($#k6_eqrel_1 :::"Class"::: ) "(" (Set "(" ($#k4_topalg_1 :::"EqRel"::: ) "(" "S" "," "s" ")" ")" ) "," (Set "(" ($#k9_topalg_4 :::"pr1"::: ) (Set (Var "l")) ")" ) ")" ")" ) "," (Set "(" ($#k6_eqrel_1 :::"Class"::: ) "(" (Set "(" ($#k4_topalg_1 :::"EqRel"::: ) "(" "T" "," "t" ")" ")" ) "," (Set "(" ($#k10_topalg_4 :::"pr2"::: ) (Set (Var "l")) ")" ) ")" ")" ) ($#k10_finseq_1 :::"*>"::: ) )) ")" ))); end; :: deftheorem defines :::"FGPrIso"::: TOPALG_4:def 2 : (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "t")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "b5")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k5_topalg_1 :::"pi_1"::: ) "(" (Set ($#k2_borsuk_1 :::"[:"::: ) (Set (Var "S")) "," (Set (Var "T")) ($#k2_borsuk_1 :::":]"::: ) ) "," (Set ($#k4_borsuk_1 :::"["::: ) (Set (Var "s")) "," (Set (Var "t")) ($#k4_borsuk_1 :::"]"::: ) ) ")" ")" ) "," (Set "(" ($#k2_group_7 :::"product"::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set "(" ($#k5_topalg_1 :::"pi_1"::: ) "(" (Set (Var "S")) "," (Set (Var "s")) ")" ")" ) "," (Set "(" ($#k5_topalg_1 :::"pi_1"::: ) "(" (Set (Var "T")) "," (Set (Var "t")) ")" ")" ) ($#k10_finseq_1 :::"*>"::: ) ) ")" ) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set ($#k11_topalg_4 :::"FGPrIso"::: ) "(" (Set (Var "s")) "," (Set (Var "t")) ")" )) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k5_topalg_1 :::"pi_1"::: ) "(" (Set ($#k2_borsuk_1 :::"[:"::: ) (Set (Var "S")) "," (Set (Var "T")) ($#k2_borsuk_1 :::":]"::: ) ) "," (Set ($#k4_borsuk_1 :::"["::: ) (Set (Var "s")) "," (Set (Var "t")) ($#k4_borsuk_1 :::"]"::: ) ) ")" ")" ) (Bool "ex" (Set (Var "l")) "being" ($#m1_borsuk_2 :::"Loop":::) "of" (Set ($#k4_borsuk_1 :::"["::: ) (Set (Var "s")) "," (Set (Var "t")) ($#k4_borsuk_1 :::"]"::: ) ) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set "(" ($#k4_topalg_1 :::"EqRel"::: ) "(" (Set ($#k2_borsuk_1 :::"[:"::: ) (Set (Var "S")) "," (Set (Var "T")) ($#k2_borsuk_1 :::":]"::: ) ) "," (Set ($#k4_borsuk_1 :::"["::: ) (Set (Var "s")) "," (Set (Var "t")) ($#k4_borsuk_1 :::"]"::: ) ) ")" ")" ) "," (Set (Var "l")) ")" )) & (Bool (Set (Set (Var "b5")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set "(" ($#k6_eqrel_1 :::"Class"::: ) "(" (Set "(" ($#k4_topalg_1 :::"EqRel"::: ) "(" (Set (Var "S")) "," (Set (Var "s")) ")" ")" ) "," (Set "(" ($#k9_topalg_4 :::"pr1"::: ) (Set (Var "l")) ")" ) ")" ")" ) "," (Set "(" ($#k6_eqrel_1 :::"Class"::: ) "(" (Set "(" ($#k4_topalg_1 :::"EqRel"::: ) "(" (Set (Var "T")) "," (Set (Var "t")) ")" ")" ) "," (Set "(" ($#k10_topalg_4 :::"pr2"::: ) (Set (Var "l")) ")" ) ")" ")" ) ($#k10_finseq_1 :::"*>"::: ) )) ")" ))) ")" ))))); theorem :: TOPALG_4:27 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "t")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k5_topalg_1 :::"pi_1"::: ) "(" (Set ($#k2_borsuk_1 :::"[:"::: ) (Set (Var "S")) "," (Set (Var "T")) ($#k2_borsuk_1 :::":]"::: ) ) "," (Set ($#k4_borsuk_1 :::"["::: ) (Set (Var "s")) "," (Set (Var "t")) ($#k4_borsuk_1 :::"]"::: ) ) ")" ")" ) (Bool "for" (Set (Var "l")) "being" ($#m1_borsuk_2 :::"Loop":::) "of" (Set ($#k4_borsuk_1 :::"["::: ) (Set (Var "s")) "," (Set (Var "t")) ($#k4_borsuk_1 :::"]"::: ) ) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set "(" ($#k4_topalg_1 :::"EqRel"::: ) "(" (Set ($#k2_borsuk_1 :::"[:"::: ) (Set (Var "S")) "," (Set (Var "T")) ($#k2_borsuk_1 :::":]"::: ) ) "," (Set ($#k4_borsuk_1 :::"["::: ) (Set (Var "s")) "," (Set (Var "t")) ($#k4_borsuk_1 :::"]"::: ) ) ")" ")" ) "," (Set (Var "l")) ")" ))) "holds" (Bool (Set (Set "(" ($#k11_topalg_4 :::"FGPrIso"::: ) "(" (Set (Var "s")) "," (Set (Var "t")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set "(" ($#k6_eqrel_1 :::"Class"::: ) "(" (Set "(" ($#k4_topalg_1 :::"EqRel"::: ) "(" (Set (Var "S")) "," (Set (Var "s")) ")" ")" ) "," (Set "(" ($#k9_topalg_4 :::"pr1"::: ) (Set (Var "l")) ")" ) ")" ")" ) "," (Set "(" ($#k6_eqrel_1 :::"Class"::: ) "(" (Set "(" ($#k4_topalg_1 :::"EqRel"::: ) "(" (Set (Var "T")) "," (Set (Var "t")) ")" ")" ) "," (Set "(" ($#k10_topalg_4 :::"pr2"::: ) (Set (Var "l")) ")" ) ")" ")" ) ($#k10_finseq_1 :::"*>"::: ) ))))))) ; theorem :: TOPALG_4:28 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "t")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "l")) "being" ($#m1_borsuk_2 :::"Loop":::) "of" (Set ($#k4_borsuk_1 :::"["::: ) (Set (Var "s")) "," (Set (Var "t")) ($#k4_borsuk_1 :::"]"::: ) ) "holds" (Bool (Set (Set "(" ($#k11_topalg_4 :::"FGPrIso"::: ) "(" (Set (Var "s")) "," (Set (Var "t")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k6_eqrel_1 :::"Class"::: ) "(" (Set "(" ($#k4_topalg_1 :::"EqRel"::: ) "(" (Set ($#k2_borsuk_1 :::"[:"::: ) (Set (Var "S")) "," (Set (Var "T")) ($#k2_borsuk_1 :::":]"::: ) ) "," (Set ($#k4_borsuk_1 :::"["::: ) (Set (Var "s")) "," (Set (Var "t")) ($#k4_borsuk_1 :::"]"::: ) ) ")" ")" ) "," (Set (Var "l")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set "(" ($#k6_eqrel_1 :::"Class"::: ) "(" (Set "(" ($#k4_topalg_1 :::"EqRel"::: ) "(" (Set (Var "S")) "," (Set (Var "s")) ")" ")" ) "," (Set "(" ($#k9_topalg_4 :::"pr1"::: ) (Set (Var "l")) ")" ) ")" ")" ) "," (Set "(" ($#k6_eqrel_1 :::"Class"::: ) "(" (Set "(" ($#k4_topalg_1 :::"EqRel"::: ) "(" (Set (Var "T")) "," (Set (Var "t")) ")" ")" ) "," (Set "(" ($#k10_topalg_4 :::"pr2"::: ) (Set (Var "l")) ")" ) ")" ")" ) ($#k10_finseq_1 :::"*>"::: ) )))))) ; registrationlet "S", "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); let "s" be ($#m1_subset_1 :::"Point":::) "of" (Set (Const "S")); let "t" be ($#m1_subset_1 :::"Point":::) "of" (Set (Const "T")); cluster (Set ($#k11_topalg_4 :::"FGPrIso"::: ) "(" "s" "," "t" ")" ) -> ($#v2_funct_1 :::"one-to-one"::: ) ($#v2_funct_2 :::"onto"::: ) ; end; registrationlet "S", "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); let "s" be ($#m1_subset_1 :::"Point":::) "of" (Set (Const "S")); let "t" be ($#m1_subset_1 :::"Point":::) "of" (Set (Const "T")); cluster (Set ($#k11_topalg_4 :::"FGPrIso"::: ) "(" "s" "," "t" ")" ) -> ($#v1_group_6 :::"multiplicative"::: ) ; end; theorem :: TOPALG_4:29 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "t")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) "holds" (Bool (Set ($#k11_topalg_4 :::"FGPrIso"::: ) "(" (Set (Var "s")) "," (Set (Var "t")) ")" ) "is" ($#v3_funct_2 :::"bijective"::: ) )))) ; theorem :: TOPALG_4:30 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "t")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) "holds" (Bool (Set ($#k5_topalg_1 :::"pi_1"::: ) "(" (Set ($#k2_borsuk_1 :::"[:"::: ) (Set (Var "S")) "," (Set (Var "T")) ($#k2_borsuk_1 :::":]"::: ) ) "," (Set ($#k4_borsuk_1 :::"["::: ) (Set (Var "s")) "," (Set (Var "t")) ($#k4_borsuk_1 :::"]"::: ) ) ")" ) "," (Set ($#k2_group_7 :::"product"::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set "(" ($#k5_topalg_1 :::"pi_1"::: ) "(" (Set (Var "S")) "," (Set (Var "s")) ")" ")" ) "," (Set "(" ($#k5_topalg_1 :::"pi_1"::: ) "(" (Set (Var "T")) "," (Set (Var "t")) ")" ")" ) ($#k10_finseq_1 :::"*>"::: ) )) ($#r2_group_6 :::"are_isomorphic"::: ) )))) ; theorem :: TOPALG_4:31 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "s1")) "," (Set (Var "s2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "t1")) "," (Set (Var "t2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Homomorphism":::) "of" (Set "(" ($#k5_topalg_1 :::"pi_1"::: ) "(" (Set (Var "S")) "," (Set (Var "s1")) ")" ")" ) "," (Set "(" ($#k5_topalg_1 :::"pi_1"::: ) "(" (Set (Var "S")) "," (Set (Var "s2")) ")" ")" ) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Homomorphism":::) "of" (Set "(" ($#k5_topalg_1 :::"pi_1"::: ) "(" (Set (Var "T")) "," (Set (Var "t1")) ")" ")" ) "," (Set "(" ($#k5_topalg_1 :::"pi_1"::: ) "(" (Set (Var "T")) "," (Set (Var "t2")) ")" ")" ) "st" (Bool (Bool (Set (Var "f")) "is" ($#v3_funct_2 :::"bijective"::: ) ) & (Bool (Set (Var "g")) "is" ($#v3_funct_2 :::"bijective"::: ) )) "holds" (Bool (Set (Set "(" ($#k1_topalg_4 :::"Gr2Iso"::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ")" ) ($#k1_partfun1 :::"*"::: ) (Set "(" ($#k11_topalg_4 :::"FGPrIso"::: ) "(" (Set (Var "s1")) "," (Set (Var "t1")) ")" ")" )) "is" ($#v3_funct_2 :::"bijective"::: ) )))))) ; theorem :: TOPALG_4:32 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_borsuk_2 :::"pathwise_connected"::: ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "s1")) "," (Set (Var "s2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "t1")) "," (Set (Var "t2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) "holds" (Bool (Set ($#k5_topalg_1 :::"pi_1"::: ) "(" (Set ($#k2_borsuk_1 :::"[:"::: ) (Set (Var "S")) "," (Set (Var "T")) ($#k2_borsuk_1 :::":]"::: ) ) "," (Set ($#k4_borsuk_1 :::"["::: ) (Set (Var "s1")) "," (Set (Var "t1")) ($#k4_borsuk_1 :::"]"::: ) ) ")" ) "," (Set ($#k2_group_7 :::"product"::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set "(" ($#k5_topalg_1 :::"pi_1"::: ) "(" (Set (Var "S")) "," (Set (Var "s2")) ")" ")" ) "," (Set "(" ($#k5_topalg_1 :::"pi_1"::: ) "(" (Set (Var "T")) "," (Set (Var "t2")) ")" ")" ) ($#k10_finseq_1 :::"*>"::: ) )) ($#r2_group_6 :::"are_isomorphic"::: ) )))) ;