:: MATRTOP3  semantic presentation begin  

















theorem :: MATRTOP3:1 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "K")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "M")) "being"   ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K"))  (Bool  "for" (Set (Var "P")) "being"   ($#m1_subset_1 :::"Permutation":::) "of" (Set  "("  ($#k2_finseq_1 :::"Seg"::: )  (Set (Var "n")) ")" ) "holds"   (Bool  "("  (Bool (Set   ($#k12_matrix_3 :::"Det"::: )  (Set  "(" (Set  "(" (Set  "(" (Set  "(" (Set (Var "M"))  ($#k4_matrix11 :::"*"::: )  (Set (Var "P")) ")" )  ($#k5_matrix_1 :::"@"::: )  ")" )  ($#k4_matrix11 :::"*"::: )  (Set (Var "P")) ")" )  ($#k5_matrix_1 :::"@"::: )  ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k12_matrix_3 :::"Det"::: )  (Set (Var "M")))) & (Bool  "("   "for" (Set (Var "i")) "," (Set (Var "j")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set   ($#k2_matrix_1 :::"Indices"::: )  (Set (Var "M"))))) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set  "(" (Set  "(" (Set (Var "M"))  ($#k4_matrix11 :::"*"::: )  (Set (Var "P")) ")" )  ($#k5_matrix_1 :::"@"::: )  ")" )  ($#k4_matrix11 :::"*"::: )  (Set (Var "P")) ")" )  ($#k5_matrix_1 :::"@"::: )  ")" )  ($#k3_matrix_1 :::"*"::: )   "(" (Set (Var "i")) "," (Set (Var "j")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "M"))  ($#k3_matrix_1 :::"*"::: )   "(" (Set  "(" (Set (Var "P"))  ($#k1_seq_1 :::"."::: )  (Set (Var "i")) ")" ) "," (Set  "(" (Set (Var "P"))  ($#k1_seq_1 :::"."::: )  (Set (Var "j")) ")" ) ")" ))  ")" )  ")" ))))) ; 
 
theorem :: MATRTOP3:2 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "K")) "being"   ($#l6_algstr_0 :::"Field":::)  (Bool  "for" (Set (Var "M")) "being" bbbadV2_MATRIX_1((Set (Var "b2")))  ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "K")) "holds"  (Bool (Set (Set (Var "M"))  ($#k5_matrix_1 :::"@"::: )  )  ($#r1_hidden :::"="::: )  (Set (Var "M")))))) ; 
 
theorem :: MATRTOP3:3 (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#v3_valued_0 :::"real-valued"::: )    ($#m1_hidden :::"FinSequence":::)  (Bool  "for" (Set (Var "i")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "f"))))) "holds"  (Bool (Set   ($#k18_rvsum_1 :::"Sum"::: )  (Set  "("  ($#k12_rvsum_1 :::"sqr"::: )  (Set  "(" (Set (Var "f"))  ($#k2_funct_7 :::"+*"::: )   "(" (Set (Var "i")) "," (Set (Var "r")) ")"  ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k18_rvsum_1 :::"Sum"::: )  (Set  "("  ($#k12_rvsum_1 :::"sqr"::: )  (Set (Var "f")) ")" ) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set  "(" (Set (Var "f"))  ($#k1_seq_1 :::"."::: )  (Set (Var "i")) ")" )  ($#k5_square_1 :::"^2"::: )  ")" ) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set (Var "r"))  ($#k3_square_1 :::"^2"::: )  ")" )))))) ; 
 definitionlet "X" be    ($#m1_hidden :::"set"::: )  ; let "F" be   ($#v1_funcop_1 :::"Function-yielding"::: )    ($#m1_hidden :::"Function":::); attr "F" is "X" :::"-support-yielding":::  means :: MATRTOP3:def 1 (Bool  "for" (Set (Var "f")) "being"   ($#m1_hidden :::"Function":::)  (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "f"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  "F")) & (Bool (Set (Set  "(" "F"  ($#k1_funct_1 :::"."::: )  (Set (Var "f")) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"<>"::: )  (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "x"))))) "holds"  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  "X"))); end; 





:: deftheorem    defines :::"-support-yielding"::: MATRTOP3:def 1 :  (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "F")) "being"   ($#v1_funcop_1 :::"Function-yielding"::: )    ($#m1_hidden :::"Function":::) "holds"   (Bool  "("  (Bool (Set (Var "F")) "is" (Set (Var "X"))  ($#v1_matrtop3 :::"-support-yielding"::: )  ) "iff" (Bool  "for" (Set (Var "f")) "being"   ($#m1_hidden :::"Function":::)  (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "f"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "F")))) & (Bool (Set (Set  "(" (Set (Var "F"))  ($#k1_funct_1 :::"."::: )  (Set (Var "f")) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"<>"::: )  (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "x"))))) "holds"  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))))  ")" ))); 
 registrationlet "X" be    ($#m1_hidden :::"set"::: )  ; 
cluster   ($#v1_relat_1 :::"Relation-like"::: )     ($#v1_funct_1 :::"Function-like"::: )     ($#v1_funcop_1 :::"Function-yielding"::: )   bbbadV2_FUNCOP_1() "X"  ($#v1_matrtop3 :::"-support-yielding"::: )    for    ($#m1_hidden :::"set"::: )  ; 
end; registrationlet "X" be    ($#m1_hidden :::"set"::: )  ; let "Y" be   ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "X")); 
cluster   ($#v1_relat_1 :::"Relation-like"::: )     ($#v1_funct_1 :::"Function-like"::: )     ($#v1_funcop_1 :::"Function-yielding"::: )   "Y"  ($#v1_matrtop3 :::"-support-yielding"::: )    ->   ($#v1_funcop_1 :::"Function-yielding"::: )   "X"  ($#v1_matrtop3 :::"-support-yielding"::: )    for    ($#m1_hidden :::"set"::: )  ; 
end; registrationlet "X", "Y" be    ($#m1_hidden :::"set"::: )  ; 
cluster   ($#v1_relat_1 :::"Relation-like"::: )     ($#v1_funct_1 :::"Function-like"::: )     ($#v1_funcop_1 :::"Function-yielding"::: )   "X"  ($#v1_matrtop3 :::"-support-yielding"::: )   "Y"  ($#v1_matrtop3 :::"-support-yielding"::: )    ->   ($#v1_funcop_1 :::"Function-yielding"::: )   (Set "X"  ($#k3_xboole_0 :::"/\"::: )  "Y")  ($#v1_matrtop3 :::"-support-yielding"::: )    for    ($#m1_hidden :::"set"::: )  ; 
let "f" be   ($#v1_funcop_1 :::"Function-yielding"::: )   (Set (Const "X"))  ($#v1_matrtop3 :::"-support-yielding"::: )    ($#m1_hidden :::"Function":::); let "g" be   ($#v1_funcop_1 :::"Function-yielding"::: )   (Set (Const "Y"))  ($#v1_matrtop3 :::"-support-yielding"::: )    ($#m1_hidden :::"Function":::); 
cluster (Set "g"  ($#k3_relat_1 :::"(#)"::: )  "f") -> (Set "X"  ($#k2_xboole_0 :::"\/"::: )  "Y")  ($#v1_matrtop3 :::"-support-yielding"::: )   ; 
end; registrationlet "n" be   ($#m1_hidden :::"Nat":::); 
cluster  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v1_relat_1 :::"Relation-like"::: )   (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  "n" ")" ))  ($#v4_relat_1 :::"-defined"::: )   (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  "n" ")" ))  ($#v5_relat_1 :::"-valued"::: )     ($#v1_funct_1 :::"Function-like"::: )     ($#v1_partfun1 :::"total"::: )     ($#v1_funct_2 :::"quasi_total"::: )     ($#v1_topreal9 :::"homogeneous"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_zfmisc_1 :::"bool"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  "n" ")" )) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  "n" ")" )) ($#k2_zfmisc_1 :::":]"::: ) )); 
end; registrationlet "n", "m" be   ($#m1_hidden :::"Nat":::); 
cluster   ($#v1_funct_1 :::"Function-like"::: )     ($#v1_funct_2 :::"quasi_total"::: )    ->   ($#v1_pre_poly :::"FinSequence-yielding"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_zfmisc_1 :::"bool"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  "n" ")" )) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  "m" ")" )) ($#k2_zfmisc_1 :::":]"::: ) )); 
end; registrationlet "n", "m" be   ($#m1_hidden :::"Nat":::); let "A" be   ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Const "n")) "," (Set (Const "m")) "," (Set  ($#k2_vectsp_1 :::"F_Real"::: ) ); 
cluster (Set   ($#k3_matrtop1 :::"Mx2Tran"::: )  "A") ->   ($#v13_vectsp_1 :::"additive"::: )   ; 
end; registrationlet "n" be   ($#m1_hidden :::"Nat":::); let "A" be   ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Const "n")) "," (Set  ($#k2_vectsp_1 :::"F_Real"::: ) ); 
cluster (Set   ($#k3_matrtop1 :::"Mx2Tran"::: )  "A") ->   ($#v1_topreal9 :::"homogeneous"::: )   ; 
end; registrationlet "n" be   ($#m1_hidden :::"Nat":::); let "f", "g" be   ($#v1_topreal9 :::"homogeneous"::: )    ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Const "n")) ")" ) "," (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Const "n")) ")" ); 
cluster (Set "g"  ($#k3_relat_1 :::"(#)"::: )  "f") ->   ($#v1_topreal9 :::"homogeneous"::: )    for  ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  "n" ")" ) "," (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  "n" ")" ); 
end; begin  



definitionlet "n", "i" be   ($#m1_hidden :::"Nat":::); assume 
(Bool (Set (Const "i"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_finseq_1 :::"Seg"::: )  (Set (Const "n"))))
 ; func  :::"AxialSymmetry":::  "(" "i" "," "n" ")"  ->   ($#v1_matrix_6 :::"invertible"::: )    ($#m1_matrix_1 :::"Matrix":::) "of" "n" "," (Set  ($#k2_vectsp_1 :::"F_Real"::: ) ) means :: MATRTOP3:def 2 (Bool  "("  (Bool (Set it  ($#k3_matrix_1 :::"*"::: )   "(" "i" "," "i" ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k4_algstr_0 :::"-"::: )  (Set  "("  ($#k5_struct_0 :::"1."::: )  (Set  ($#k2_vectsp_1 :::"F_Real"::: ) ) ")" ))) & (Bool  "("   "for" (Set (Var "k")) "," (Set (Var "m")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "k")) "," (Set (Var "m")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set   ($#k2_matrix_1 :::"Indices"::: )  it))) "holds"  (Bool  "("   "("  (Bool (Bool (Set (Var "k"))  ($#r1_hidden :::"="::: )  (Set (Var "m"))) & (Bool (Set (Var "k"))  ($#r1_hidden :::"<>"::: )  "i")) "implies" (Bool (Set it  ($#k3_matrix_1 :::"*"::: )   "(" (Set (Var "k")) "," (Set (Var "k")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k5_struct_0 :::"1."::: )  (Set  ($#k2_vectsp_1 :::"F_Real"::: ) )))  ")"  &  "("  (Bool (Bool (Set (Var "k"))  ($#r1_hidden :::"<>"::: )  (Set (Var "m")))) "implies" (Bool (Set it  ($#k3_matrix_1 :::"*"::: )   "(" (Set (Var "k")) "," (Set (Var "m")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set  ($#k2_vectsp_1 :::"F_Real"::: ) )))  ")"   ")" )  ")" )  ")" ); end; 







:: deftheorem    defines :::"AxialSymmetry"::: MATRTOP3:def 2 :  (Bool  "for" (Set (Var "n")) "," (Set (Var "i")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_finseq_1 :::"Seg"::: )  (Set (Var "n"))))) "holds"  (Bool  "for" (Set (Var "b3")) "being"   ($#v1_matrix_6 :::"invertible"::: )    ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set  ($#k2_vectsp_1 :::"F_Real"::: ) ) "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_matrtop3 :::"AxialSymmetry"::: )   "(" (Set (Var "i")) "," (Set (Var "n")) ")" )) "iff" (Bool  "("  (Bool (Set (Set (Var "b3"))  ($#k3_matrix_1 :::"*"::: )   "(" (Set (Var "i")) "," (Set (Var "i")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k4_algstr_0 :::"-"::: )  (Set  "("  ($#k5_struct_0 :::"1."::: )  (Set  ($#k2_vectsp_1 :::"F_Real"::: ) ) ")" ))) & (Bool  "("   "for" (Set (Var "k")) "," (Set (Var "m")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "k")) "," (Set (Var "m")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set   ($#k2_matrix_1 :::"Indices"::: )  (Set (Var "b3"))))) "holds"  (Bool  "("   "("  (Bool (Bool (Set (Var "k"))  ($#r1_hidden :::"="::: )  (Set (Var "m"))) & (Bool (Set (Var "k"))  ($#r1_hidden :::"<>"::: )  (Set (Var "i")))) "implies" (Bool (Set (Set (Var "b3"))  ($#k3_matrix_1 :::"*"::: )   "(" (Set (Var "k")) "," (Set (Var "k")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k5_struct_0 :::"1."::: )  (Set  ($#k2_vectsp_1 :::"F_Real"::: ) )))  ")"  &  "("  (Bool (Bool (Set (Var "k"))  ($#r1_hidden :::"<>"::: )  (Set (Var "m")))) "implies" (Bool (Set (Set (Var "b3"))  ($#k3_matrix_1 :::"*"::: )   "(" (Set (Var "k")) "," (Set (Var "m")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set  ($#k2_vectsp_1 :::"F_Real"::: ) )))  ")"   ")" )  ")" )  ")" )  ")" ))); 
 
theorem :: MATRTOP3:4 (Bool  "for" (Set (Var "i")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_finseq_1 :::"Seg"::: )  (Set (Var "n"))))) "holds"  (Bool (Set   ($#k12_matrix_3 :::"Det"::: )  (Set  "("  ($#k1_matrtop3 :::"AxialSymmetry"::: )   "(" (Set (Var "i")) "," (Set (Var "n")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k4_algstr_0 :::"-"::: )  (Set  "("  ($#k5_struct_0 :::"1."::: )  (Set  ($#k2_vectsp_1 :::"F_Real"::: ) ) ")" )))) ; 
 
theorem :: MATRTOP3:5 (Bool  "for" (Set (Var "i")) "," (Set (Var "n")) "," (Set (Var "j")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  "st" (Bool (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_finseq_1 :::"Seg"::: )  (Set (Var "n")))) & (Bool (Set (Var "j"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_finseq_1 :::"Seg"::: )  (Set (Var "n")))) & (Bool (Set (Var "i"))  ($#r1_hidden :::"<>"::: )  (Set (Var "j")))) "holds"  (Bool (Set (Set  "("  ($#k1_matrtop1 :::"@"::: )  (Set (Var "p")) ")" )  ($#k13_fvsum_1 :::""*""::: )  (Set  "("  ($#k9_matrix_1 :::"Col"::: )   "(" (Set  "("  ($#k1_matrtop3 :::"AxialSymmetry"::: )   "(" (Set (Var "i")) "," (Set (Var "n")) ")"  ")" ) "," (Set (Var "j")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "p"))  ($#k1_seq_1 :::"."::: )  (Set (Var "j")))))) ; 
 
theorem :: MATRTOP3:6 (Bool  "for" (Set (Var "i")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  "st" (Bool (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_finseq_1 :::"Seg"::: )  (Set (Var "n"))))) "holds"  (Bool (Set (Set  "("  ($#k1_matrtop1 :::"@"::: )  (Set (Var "p")) ")" )  ($#k13_fvsum_1 :::""*""::: )  (Set  "("  ($#k9_matrix_1 :::"Col"::: )   "(" (Set  "("  ($#k1_matrtop3 :::"AxialSymmetry"::: )   "(" (Set (Var "i")) "," (Set (Var "n")) ")"  ")" ) "," (Set (Var "i")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_real_1 :::"-"::: )  (Set  "(" (Set (Var "p"))  ($#k1_seq_1 :::"."::: )  (Set (Var "i")) ")" ))))) ; 
 
theorem :: MATRTOP3:7 (Bool  "for" (Set (Var "i")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_finseq_1 :::"Seg"::: )  (Set (Var "n"))))) "holds"  (Bool  "("  (Bool (Set   ($#k1_matrtop3 :::"AxialSymmetry"::: )   "(" (Set (Var "i")) "," (Set (Var "n")) ")" ) "is" bbbadV2_MATRIX_1((Set   ($#k2_vectsp_1 :::"F_Real"::: )  ))) & (Bool (Set (Set  "("  ($#k1_matrtop3 :::"AxialSymmetry"::: )   "(" (Set (Var "i")) "," (Set (Var "n")) ")"  ")" )  ($#k5_matrix_6 :::"~"::: )  )  ($#r1_hidden :::"="::: )  (Set   ($#k1_matrtop3 :::"AxialSymmetry"::: )   "(" (Set (Var "i")) "," (Set (Var "n")) ")" ))  ")" )) ; 
 
theorem :: MATRTOP3:8 (Bool  "for" (Set (Var "i")) "," (Set (Var "n")) "," (Set (Var "j")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  "st" (Bool (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_finseq_1 :::"Seg"::: )  (Set (Var "n")))) & (Bool (Set (Var "i"))  ($#r1_hidden :::"<>"::: )  (Set (Var "j")))) "holds"  (Bool (Set (Set  "(" (Set  "("  ($#k3_matrtop1 :::"Mx2Tran"::: )  (Set  "("  ($#k1_matrtop3 :::"AxialSymmetry"::: )   "(" (Set (Var "i")) "," (Set (Var "n")) ")"  ")" ) ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "p")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "j")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "p"))  ($#k1_seq_1 :::"."::: )  (Set (Var "j")))))) ; 
 
theorem :: MATRTOP3:9 (Bool  "for" (Set (Var "i")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  "st" (Bool (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_finseq_1 :::"Seg"::: )  (Set (Var "n"))))) "holds"  (Bool (Set (Set  "(" (Set  "("  ($#k3_matrtop1 :::"Mx2Tran"::: )  (Set  "("  ($#k1_matrtop3 :::"AxialSymmetry"::: )   "(" (Set (Var "i")) "," (Set (Var "n")) ")"  ")" ) ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "p")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "i")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_real_1 :::"-"::: )  (Set  "(" (Set (Var "p"))  ($#k1_seq_1 :::"."::: )  (Set (Var "i")) ")" ))))) ; 
 
theorem :: MATRTOP3:10 (Bool  "for" (Set (Var "i")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  "st" (Bool (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_finseq_1 :::"Seg"::: )  (Set (Var "n"))))) "holds"  (Bool (Set (Set  "("  ($#k3_matrtop1 :::"Mx2Tran"::: )  (Set  "("  ($#k1_matrtop3 :::"AxialSymmetry"::: )   "(" (Set (Var "i")) "," (Set (Var "n")) ")"  ")" ) ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "p"))  ($#k2_funct_7 :::"+*"::: )   "(" (Set (Var "i")) "," (Set  "("  ($#k1_real_1 :::"-"::: )  (Set  "(" (Set (Var "p"))  ($#k1_seq_1 :::"."::: )  (Set (Var "i")) ")" ) ")" ) ")" )))) ; 
 
theorem :: MATRTOP3:11 (Bool  "for" (Set (Var "i")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_finseq_1 :::"Seg"::: )  (Set (Var "n"))))) "holds"  (Bool (Set   ($#k3_matrtop1 :::"Mx2Tran"::: )  (Set  "("  ($#k1_matrtop3 :::"AxialSymmetry"::: )   "(" (Set (Var "i")) "," (Set (Var "n")) ")"  ")" )) "is" (Set  ($#k3_matrix13 :::"{"::: ) (Set (Var "i")) ($#k3_matrix13 :::"}"::: ) )  ($#v1_matrtop3 :::"-support-yielding"::: )  )) ; 
 
theorem :: MATRTOP3:12 (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  ($#k2_vectsp_1 :::"F_Real"::: ) )  "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set   ($#k20_sin_cos :::"cos"::: )  (Set (Var "r")))) & (Bool (Set (Var "b"))  ($#r1_hidden :::"="::: )  (Set   ($#k17_sin_cos :::"sin"::: )  (Set (Var "r"))))) "holds"  (Bool (Set   ($#k12_matrix_3 :::"Det"::: )  (Set  "("  ($#k20_matrixj1 :::"block_diagonal"::: )   "(" (Set  ($#k17_matrixj1 :::"<*"::: ) (Set  "("  "(" (Set (Var "a")) "," (Set (Var "b")) ")"   ($#k6_matrix_2 :::"]["::: )   "(" (Set  "("  ($#k4_algstr_0 :::"-"::: )  (Set (Var "b")) ")" ) "," (Set (Var "a")) ")"  ")" ) "," (Set  "("  ($#k12_matrix_1 :::"1."::: )   "(" (Set  ($#k2_vectsp_1 :::"F_Real"::: ) ) "," (Set (Var "n")) ")"  ")" ) ($#k17_matrixj1 :::"*>"::: ) ) "," (Set  "("  ($#k4_struct_0 :::"0."::: )  (Set  ($#k2_vectsp_1 :::"F_Real"::: ) ) ")" ) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k5_struct_0 :::"1."::: )  (Set  ($#k2_vectsp_1 :::"F_Real"::: ) )))))) ; 
 begin  definitionlet "n" be   ($#m1_hidden :::"Nat":::); let "r" be   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; let "i", "j" be   ($#m1_hidden :::"Nat":::); assume 
(Bool  "("  (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Const "i"))) & (Bool (Set (Const "i"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Const "j"))) & (Bool (Set (Const "j"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Const "n")))  ")" )
 ; func  :::"Rotation":::  "(" "i" "," "j" "," "n" "," "r" ")"  ->   ($#v1_matrix_6 :::"invertible"::: )    ($#m1_matrix_1 :::"Matrix":::) "of" "n" "," (Set  ($#k2_vectsp_1 :::"F_Real"::: ) ) means :: MATRTOP3:def 3 (Bool  "("  (Bool (Set it  ($#k3_matrix_1 :::"*"::: )   "(" "i" "," "i" ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k20_sin_cos :::"cos"::: )  "r")) & (Bool (Set it  ($#k3_matrix_1 :::"*"::: )   "(" "j" "," "j" ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k20_sin_cos :::"cos"::: )  "r")) & (Bool (Set it  ($#k3_matrix_1 :::"*"::: )   "(" "i" "," "j" ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k17_sin_cos :::"sin"::: )  "r")) & (Bool (Set it  ($#k3_matrix_1 :::"*"::: )   "(" "j" "," "i" ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k4_xcmplx_0 :::"-"::: )  (Set  "("  ($#k17_sin_cos :::"sin"::: )  "r" ")" ))) & (Bool  "("   "for" (Set (Var "k")) "," (Set (Var "m")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "k")) "," (Set (Var "m")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set   ($#k2_matrix_1 :::"Indices"::: )  it))) "holds"  (Bool  "("   "("  (Bool (Bool (Set (Var "k"))  ($#r1_hidden :::"="::: )  (Set (Var "m"))) & (Bool (Set (Var "k"))  ($#r1_hidden :::"<>"::: )  "i") & (Bool (Set (Var "k"))  ($#r1_hidden :::"<>"::: )  "j")) "implies" (Bool (Set it  ($#k3_matrix_1 :::"*"::: )   "(" (Set (Var "k")) "," (Set (Var "k")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k5_struct_0 :::"1."::: )  (Set  ($#k2_vectsp_1 :::"F_Real"::: ) )))  ")"  &  "("  (Bool (Bool (Set (Var "k"))  ($#r1_hidden :::"<>"::: )  (Set (Var "m"))) & (Bool (Set  ($#k4_matrix13 :::"{"::: ) (Set (Var "k")) "," (Set (Var "m")) ($#k4_matrix13 :::"}"::: ) )  ($#r1_hidden :::"<>"::: )  (Set  ($#k4_matrix13 :::"{"::: ) "i" "," "j" ($#k4_matrix13 :::"}"::: ) ))) "implies" (Bool (Set it  ($#k3_matrix_1 :::"*"::: )   "(" (Set (Var "k")) "," (Set (Var "m")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set  ($#k2_vectsp_1 :::"F_Real"::: ) )))  ")"   ")" )  ")" )  ")" ); end; 









:: deftheorem    defines :::"Rotation"::: MATRTOP3:def 3 :  (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "i")) "," (Set (Var "j")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i"))) & (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "j"))) & (Bool (Set (Var "j"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n")))) "holds"  (Bool  "for" (Set (Var "b5")) "being"   ($#v1_matrix_6 :::"invertible"::: )    ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set  ($#k2_vectsp_1 :::"F_Real"::: ) ) "holds"   (Bool  "("  (Bool (Set (Var "b5"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_matrtop3 :::"Rotation"::: )   "(" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "n")) "," (Set (Var "r")) ")" )) "iff" (Bool  "("  (Bool (Set (Set (Var "b5"))  ($#k3_matrix_1 :::"*"::: )   "(" (Set (Var "i")) "," (Set (Var "i")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k20_sin_cos :::"cos"::: )  (Set (Var "r")))) & (Bool (Set (Set (Var "b5"))  ($#k3_matrix_1 :::"*"::: )   "(" (Set (Var "j")) "," (Set (Var "j")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k20_sin_cos :::"cos"::: )  (Set (Var "r")))) & (Bool (Set (Set (Var "b5"))  ($#k3_matrix_1 :::"*"::: )   "(" (Set (Var "i")) "," (Set (Var "j")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k17_sin_cos :::"sin"::: )  (Set (Var "r")))) & (Bool (Set (Set (Var "b5"))  ($#k3_matrix_1 :::"*"::: )   "(" (Set (Var "j")) "," (Set (Var "i")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k4_xcmplx_0 :::"-"::: )  (Set  "("  ($#k17_sin_cos :::"sin"::: )  (Set (Var "r")) ")" ))) & (Bool  "("   "for" (Set (Var "k")) "," (Set (Var "m")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "k")) "," (Set (Var "m")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set   ($#k2_matrix_1 :::"Indices"::: )  (Set (Var "b5"))))) "holds"  (Bool  "("   "("  (Bool (Bool (Set (Var "k"))  ($#r1_hidden :::"="::: )  (Set (Var "m"))) & (Bool (Set (Var "k"))  ($#r1_hidden :::"<>"::: )  (Set (Var "i"))) & (Bool (Set (Var "k"))  ($#r1_hidden :::"<>"::: )  (Set (Var "j")))) "implies" (Bool (Set (Set (Var "b5"))  ($#k3_matrix_1 :::"*"::: )   "(" (Set (Var "k")) "," (Set (Var "k")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k5_struct_0 :::"1."::: )  (Set  ($#k2_vectsp_1 :::"F_Real"::: ) )))  ")"  &  "("  (Bool (Bool (Set (Var "k"))  ($#r1_hidden :::"<>"::: )  (Set (Var "m"))) & (Bool (Set  ($#k4_matrix13 :::"{"::: ) (Set (Var "k")) "," (Set (Var "m")) ($#k4_matrix13 :::"}"::: ) )  ($#r1_hidden :::"<>"::: )  (Set  ($#k4_matrix13 :::"{"::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k4_matrix13 :::"}"::: ) ))) "implies" (Bool (Set (Set (Var "b5"))  ($#k3_matrix_1 :::"*"::: )   "(" (Set (Var "k")) "," (Set (Var "m")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set  ($#k2_vectsp_1 :::"F_Real"::: ) )))  ")"   ")" )  ")" )  ")" )  ")" ))))); 
 
theorem :: MATRTOP3:13 (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i"))) & (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "j"))) & (Bool (Set (Var "j"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n")))) "holds"  (Bool (Set   ($#k12_matrix_3 :::"Det"::: )  (Set  "("  ($#k2_matrtop3 :::"Rotation"::: )   "(" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "n")) "," (Set (Var "r")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k5_struct_0 :::"1."::: )  (Set  ($#k2_vectsp_1 :::"F_Real"::: ) ))))) ; 
 
theorem :: MATRTOP3:14 (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "n")) "," (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i"))) & (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "j"))) & (Bool (Set (Var "j"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n"))) & (Bool (Set (Var "k"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_finseq_1 :::"Seg"::: )  (Set (Var "n")))) & (Bool (Set (Var "k"))  ($#r1_hidden :::"<>"::: )  (Set (Var "i"))) & (Bool (Set (Var "k"))  ($#r1_hidden :::"<>"::: )  (Set (Var "j")))) "holds"  (Bool (Set (Set  "("  ($#k1_matrtop1 :::"@"::: )  (Set (Var "p")) ")" )  ($#k13_fvsum_1 :::""*""::: )  (Set  "("  ($#k9_matrix_1 :::"Col"::: )   "(" (Set  "("  ($#k2_matrtop3 :::"Rotation"::: )   "(" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "n")) "," (Set (Var "r")) ")"  ")" ) "," (Set (Var "k")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "p"))  ($#k1_seq_1 :::"."::: )  (Set (Var "k"))))))) ; 
 
theorem :: MATRTOP3:15 (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i"))) & (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "j"))) & (Bool (Set (Var "j"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n")))) "holds"  (Bool (Set (Set  "("  ($#k1_matrtop1 :::"@"::: )  (Set (Var "p")) ")" )  ($#k13_fvsum_1 :::""*""::: )  (Set  "("  ($#k9_matrix_1 :::"Col"::: )   "(" (Set  "("  ($#k2_matrtop3 :::"Rotation"::: )   "(" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "n")) "," (Set (Var "r")) ")"  ")" ) "," (Set (Var "i")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set (Var "p"))  ($#k1_seq_1 :::"."::: )  (Set (Var "i")) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "("  ($#k20_sin_cos :::"cos"::: )  (Set (Var "r")) ")" ) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "(" (Set (Var "p"))  ($#k1_seq_1 :::"."::: )  (Set (Var "j")) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set  "("  ($#k17_sin_cos :::"sin"::: )  (Set (Var "r")) ")" ) ")" ) ")" )))))) ; 
 
theorem :: MATRTOP3:16 (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i"))) & (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "j"))) & (Bool (Set (Var "j"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n")))) "holds"  (Bool (Set (Set  "("  ($#k1_matrtop1 :::"@"::: )  (Set (Var "p")) ")" )  ($#k13_fvsum_1 :::""*""::: )  (Set  "("  ($#k9_matrix_1 :::"Col"::: )   "(" (Set  "("  ($#k2_matrtop3 :::"Rotation"::: )   "(" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "n")) "," (Set (Var "r")) ")"  ")" ) "," (Set (Var "j")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set (Var "p"))  ($#k1_seq_1 :::"."::: )  (Set (Var "i")) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "("  ($#k17_sin_cos :::"sin"::: )  (Set (Var "r")) ")" ) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "(" (Set (Var "p"))  ($#k1_seq_1 :::"."::: )  (Set (Var "j")) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "("  ($#k20_sin_cos :::"cos"::: )  (Set (Var "r")) ")" ) ")" )))))) ; 
 
theorem :: MATRTOP3:17 (Bool  "for" (Set (Var "r1")) "," (Set (Var "r2")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i"))) & (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "j"))) & (Bool (Set (Var "j"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n")))) "holds"  (Bool (Set (Set  "("  ($#k2_matrtop3 :::"Rotation"::: )   "(" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "n")) "," (Set (Var "r1")) ")"  ")" )  ($#k4_matrix_6 :::"*"::: )  (Set  "("  ($#k2_matrtop3 :::"Rotation"::: )   "(" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "n")) "," (Set (Var "r2")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k2_matrtop3 :::"Rotation"::: )   "(" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "n")) "," (Set  "(" (Set (Var "r1"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "r2")) ")" ) ")" )))) ; 
 
theorem :: MATRTOP3:18 (Bool  "for" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i"))) & (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "j"))) & (Bool (Set (Var "j"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n")))) "holds"  (Bool (Set   ($#k2_matrtop3 :::"Rotation"::: )   "(" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "n")) "," (Set  ($#k1_xboole_0 :::"0"::: ) ) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k12_matrix_1 :::"1."::: )   "(" (Set  ($#k2_vectsp_1 :::"F_Real"::: ) ) "," (Set (Var "n")) ")" ))) ; 
 
theorem :: MATRTOP3:19 (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i"))) & (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "j"))) & (Bool (Set (Var "j"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n")))) "holds"  (Bool  "("  (Bool (Set   ($#k2_matrtop3 :::"Rotation"::: )   "(" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "n")) "," (Set (Var "r")) ")" ) "is"   ($#v4_matrix_6 :::"Orthogonal"::: )  ) & (Bool (Set (Set  "("  ($#k2_matrtop3 :::"Rotation"::: )   "(" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "n")) "," (Set (Var "r")) ")"  ")" )  ($#k5_matrix_6 :::"~"::: )  )  ($#r1_hidden :::"="::: )  (Set   ($#k2_matrtop3 :::"Rotation"::: )   "(" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "n")) "," (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "r")) ")" ) ")" ))  ")" ))) ; 
 
theorem :: MATRTOP3:20 (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "n")) "," (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i"))) & (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "j"))) & (Bool (Set (Var "j"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n"))) & (Bool (Set (Var "k"))  ($#r1_hidden :::"<>"::: )  (Set (Var "i"))) & (Bool (Set (Var "k"))  ($#r1_hidden :::"<>"::: )  (Set (Var "j")))) "holds"  (Bool (Set (Set  "(" (Set  "("  ($#k3_matrtop1 :::"Mx2Tran"::: )  (Set  "("  ($#k2_matrtop3 :::"Rotation"::: )   "(" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "n")) "," (Set (Var "r")) ")"  ")" ) ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "p")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "k")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "p"))  ($#k1_seq_1 :::"."::: )  (Set (Var "k"))))))) ; 
 
theorem :: MATRTOP3:21 (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i"))) & (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "j"))) & (Bool (Set (Var "j"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n")))) "holds"  (Bool (Set (Set  "(" (Set  "("  ($#k3_matrtop1 :::"Mx2Tran"::: )  (Set  "("  ($#k2_matrtop3 :::"Rotation"::: )   "(" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "n")) "," (Set (Var "r")) ")"  ")" ) ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "p")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "i")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set (Var "p"))  ($#k1_seq_1 :::"."::: )  (Set (Var "i")) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "("  ($#k20_sin_cos :::"cos"::: )  (Set (Var "r")) ")" ) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "(" (Set (Var "p"))  ($#k1_seq_1 :::"."::: )  (Set (Var "j")) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set  "("  ($#k17_sin_cos :::"sin"::: )  (Set (Var "r")) ")" ) ")" ) ")" )))))) ; 
 
theorem :: MATRTOP3:22 (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i"))) & (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "j"))) & (Bool (Set (Var "j"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n")))) "holds"  (Bool (Set (Set  "(" (Set  "("  ($#k3_matrtop1 :::"Mx2Tran"::: )  (Set  "("  ($#k2_matrtop3 :::"Rotation"::: )   "(" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "n")) "," (Set (Var "r")) ")"  ")" ) ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "p")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "j")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set (Var "p"))  ($#k1_seq_1 :::"."::: )  (Set (Var "i")) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "("  ($#k17_sin_cos :::"sin"::: )  (Set (Var "r")) ")" ) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "(" (Set (Var "p"))  ($#k1_seq_1 :::"."::: )  (Set (Var "j")) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "("  ($#k20_sin_cos :::"cos"::: )  (Set (Var "r")) ")" ) ")" )))))) ; 
 
theorem :: MATRTOP3:23 (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i"))) & (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "j"))) & (Bool (Set (Var "j"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n")))) "holds"  (Bool (Set (Set  "("  ($#k3_matrtop1 :::"Mx2Tran"::: )  (Set  "("  ($#k2_matrtop3 :::"Rotation"::: )   "(" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "n")) "," (Set (Var "r")) ")"  ")" ) ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "(" (Set  "(" (Set (Var "p"))  ($#k16_finseq_1 :::"|"::: )  (Set  "(" (Set (Var "i"))  ($#k7_nat_d :::"-'"::: )  (Num 1) ")" ) ")" )  ($#k7_finseq_1 :::"^"::: )  (Set  ($#k4_matrix_2 :::"<*"::: ) (Set  "(" (Set  "(" (Set  "(" (Set (Var "p"))  ($#k1_seq_1 :::"."::: )  (Set (Var "i")) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "("  ($#k20_sin_cos :::"cos"::: )  (Set (Var "r")) ")" ) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "(" (Set (Var "p"))  ($#k1_seq_1 :::"."::: )  (Set (Var "j")) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set  "("  ($#k17_sin_cos :::"sin"::: )  (Set (Var "r")) ")" ) ")" ) ")" ) ")" ) ($#k4_matrix_2 :::"*>"::: ) ) ")" )  ($#k7_finseq_1 :::"^"::: )  (Set  "(" (Set  "(" (Set (Var "p"))  ($#k1_rfinseq :::"/^"::: )  (Set (Var "i")) ")" )  ($#k16_finseq_1 :::"|"::: )  (Set  "(" (Set  "(" (Set (Var "j"))  ($#k7_nat_d :::"-'"::: )  (Set (Var "i")) ")" )  ($#k7_nat_d :::"-'"::: )  (Num 1) ")" ) ")" ) ")" )  ($#k7_finseq_1 :::"^"::: )  (Set  ($#k4_matrix_2 :::"<*"::: ) (Set  "(" (Set  "(" (Set  "(" (Set (Var "p"))  ($#k1_seq_1 :::"."::: )  (Set (Var "i")) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "("  ($#k17_sin_cos :::"sin"::: )  (Set (Var "r")) ")" ) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "(" (Set (Var "p"))  ($#k1_seq_1 :::"."::: )  (Set (Var "j")) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "("  ($#k20_sin_cos :::"cos"::: )  (Set (Var "r")) ")" ) ")" ) ")" ) ($#k4_matrix_2 :::"*>"::: ) ) ")" )  ($#k7_finseq_1 :::"^"::: )  (Set  "(" (Set (Var "p"))  ($#k1_rfinseq :::"/^"::: )  (Set (Var "j")) ")" )))))) ; 
 
theorem :: MATRTOP3:24 (Bool  "for" (Set (Var "s")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i"))) & (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "j"))) & (Bool (Set (Var "j"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n"))) & (Bool (Set (Set (Var "s"))  ($#k3_square_1 :::"^2"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "(" (Set  "(" (Set (Var "p"))  ($#k1_seq_1 :::"."::: )  (Set (Var "i")) ")" )  ($#k5_square_1 :::"^2"::: )  ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "(" (Set (Var "p"))  ($#k1_seq_1 :::"."::: )  (Set (Var "j")) ")" )  ($#k5_square_1 :::"^2"::: )  ")" )))) "holds"  (Bool  "ex" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "st" (Bool (Set (Set  "(" (Set  "("  ($#k3_matrtop1 :::"Mx2Tran"::: )  (Set  "("  ($#k2_matrtop3 :::"Rotation"::: )   "(" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "n")) "," (Set (Var "r")) ")"  ")" ) ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "p")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "i")))  ($#r1_hidden :::"="::: )  (Set (Var "s"))))))) ; 
 
theorem :: MATRTOP3:25 (Bool  "for" (Set (Var "s")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i"))) & (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "j"))) & (Bool (Set (Var "j"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n"))) & (Bool (Set (Set (Var "s"))  ($#k3_square_1 :::"^2"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "(" (Set  "(" (Set (Var "p"))  ($#k1_seq_1 :::"."::: )  (Set (Var "i")) ")" )  ($#k5_square_1 :::"^2"::: )  ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "(" (Set (Var "p"))  ($#k1_seq_1 :::"."::: )  (Set (Var "j")) ")" )  ($#k5_square_1 :::"^2"::: )  ")" )))) "holds"  (Bool  "ex" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "st" (Bool (Set (Set  "(" (Set  "("  ($#k3_matrtop1 :::"Mx2Tran"::: )  (Set  "("  ($#k2_matrtop3 :::"Rotation"::: )   "(" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "n")) "," (Set (Var "r")) ")"  ")" ) ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "p")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "j")))  ($#r1_hidden :::"="::: )  (Set (Var "s"))))))) ; 
 
theorem :: MATRTOP3:26 (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i"))) & (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "j"))) & (Bool (Set (Var "j"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n")))) "holds"  (Bool (Set   ($#k3_matrtop1 :::"Mx2Tran"::: )  (Set  "("  ($#k2_matrtop3 :::"Rotation"::: )   "(" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "n")) "," (Set (Var "r")) ")"  ")" )) "is" (Set  ($#k4_matrix13 :::"{"::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k4_matrix13 :::"}"::: ) )  ($#v1_matrtop3 :::"-support-yielding"::: )  ))) ; 
 begin  definitionlet "n" be   ($#m1_hidden :::"Nat":::); let "f" be   ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Const "n")) ")" ) "," (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Const "n")) ")" ); attr "f" is  :::"rotation":::  means :: MATRTOP3:def 4 (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  "n" ")" ) "holds"  (Bool (Set  ($#k12_euclid :::"|."::: ) (Set (Var "p")) ($#k12_euclid :::".|"::: ) )  ($#r1_hidden :::"="::: )  (Set  ($#k12_euclid :::"|."::: ) (Set  "(" "f"  ($#k3_funct_2 :::"."::: )  (Set (Var "p")) ")" ) ($#k12_euclid :::".|"::: ) ))); end; 





:: deftheorem    defines :::"rotation"::: MATRTOP3:def 4 :  (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" ) "," (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" ) "holds"   (Bool  "("  (Bool (Set (Var "f")) "is"   ($#v2_matrtop3 :::"rotation"::: )  ) "iff" (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" ) "holds"  (Bool (Set  ($#k12_euclid :::"|."::: ) (Set (Var "p")) ($#k12_euclid :::".|"::: ) )  ($#r1_hidden :::"="::: )  (Set  ($#k12_euclid :::"|."::: ) (Set  "(" (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "p")) ")" ) ($#k12_euclid :::".|"::: ) )))  ")" ))); 
 
theorem :: MATRTOP3:27 (Bool  "for" (Set (Var "i")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_finseq_1 :::"Seg"::: )  (Set (Var "n"))))) "holds"  (Bool (Set   ($#k3_matrtop1 :::"Mx2Tran"::: )  (Set  "("  ($#k1_matrtop3 :::"AxialSymmetry"::: )   "(" (Set (Var "i")) "," (Set (Var "n")) ")"  ")" )) "is"   ($#v2_matrtop3 :::"rotation"::: )  )) ; 
 definitionlet "n" be   ($#m1_hidden :::"Nat":::); let "f" be   ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Const "n")) ")" ) "," (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Const "n")) ")" ); attr "f" is  :::"base_rotation":::  means :: MATRTOP3:def 5 (Bool  "ex" (Set (Var "F")) "being"   ($#m2_finseq_1 :::"FinSequence":::) "of" (Set  "("  ($#k15_monoid_0 :::"GFuncs"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  "n" ")" )) ")" ) "st"  (Bool  "("  (Bool "f"  ($#r1_hidden :::"="::: )  (Set   ($#k3_group_4 :::"Product"::: )  (Set (Var "F")))) & (Bool  "("   "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "k"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "F"))))) "holds"  (Bool  "ex" (Set (Var "i")) "," (Set (Var "j")) "being"   ($#m1_hidden :::"Nat":::)(Bool  "ex" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "st"  (Bool  "("  (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i"))) & (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "j"))) & (Bool (Set (Var "j"))  ($#r1_xxreal_0 :::"<="::: )  "n") & (Bool (Set (Set (Var "F"))  ($#k1_funct_1 :::"."::: )  (Set (Var "k")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_matrtop1 :::"Mx2Tran"::: )  (Set  "("  ($#k2_matrtop3 :::"Rotation"::: )   "(" (Set (Var "i")) "," (Set (Var "j")) "," "n" "," (Set (Var "r")) ")"  ")" )))  ")" )))  ")" )  ")" )); end; 





:: deftheorem    defines :::"base_rotation"::: MATRTOP3:def 5 :  (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" ) "," (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" ) "holds"   (Bool  "("  (Bool (Set (Var "f")) "is"   ($#v3_matrtop3 :::"base_rotation"::: )  ) "iff" (Bool  "ex" (Set (Var "F")) "being"   ($#m2_finseq_1 :::"FinSequence":::) "of" (Set  "("  ($#k15_monoid_0 :::"GFuncs"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )) ")" ) "st"  (Bool  "("  (Bool (Set (Var "f"))  ($#r1_hidden :::"="::: )  (Set   ($#k3_group_4 :::"Product"::: )  (Set (Var "F")))) & (Bool  "("   "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "k"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "F"))))) "holds"  (Bool  "ex" (Set (Var "i")) "," (Set (Var "j")) "being"   ($#m1_hidden :::"Nat":::)(Bool  "ex" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "st"  (Bool  "("  (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i"))) & (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "j"))) & (Bool (Set (Var "j"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n"))) & (Bool (Set (Set (Var "F"))  ($#k1_funct_1 :::"."::: )  (Set (Var "k")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_matrtop1 :::"Mx2Tran"::: )  (Set  "("  ($#k2_matrtop3 :::"Rotation"::: )   "(" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "n")) "," (Set (Var "r")) ")"  ")" )))  ")" )))  ")" )  ")" ))  ")" ))); 
 registrationlet "n" be   ($#m1_hidden :::"Nat":::); 
cluster (Set   ($#k3_struct_0 :::"id"::: )  (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  "n" ")" )) ->   ($#v3_matrtop3 :::"base_rotation"::: )   ; 
end; registrationlet "n" be   ($#m1_hidden :::"Nat":::); 
cluster  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v1_relat_1 :::"Relation-like"::: )   (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  "n" ")" ))  ($#v4_relat_1 :::"-defined"::: )   (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  "n" ")" ))  ($#v5_relat_1 :::"-valued"::: )     ($#v1_funct_1 :::"Function-like"::: )     ($#v1_partfun1 :::"total"::: )     ($#v1_funct_2 :::"quasi_total"::: )     ($#v1_pre_poly :::"FinSequence-yielding"::: )     ($#v1_funcop_1 :::"Function-yielding"::: )   bbbadV2_FUNCOP_1()   ($#v3_matrtop3 :::"base_rotation"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_zfmisc_1 :::"bool"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  "n" ")" )) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  "n" ")" )) ($#k2_zfmisc_1 :::":]"::: ) )); 
end; registrationlet "n" be   ($#m1_hidden :::"Nat":::); let "f", "g" be   ($#v3_matrtop3 :::"base_rotation"::: )    ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Const "n")) ")" ) "," (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Const "n")) ")" ); 
cluster (Set "g"  ($#k3_relat_1 :::"(#)"::: )  "f") ->   ($#v3_matrtop3 :::"base_rotation"::: )    for  ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  "n" ")" ) "," (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  "n" ")" ); 
end; 
theorem :: MATRTOP3:28 (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i"))) & (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "j"))) & (Bool (Set (Var "j"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n")))) "holds"  (Bool (Set   ($#k3_matrtop1 :::"Mx2Tran"::: )  (Set  "("  ($#k2_matrtop3 :::"Rotation"::: )   "(" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "n")) "," (Set (Var "r")) ")"  ")" )) "is"   ($#v3_matrtop3 :::"base_rotation"::: )  ))) ; 
 registrationlet "n" be   ($#m1_hidden :::"Nat":::); 
cluster   ($#v1_funct_1 :::"Function-like"::: )     ($#v1_funct_2 :::"quasi_total"::: )     ($#v3_matrtop3 :::"base_rotation"::: )    ->   ($#v13_vectsp_1 :::"additive"::: )     ($#v1_topreal9 :::"homogeneous"::: )     ($#v3_tops_2 :::"being_homeomorphism"::: )     ($#v2_matrtop3 :::"rotation"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_zfmisc_1 :::"bool"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  "n" ")" )) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  "n" ")" )) ($#k2_zfmisc_1 :::":]"::: ) )); 
end; registrationlet "n" be   ($#m1_hidden :::"Nat":::); let "f" be   ($#v3_matrtop3 :::"base_rotation"::: )    ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Const "n")) ")" ) "," (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Const "n")) ")" ); 
cluster (Set "f"  ($#k2_tops_2 :::"/""::: )  ) ->   ($#v3_matrtop3 :::"base_rotation"::: )   ; 
end; registrationlet "n" be   ($#m1_hidden :::"Nat":::); let "f", "g" be   ($#v2_matrtop3 :::"rotation"::: )    ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Const "n")) ")" ) "," (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Const "n")) ")" ); 
cluster (Set "g"  ($#k3_relat_1 :::"(#)"::: )  "f") ->   ($#v2_matrtop3 :::"rotation"::: )    for  ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  "n" ")" ) "," (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  "n" ")" ); 
end; 




definitionlet "n" be   ($#m1_hidden :::"Nat":::); let "f" be   ($#v13_vectsp_1 :::"additive"::: )     ($#v1_topreal9 :::"homogeneous"::: )    ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Const "n")) ")" ) "," (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Const "n")) ")" ); func  :::"AutMt"::: "f" ->   ($#m1_matrix_1 :::"Matrix":::) "of" "n" "," (Set  ($#k2_vectsp_1 :::"F_Real"::: ) ) means :: MATRTOP3:def 6 (Bool "f"  ($#r2_funct_2 :::"="::: )  (Set   ($#k3_matrtop1 :::"Mx2Tran"::: )  it)); end; 






:: deftheorem    defines :::"AutMt"::: MATRTOP3:def 6 :  (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "f")) "being"   ($#v13_vectsp_1 :::"additive"::: )     ($#v1_topreal9 :::"homogeneous"::: )    ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" ) "," (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  (Bool  "for" (Set (Var "b3")) "being"   ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set  ($#k2_vectsp_1 :::"F_Real"::: ) ) "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k3_matrtop3 :::"AutMt"::: )  (Set (Var "f")))) "iff" (Bool (Set (Var "f"))  ($#r2_funct_2 :::"="::: )  (Set   ($#k3_matrtop1 :::"Mx2Tran"::: )  (Set (Var "b3"))))  ")" )))); 
 
theorem :: MATRTOP3:29 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "f1")) "," (Set (Var "f2")) "being"   ($#v13_vectsp_1 :::"additive"::: )     ($#v1_topreal9 :::"homogeneous"::: )    ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" ) "," (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" ) "holds"  (Bool (Set   ($#k3_matrtop3 :::"AutMt"::: )  (Set  "(" (Set (Var "f1"))  ($#k1_partfun1 :::"*"::: )  (Set (Var "f2")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k3_matrtop3 :::"AutMt"::: )  (Set (Var "f2")) ")" )  ($#k4_matrix_6 :::"*"::: )  (Set  "("  ($#k3_matrtop3 :::"AutMt"::: )  (Set (Var "f1")) ")" ))))) ; 
 
theorem :: MATRTOP3:30 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "k")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  "st" (Bool (Bool (Set (Var "k"))  ($#r2_hidden :::"in"::: )  (Set (Var "X"))) & (Bool (Set (Var "k"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_finseq_1 :::"Seg"::: )  (Set (Var "n"))))) "holds"  (Bool  "ex" (Set (Var "f")) "being"   ($#v13_vectsp_1 :::"additive"::: )     ($#v1_topreal9 :::"homogeneous"::: )    ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" ) "," (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" ) "st"  (Bool  "("  (Bool (Set (Var "f")) "is" (Set (Var "X"))  ($#v1_matrtop3 :::"-support-yielding"::: )  ) & (Bool (Set (Var "f")) "is"   ($#v3_matrtop3 :::"base_rotation"::: )  ) &  "("  (Bool (Bool (Set   ($#k5_card_1 :::"card"::: )  (Set  "(" (Set (Var "X"))  ($#k9_subset_1 :::"/\"::: )  (Set  "("  ($#k2_finseq_1 :::"Seg"::: )  (Set (Var "n")) ")" ) ")" ))  ($#r1_xxreal_0 :::">"::: )  (Num 1))) "implies" (Bool (Set (Set  "(" (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "p")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "k")))  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k1_xboole_0 :::"0"::: )  ))  ")"  & (Bool  "("   "for" (Set (Var "i")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set (Set (Var "X"))  ($#k9_subset_1 :::"/\"::: )  (Set  "("  ($#k2_finseq_1 :::"Seg"::: )  (Set (Var "n")) ")" ))) & (Bool (Set (Var "i"))  ($#r1_hidden :::"<>"::: )  (Set (Var "k")))) "holds"  (Bool (Set (Set  "(" (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "p")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "i")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"0"::: )  ))  ")" )  ")" ))))) ; 
 
theorem :: MATRTOP3:31 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "f")) "being"   ($#v13_vectsp_1 :::"additive"::: )     ($#v1_topreal9 :::"homogeneous"::: )    ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" ) "," (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  "st" (Bool (Bool (Set (Set (Var "f"))  ($#k2_partfun1 :::"|"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_partfun1 :::"id"::: )  (Set (Var "A"))))) "holds"  (Bool (Set (Set (Var "f"))  ($#k2_tmap_1 :::"|"::: )  (Set  "("  ($#k1_rlvect_3 :::"Lin"::: )  (Set (Var "A")) ")" ))  ($#r1_funct_2 :::"="::: )  (Set   ($#k3_struct_0 :::"id"::: )  (Set  "("  ($#k1_rlvect_3 :::"Lin"::: )  (Set (Var "A")) ")" )))))) ; 
 
theorem :: MATRTOP3:32 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  (Bool  "for" (Set (Var "f")) "being"   ($#v13_vectsp_1 :::"additive"::: )     ($#v1_topreal9 :::"homogeneous"::: )    ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" ) "," (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  "st" (Bool (Bool (Set (Var "f")) "is"   ($#v2_matrtop3 :::"rotation"::: )  ) & (Bool (Set (Set (Var "f"))  ($#k2_partfun1 :::"|"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_partfun1 :::"id"::: )  (Set (Var "A"))))) "holds"  (Bool  "for" (Set (Var "i")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_finseq_1 :::"Seg"::: )  (Set (Var "n")))) & (Bool (Set   ($#k6_matrixr2 :::"Base_FinSeq"::: )   "(" (Set (Var "n")) "," (Set (Var "i")) ")" )  ($#r1_struct_0 :::"in"::: )  (Set   ($#k1_rlvect_3 :::"Lin"::: )  (Set (Var "A"))))) "holds"  (Bool (Set (Set  "(" (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "p")) ")" )  ($#k1_seq_1 :::"."::: )  (Set (Var "i")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "p"))  ($#k1_seq_1 :::"."::: )  (Set (Var "i"))))))))) ; 
 
theorem :: MATRTOP3:33 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  (Bool  "for" (Set (Var "f")) "being"   ($#v2_matrtop3 :::"rotation"::: )    ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" ) "," (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  "st" (Bool (Bool (Set (Var "f")) "is" (Set (Var "X"))  ($#v1_matrtop3 :::"-support-yielding"::: )  ) & (Bool  "("   "for" (Set (Var "i")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set (Set (Var "X"))  ($#k9_subset_1 :::"/\"::: )  (Set  "("  ($#k2_finseq_1 :::"Seg"::: )  (Set (Var "n")) ")" )))) "holds"  (Bool (Set (Set (Var "p"))  ($#k1_seq_1 :::"."::: )  (Set (Var "i")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"0"::: )  ))  ")" )) "holds"  (Bool (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set (Var "p"))))))) ; 
 
theorem :: MATRTOP3:34 (Bool  "for" (Set (Var "i")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  "st" (Bool (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_finseq_1 :::"Seg"::: )  (Set (Var "n")))) & (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">="::: )  (Num 2))) "holds"  (Bool  "ex" (Set (Var "f")) "being"   ($#v13_vectsp_1 :::"additive"::: )     ($#v1_topreal9 :::"homogeneous"::: )    ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" ) "," (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" ) "st"  (Bool  "("  (Bool (Set (Var "f")) "is"   ($#v3_matrtop3 :::"base_rotation"::: )  ) & (Bool (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "p"))  ($#k2_funct_7 :::"+*"::: )   "(" (Set (Var "i")) "," (Set  "("  ($#k1_real_1 :::"-"::: )  (Set  "(" (Set (Var "p"))  ($#k1_seq_1 :::"."::: )  (Set (Var "i")) ")" ) ")" ) ")" ))  ")" )))) ; 
 
theorem :: MATRTOP3:35 (Bool  "for" (Set (Var "i")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "f")) "being"   ($#v13_vectsp_1 :::"additive"::: )     ($#v1_topreal9 :::"homogeneous"::: )    ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" ) "," (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  "st" (Bool (Bool (Set (Var "f")) "is" (Set  ($#k3_matrix13 :::"{"::: ) (Set (Var "i")) ($#k3_matrix13 :::"}"::: ) )  ($#v1_matrtop3 :::"-support-yielding"::: )  ) & (Bool (Set (Var "f")) "is"   ($#v2_matrtop3 :::"rotation"::: )  ) & (Bool (Bool  "not" (Set   ($#k3_matrtop3 :::"AutMt"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_matrtop3 :::"AxialSymmetry"::: )   "(" (Set (Var "i")) "," (Set (Var "n")) ")" )))) "holds"  (Bool (Set   ($#k3_matrtop3 :::"AutMt"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set   ($#k12_matrix_1 :::"1."::: )   "(" (Set  ($#k2_vectsp_1 :::"F_Real"::: ) ) "," (Set (Var "n")) ")" )))) ; 
 
theorem :: MATRTOP3:36 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "f1")) "being"   ($#v13_vectsp_1 :::"additive"::: )     ($#v1_topreal9 :::"homogeneous"::: )    ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" ) "," (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  "st" (Bool (Bool (Set (Var "f1")) "is"   ($#v2_matrtop3 :::"rotation"::: )  )) "holds"  (Bool  "ex" (Set (Var "f2")) "being"   ($#v13_vectsp_1 :::"additive"::: )     ($#v1_topreal9 :::"homogeneous"::: )    ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" ) "," (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" ) "st"  (Bool  "("  (Bool (Set (Var "f2")) "is"   ($#v3_matrtop3 :::"base_rotation"::: )  ) & (Bool (Set (Set (Var "f2"))  ($#k1_partfun1 :::"*"::: )  (Set (Var "f1"))) "is" (Set  ($#k3_matrix13 :::"{"::: ) (Set (Var "n")) ($#k3_matrix13 :::"}"::: ) )  ($#v1_matrtop3 :::"-support-yielding"::: )  )  ")" )))) ; 
 begin  
theorem :: MATRTOP3:37 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "f")) "being"   ($#v13_vectsp_1 :::"additive"::: )     ($#v1_topreal9 :::"homogeneous"::: )    ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" ) "," (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  "st" (Bool (Bool (Set (Var "f")) "is"   ($#v2_matrtop3 :::"rotation"::: )  )) "holds"  (Bool  "("  (Bool (Set   ($#k12_matrix_3 :::"Det"::: )  (Set  "("  ($#k3_matrtop3 :::"AutMt"::: )  (Set (Var "f")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k5_struct_0 :::"1."::: )  (Set  ($#k2_vectsp_1 :::"F_Real"::: ) ))) "iff" (Bool (Set (Var "f")) "is"   ($#v3_matrtop3 :::"base_rotation"::: )  )  ")" ))) ; 
 
theorem :: MATRTOP3:38 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "f")) "being"   ($#v13_vectsp_1 :::"additive"::: )     ($#v1_topreal9 :::"homogeneous"::: )    ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" ) "," (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  "holds"  (Bool  "("   "not" (Bool (Set (Var "f")) "is"   ($#v2_matrtop3 :::"rotation"::: )  ) "or" (Bool (Set   ($#k12_matrix_3 :::"Det"::: )  (Set  "("  ($#k3_matrtop3 :::"AutMt"::: )  (Set (Var "f")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k5_struct_0 :::"1."::: )  (Set  ($#k2_vectsp_1 :::"F_Real"::: ) ))) "or" (Bool (Set   ($#k12_matrix_3 :::"Det"::: )  (Set  "("  ($#k3_matrtop3 :::"AutMt"::: )  (Set (Var "f")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k4_algstr_0 :::"-"::: )  (Set  "("  ($#k5_struct_0 :::"1."::: )  (Set  ($#k2_vectsp_1 :::"F_Real"::: ) ) ")" )))  ")" ))) ; 
 
theorem :: MATRTOP3:39 (Bool  "for" (Set (Var "i")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "f1")) "," (Set (Var "f2")) "being"   ($#v13_vectsp_1 :::"additive"::: )     ($#v1_topreal9 :::"homogeneous"::: )    ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" ) "," (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  "st" (Bool (Bool (Set (Var "f1")) "is"   ($#v2_matrtop3 :::"rotation"::: )  ) & (Bool (Set   ($#k12_matrix_3 :::"Det"::: )  (Set  "("  ($#k3_matrtop3 :::"AutMt"::: )  (Set (Var "f1")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k4_algstr_0 :::"-"::: )  (Set  "("  ($#k5_struct_0 :::"1."::: )  (Set  ($#k2_vectsp_1 :::"F_Real"::: ) ) ")" ))) & (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_finseq_1 :::"Seg"::: )  (Set (Var "n")))) & (Bool (Set   ($#k3_matrtop3 :::"AutMt"::: )  (Set (Var "f2")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_matrtop3 :::"AxialSymmetry"::: )   "(" (Set (Var "i")) "," (Set (Var "n")) ")" ))) "holds"  (Bool (Set (Set (Var "f1"))  ($#k1_partfun1 :::"*"::: )  (Set (Var "f2"))) "is"   ($#v3_matrtop3 :::"base_rotation"::: )  ))) ; 
 registrationlet "n" be   ($#m1_hidden :::"Nat":::); let "f" be   ($#v13_vectsp_1 :::"additive"::: )     ($#v1_topreal9 :::"homogeneous"::: )     ($#v2_matrtop3 :::"rotation"::: )    ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Const "n")) ")" ) "," (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Const "n")) ")" ); 
cluster (Set   ($#k3_matrtop3 :::"AutMt"::: )  "f") ->   ($#v4_matrix_6 :::"Orthogonal"::: )   ; 
end; registrationlet "n" be   ($#m1_hidden :::"Nat":::); 
cluster   ($#v1_funct_1 :::"Function-like"::: )     ($#v1_funct_2 :::"quasi_total"::: )     ($#v13_vectsp_1 :::"additive"::: )     ($#v1_topreal9 :::"homogeneous"::: )     ($#v2_matrtop3 :::"rotation"::: )    ->   ($#v3_tops_2 :::"being_homeomorphism"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_zfmisc_1 :::"bool"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  "n" ")" )) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  "n" ")" )) ($#k2_zfmisc_1 :::":]"::: ) )); 
end; begin  
theorem :: MATRTOP3:40 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  "st" (Bool (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Num 1)) & (Bool (Set  ($#k12_euclid :::"|."::: ) (Set (Var "p")) ($#k12_euclid :::".|"::: ) )  ($#r1_hidden :::"="::: )  (Set  ($#k12_euclid :::"|."::: ) (Set (Var "q")) ($#k12_euclid :::".|"::: ) ))) "holds"  (Bool  "ex" (Set (Var "f")) "being"   ($#v13_vectsp_1 :::"additive"::: )     ($#v1_topreal9 :::"homogeneous"::: )    ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" ) "," (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" ) "st"  (Bool  "("  (Bool (Set (Var "f")) "is"   ($#v2_matrtop3 :::"rotation"::: )  ) & (Bool (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set (Var "q"))) & (Bool  "("  (Bool (Set   ($#k3_matrtop3 :::"AutMt"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_matrtop3 :::"AxialSymmetry"::: )   "(" (Set (Var "n")) "," (Set (Var "n")) ")" )) "or" (Bool (Set   ($#k3_matrtop3 :::"AutMt"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set   ($#k12_matrix_1 :::"1."::: )   "(" (Set  ($#k2_vectsp_1 :::"F_Real"::: ) ) "," (Set (Var "n")) ")" ))  ")" )  ")" )))) ; 
 
theorem :: MATRTOP3:41 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  "st" (Bool (Bool (Set (Var "n"))  ($#r1_hidden :::"<>"::: )  (Num 1)) & (Bool (Set  ($#k12_euclid :::"|."::: ) (Set (Var "p")) ($#k12_euclid :::".|"::: ) )  ($#r1_hidden :::"="::: )  (Set  ($#k12_euclid :::"|."::: ) (Set (Var "q")) ($#k12_euclid :::".|"::: ) ))) "holds"  (Bool  "ex" (Set (Var "f")) "being"   ($#v13_vectsp_1 :::"additive"::: )     ($#v1_topreal9 :::"homogeneous"::: )    ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" ) "," (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" ) "st"  (Bool  "("  (Bool (Set (Var "f")) "is"   ($#v3_matrtop3 :::"base_rotation"::: )  ) & (Bool (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set (Var "q")))  ")" )))) ;