:: RLAFFIN3  semantic presentation begin  


























theorem :: RLAFFIN3:1 (Bool  "for" (Set (Var "f1")) "," (Set (Var "f2")) "being"   ($#v3_valued_0 :::"real-valued"::: )    ($#m1_hidden :::"FinSequence":::)  (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "("  ($#k3_euclid_9 :::"Intervals"::: )   "(" (Set (Var "f1")) "," (Set (Var "r")) ")"  ")" )  ($#k7_finseq_1 :::"^"::: )  (Set  "("  ($#k3_euclid_9 :::"Intervals"::: )   "(" (Set (Var "f2")) "," (Set (Var "r")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k3_euclid_9 :::"Intervals"::: )   "(" (Set  "(" (Set (Var "f1"))  ($#k7_finseq_1 :::"^"::: )  (Set (Var "f2")) ")" ) "," (Set (Var "r")) ")" )))) ; 
 
theorem :: RLAFFIN3:2 (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f1")) "," (Set (Var "f2")) "being"   ($#m1_hidden :::"FinSequence":::) "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_card_3 :::"product"::: )  (Set  "(" (Set (Var "f1"))  ($#k7_finseq_1 :::"^"::: )  (Set (Var "f2")) ")" ))) "iff" (Bool  "ex" (Set (Var "p1")) "," (Set (Var "p2")) "being"   ($#m1_hidden :::"FinSequence":::) "st"  (Bool  "("  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "p1"))  ($#k7_finseq_1 :::"^"::: )  (Set (Var "p2")))) & (Bool (Set (Var "p1"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_card_3 :::"product"::: )  (Set (Var "f1")))) & (Bool (Set (Var "p2"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_card_3 :::"product"::: )  (Set (Var "f2"))))  ")" ))  ")" ))) ; 
 
theorem :: RLAFFIN3:3 (Bool  "for" (Set (Var "V")) "being"   ($#l1_rlvect_1 :::"RealLinearSpace":::) "holds"   (Bool  "("  (Bool (Set (Var "V")) "is"   ($#v1_rlvect_5 :::"finite-dimensional"::: )  ) "iff" (Bool (Set   ($#k2_rlsub_1 :::"(Omega)."::: )  (Set (Var "V"))) "is"   ($#v1_rlvect_5 :::"finite-dimensional"::: )  )  ")" )) ; 
 registrationlet "V" be   ($#v1_rlvect_5 :::"finite-dimensional"::: )    ($#l1_rlvect_1 :::"RealLinearSpace":::); 
cluster   ($#v1_rlaffin1 :::"affinely-independent"::: )    ->   ($#v1_finset_1 :::"finite"::: )     ($#v1_rlaffin1 :::"affinely-independent"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_zfmisc_1 :::"bool"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "V")); 
end; registrationlet "n" be   ($#m1_hidden :::"Nat":::); 
cluster (Set   ($#k15_euclid :::"TOP-REAL"::: )  "n") ->   ($#v6_rltopsp1 :::"add-continuous"::: )     ($#v7_rltopsp1 :::"Mult-continuous"::: )   ; 

cluster (Set   ($#k15_euclid :::"TOP-REAL"::: )  "n") ->   ($#v1_rlvect_5 :::"finite-dimensional"::: )   ; 
end; 












theorem :: RLAFFIN3:4 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set   ($#k1_rlvect_5 :::"dim"::: )  (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "n")))) ; 
 
theorem :: RLAFFIN3:5 (Bool  "for" (Set (Var "V")) "being"   ($#v1_rlvect_5 :::"finite-dimensional"::: )    ($#l1_rlvect_1 :::"RealLinearSpace":::)  (Bool  "for" (Set (Var "A")) "being"   ($#v1_rlaffin1 :::"affinely-independent"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "holds"  (Bool (Set   ($#k5_card_1 :::"card"::: )  (Set (Var "A")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Num 1)  ($#k23_binop_2 :::"+"::: )  (Set  "("  ($#k1_rlvect_5 :::"dim"::: )  (Set (Var "V")) ")" ))))) ; 
 
theorem :: RLAFFIN3:6 (Bool  "for" (Set (Var "V")) "being"   ($#v1_rlvect_5 :::"finite-dimensional"::: )    ($#l1_rlvect_1 :::"RealLinearSpace":::)  (Bool  "for" (Set (Var "A")) "being"   ($#v1_rlaffin1 :::"affinely-independent"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "holds"   (Bool  "("  (Bool (Set   ($#k5_card_1 :::"card"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k1_rlvect_5 :::"dim"::: )  (Set (Var "V")) ")" )  ($#k23_binop_2 :::"+"::: )  (Num 1))) "iff" (Bool (Set   ($#k4_rlaffin1 :::"Affin"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_struct_0 :::"[#]"::: )  (Set (Var "V"))))  ")" ))) ; 
 begin  
theorem :: RLAFFIN3:7 (Bool  "for" (Set (Var "k")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "An")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  (Bool  "for" (Set (Var "Ak")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "k")) ")" )  "st" (Bool (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n"))) & (Bool (Set (Var "An"))  ($#r1_hidden :::"="::: )   "{"  (Set (Var "v")) where v "is"   ($#m1_subset_1 :::"Element":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" ) : (Bool (Set (Set (Var "v"))  ($#k16_finseq_1 :::"|"::: )  (Set (Var "k")))  ($#r2_hidden :::"in"::: )  (Set (Var "Ak")))  "}"  )) "holds"  (Bool  "("  (Bool (Set (Var "An")) "is"   ($#v3_pre_topc :::"open"::: )  ) "iff" (Bool (Set (Var "Ak")) "is"   ($#v3_pre_topc :::"open"::: )  )  ")" )))) ; 
 
theorem :: RLAFFIN3:8 (Bool  "for" (Set (Var "k")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "Ak")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "k")) ")" )  (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set  "(" (Set (Var "k"))  ($#k23_binop_2 :::"+"::: )  (Set (Var "n")) ")" ) ")" )  "st" (Bool (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )   "{"  (Set  "(" (Set (Var "v"))  ($#k7_finseq_1 :::"^"::: )  (Set  "(" (Set (Var "n"))  ($#k2_finseq_2 :::"|->"::: )  (Set  ($#k1_xboole_0 :::"0"::: ) ) ")" ) ")" ) where v "is"   ($#m1_subset_1 :::"Element":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "k")) ")" ) : (Bool verum)  "}"  )) "holds"  (Bool  "for" (Set (Var "B")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "(" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set  "(" (Set (Var "k"))  ($#k23_binop_2 :::"+"::: )  (Set (Var "n")) ")" ) ")" )  ($#k1_pre_topc :::"|"::: )  (Set (Var "A")) ")" )  "st" (Bool (Bool (Set (Var "B"))  ($#r1_hidden :::"="::: )   "{"  (Set (Var "v")) where v "is"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set  "(" (Set (Var "k"))  ($#k23_binop_2 :::"+"::: )  (Set (Var "n")) ")" ) ")" ) : (Bool  "("  (Bool (Set (Set (Var "v"))  ($#k16_finseq_1 :::"|"::: )  (Set (Var "k")))  ($#r2_hidden :::"in"::: )  (Set (Var "Ak"))) & (Bool (Set (Var "v"))  ($#r2_hidden :::"in"::: )  (Set (Var "A")))  ")" )  "}"  )) "holds"  (Bool  "("  (Bool (Set (Var "Ak")) "is"   ($#v3_pre_topc :::"open"::: )  ) "iff" (Bool (Set (Var "B")) "is"   ($#v3_pre_topc :::"open"::: )  )  ")" ))))) ; 
 
theorem :: RLAFFIN3:9 (Bool  "for" (Set (Var "V")) "being"   ($#l1_rlvect_1 :::"RealLinearSpace":::)  (Bool  "for" (Set (Var "A")) "being"   ($#v1_rlaffin1 :::"affinely-independent"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V"))  (Bool  "for" (Set (Var "B")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V"))  "st" (Bool (Bool (Set (Var "B"))  ($#r1_tarski :::"c="::: )  (Set (Var "A")))) "holds"  (Bool (Set (Set  "("  ($#k3_convex1 :::"conv"::: )  (Set (Var "A")) ")" )  ($#k9_subset_1 :::"/\"::: )  (Set  "("  ($#k4_rlaffin1 :::"Affin"::: )  (Set (Var "B")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k3_convex1 :::"conv"::: )  (Set (Var "B"))))))) ; 
 
theorem :: RLAFFIN3:10 (Bool  "for" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "V")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_rlvect_1 :::"RLSStruct"::: )    (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "A")) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "V")))  (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set (Set  "(" (Set (Var "r"))  ($#k4_vfunct_1 :::"(#)"::: )  (Set (Var "f")) ")" )  ($#k7_relset_1 :::".:"::: )  (Set (Var "X")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "r"))  ($#k1_convex1 :::"*"::: )  (Set  "(" (Set (Var "f"))  ($#k7_relset_1 :::".:"::: )  (Set (Var "X")) ")" )))))))) ; 
 
theorem :: RLAFFIN3:11 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "An")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  "st" (Bool (Bool (Set   ($#k5_euclid :::"0*"::: )  (Set (Var "n")))  ($#r2_hidden :::"in"::: )  (Set (Var "An")))) "holds"  (Bool (Set   ($#k4_rlaffin1 :::"Affin"::: )  (Set (Var "An")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_struct_0 :::"[#]"::: )  (Set  "("  ($#k1_rlvect_3 :::"Lin"::: )  (Set (Var "An")) ")" ))))) ; 
 registrationlet "V" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l2_algstr_0 :::"addLoopStr"::: )  ; let "A" be   ($#v1_finset_1 :::"finite"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "V")); let "v" be   ($#m1_subset_1 :::"Element":::) "of" (Set (Const "V")); 
cluster (Set "v"  ($#k5_rusub_4 :::"+"::: )  "A") ->   ($#v1_finset_1 :::"finite"::: )   ; 
end; registrationlet "V" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_rlvect_1 :::"RLSStruct"::: )  ; let "A" be   ($#v1_finset_1 :::"finite"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "V")); let "r" be   ($#m1_subset_1 :::"Real":::); 
cluster (Set "r"  ($#k1_convex1 :::"*"::: )  "A") ->   ($#v1_finset_1 :::"finite"::: )   ; 
end; 
theorem :: RLAFFIN3:12 (Bool  "for" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "V")) "being"   ($#l1_rlvect_1 :::"RealLinearSpace":::)  (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V")) "holds"   (Bool  "("  (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set  "(" (Set (Var "r"))  ($#k1_convex1 :::"*"::: )  (Set (Var "A")) ")" ))) "iff" (Bool  "("  (Bool (Set (Var "r"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"0"::: )  )) "or" (Bool (Set (Var "A")) "is"   ($#v1_zfmisc_1 :::"trivial"::: )  )  ")" )  ")" )))) ; 
 registrationlet "V" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_rlvect_1 :::"RLSStruct"::: )  ; let "f" be   ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Const "V")); let "r" be   ($#m1_subset_1 :::"Real":::); 
cluster (Set "r"  ($#k4_vfunct_1 :::"(#)"::: )  "f") ->   ($#v1_finseq_1 :::"FinSequence-like"::: )   ; 
end; begin  definitionlet "X" be   ($#v1_finset_1 :::"finite"::: )     ($#m1_hidden :::"set"::: )  ; mode  :::"Enumeration":::  "of" "X" ->   ($#v2_funct_1 :::"one-to-one"::: )    ($#m1_hidden :::"FinSequence":::) means :: RLAFFIN3:def 1 (Bool (Set   ($#k10_xtuple_0 :::"rng"::: )  it)  ($#r1_hidden :::"="::: )  "X"); end; 





:: deftheorem    defines :::"Enumeration"::: RLAFFIN3:def 1 :  (Bool  "for" (Set (Var "X")) "being"   ($#v1_finset_1 :::"finite"::: )     ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "b2")) "being"   ($#v2_funct_1 :::"one-to-one"::: )    ($#m1_hidden :::"FinSequence":::) "holds"   (Bool  "("  (Bool (Set (Var "b2")) "is"    ($#m1_rlaffin3 :::"Enumeration"::: )   "of" (Set (Var "X"))) "iff" (Bool (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "b2")))  ($#r1_hidden :::"="::: )  (Set (Var "X")))  ")" ))); 
 definitionlet "X" be    ($#l1_struct_0 :::"1-sorted"::: )  ; let "A" be   ($#v1_finset_1 :::"finite"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "X")); :: original: :::"Enumeration"::: redefine mode  :::"Enumeration":::  "of" "A" ->   ($#v2_funct_1 :::"one-to-one"::: )    ($#m2_finseq_1 :::"FinSequence":::) "of" "X"; end; 






theorem :: RLAFFIN3:13 (Bool  "for" (Set (Var "V")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v13_algstr_0 :::"right_complementable"::: )     ($#v2_rlvect_1 :::"Abelian"::: )     ($#v3_rlvect_1 :::"add-associative"::: )     ($#v4_rlvect_1 :::"right_zeroed"::: )     ($#l2_algstr_0 :::"addLoopStr"::: )    (Bool  "for" (Set (Var "A")) "being"   ($#v1_finset_1 :::"finite"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V"))  (Bool  "for" (Set (Var "E")) "being"    ($#m2_rlaffin3 :::"Enumeration"::: )   "of" (Set (Var "A"))  (Bool  "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "holds"  (Bool (Set (Set (Var "E"))  ($#k3_fvsum_1 :::"+"::: )  (Set  "(" (Set  "("  ($#k5_card_1 :::"card"::: )  (Set (Var "A")) ")" )  ($#k5_finseq_2 :::"|->"::: )  (Set (Var "v")) ")" )) "is"    ($#m2_rlaffin3 :::"Enumeration"::: )   "of" (Set (Set (Var "v"))  ($#k5_rusub_4 :::"+"::: )  (Set (Var "A")))))))) ; 
 
theorem :: RLAFFIN3:14 (Bool  "for" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "V")) "being"   ($#l1_rlvect_1 :::"RealLinearSpace":::)  (Bool  "for" (Set (Var "Av")) "being"   ($#v1_finset_1 :::"finite"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V"))  (Bool  "for" (Set (Var "E")) "being"    ($#m2_rlaffin3 :::"Enumeration"::: )   "of" (Set (Var "Av")) "holds"   (Bool  "("  (Bool (Set (Set (Var "r"))  ($#k4_vfunct_1 :::"(#)"::: )  (Set (Var "E"))) "is"    ($#m2_rlaffin3 :::"Enumeration"::: )   "of" (Set (Set (Var "r"))  ($#k1_convex1 :::"*"::: )  (Set (Var "Av")))) "iff" (Bool  "("  (Bool (Set (Var "r"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"0"::: )  )) "or" (Bool (Set (Var "Av")) "is"   ($#v1_zfmisc_1 :::"trivial"::: )  )  ")" )  ")" ))))) ; 
 
theorem :: RLAFFIN3:15 (Bool  "for" (Set (Var "n")) "," (Set (Var "m")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "M")) "being"   ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "m")) "," (Set  ($#k2_vectsp_1 :::"F_Real"::: ) )  "st" (Bool (Bool (Set   ($#k8_matrix13 :::"the_rank_of"::: )  (Set (Var "M")))  ($#r1_hidden :::"="::: )  (Set (Var "n")))) "holds"  (Bool  "for" (Set (Var "A")) "being"   ($#v1_finset_1 :::"finite"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  (Bool  "for" (Set (Var "E")) "being"    ($#m2_rlaffin3 :::"Enumeration"::: )   "of" (Set (Var "A")) "holds"  (Bool (Set (Set  "("  ($#k3_matrtop1 :::"Mx2Tran"::: )  (Set (Var "M")) ")" )  ($#k4_finseqop :::"*"::: )  (Set (Var "E"))) "is"    ($#m2_rlaffin3 :::"Enumeration"::: )   "of" (Set (Set  "("  ($#k3_matrtop1 :::"Mx2Tran"::: )  (Set (Var "M")) ")" )  ($#k7_relset_1 :::".:"::: )  (Set (Var "A")))))))) ; 
 definitionlet "V" be   ($#l1_rlvect_1 :::"RealLinearSpace":::); let "Av" be   ($#v1_finset_1 :::"finite"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "V")); let "E" be    ($#m2_rlaffin3 :::"Enumeration"::: )   "of" (Set (Const "Av")); let "x" be    ($#m1_hidden :::"set"::: )  ; func "x" :::"|--"::: "E" ->    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  ) equals :: RLAFFIN3:def 2 (Set (Set  "(" "x"  ($#k5_rlaffin1 :::"|--"::: )  "Av" ")" )  ($#k4_finseqop :::"*"::: )  "E"); end; 








:: deftheorem    defines :::"|--"::: RLAFFIN3:def 2 :  (Bool  "for" (Set (Var "V")) "being"   ($#l1_rlvect_1 :::"RealLinearSpace":::)  (Bool  "for" (Set (Var "Av")) "being"   ($#v1_finset_1 :::"finite"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V"))  (Bool  "for" (Set (Var "E")) "being"    ($#m2_rlaffin3 :::"Enumeration"::: )   "of" (Set (Var "Av"))  (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set (Set (Var "x"))  ($#k1_rlaffin3 :::"|--"::: )  (Set (Var "E")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "x"))  ($#k5_rlaffin1 :::"|--"::: )  (Set (Var "Av")) ")" )  ($#k4_finseqop :::"*"::: )  (Set (Var "E")))))))); 
 
theorem :: RLAFFIN3:16 (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "V")) "being"   ($#l1_rlvect_1 :::"RealLinearSpace":::)  (Bool  "for" (Set (Var "Av")) "being"   ($#v1_finset_1 :::"finite"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V"))  (Bool  "for" (Set (Var "E")) "being"    ($#m2_rlaffin3 :::"Enumeration"::: )   "of" (Set (Var "Av")) "holds"  (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set  "(" (Set (Var "x"))  ($#k1_rlaffin3 :::"|--"::: )  (Set (Var "E")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k5_card_1 :::"card"::: )  (Set (Var "Av")))))))) ; 
 
theorem :: RLAFFIN3:17 (Bool  "for" (Set (Var "V")) "being"   ($#l1_rlvect_1 :::"RealLinearSpace":::)  (Bool  "for" (Set (Var "v")) "," (Set (Var "w")) "being"   ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V"))  (Bool  "for" (Set (Var "Affv")) "being"   ($#v1_finset_1 :::"finite"::: )     ($#v1_rlaffin1 :::"affinely-independent"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V"))  (Bool  "for" (Set (Var "EV")) "being"    ($#m2_rlaffin3 :::"Enumeration"::: )   "of" (Set (Var "Affv"))  (Bool  "for" (Set (Var "E")) "being"    ($#m2_rlaffin3 :::"Enumeration"::: )   "of" (Set (Set (Var "v"))  ($#k5_rusub_4 :::"+"::: )  (Set (Var "Affv")))  "st" (Bool (Bool (Set (Var "w"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_rlaffin1 :::"Affin"::: )  (Set (Var "Affv")))) & (Bool (Set (Var "E"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "EV"))  ($#k3_fvsum_1 :::"+"::: )  (Set  "(" (Set  "("  ($#k5_card_1 :::"card"::: )  (Set (Var "Affv")) ")" )  ($#k5_finseq_2 :::"|->"::: )  (Set (Var "v")) ")" )))) "holds"  (Bool (Set (Set (Var "w"))  ($#k1_rlaffin3 :::"|--"::: )  (Set (Var "EV")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "v"))  ($#k1_algstr_0 :::"+"::: )  (Set (Var "w")) ")" )  ($#k1_rlaffin3 :::"|--"::: )  (Set (Var "E"))))))))) ; 
 
theorem :: RLAFFIN3:18 (Bool  "for" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "V")) "being"   ($#l1_rlvect_1 :::"RealLinearSpace":::)  (Bool  "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V"))  (Bool  "for" (Set (Var "Affv")) "being"   ($#v1_finset_1 :::"finite"::: )     ($#v1_rlaffin1 :::"affinely-independent"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V"))  (Bool  "for" (Set (Var "EV")) "being"    ($#m2_rlaffin3 :::"Enumeration"::: )   "of" (Set (Var "Affv"))  (Bool  "for" (Set (Var "rE")) "being"    ($#m2_rlaffin3 :::"Enumeration"::: )   "of" (Set (Set (Var "r"))  ($#k1_convex1 :::"*"::: )  (Set (Var "Affv")))  "st" (Bool (Bool (Set (Var "v"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_rlaffin1 :::"Affin"::: )  (Set (Var "Affv")))) & (Bool (Set (Var "rE"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "r"))  ($#k4_vfunct_1 :::"(#)"::: )  (Set (Var "EV")))) & (Bool (Set (Var "r"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"0"::: )  ))) "holds"  (Bool (Set (Set (Var "v"))  ($#k1_rlaffin3 :::"|--"::: )  (Set (Var "EV")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "r"))  ($#k1_rlvect_1 :::"*"::: )  (Set (Var "v")) ")" )  ($#k1_rlaffin3 :::"|--"::: )  (Set (Var "rE")))))))))) ; 
 
theorem :: RLAFFIN3:19 (Bool  "for" (Set (Var "n")) "," (Set (Var "m")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "Affn")) "being"   ($#v1_rlaffin1 :::"affinely-independent"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  (Bool  "for" (Set (Var "EN")) "being"    ($#m2_rlaffin3 :::"Enumeration"::: )   "of" (Set (Var "Affn"))  (Bool  "for" (Set (Var "M")) "being"   ($#m1_matrix_1 :::"Matrix":::) "of" (Set (Var "n")) "," (Set (Var "m")) "," (Set  ($#k2_vectsp_1 :::"F_Real"::: ) )  "st" (Bool (Bool (Set   ($#k8_matrix13 :::"the_rank_of"::: )  (Set (Var "M")))  ($#r1_hidden :::"="::: )  (Set (Var "n")))) "holds"  (Bool  "for" (Set (Var "ME")) "being"    ($#m2_rlaffin3 :::"Enumeration"::: )   "of" (Set (Set  "("  ($#k3_matrtop1 :::"Mx2Tran"::: )  (Set (Var "M")) ")" )  ($#k7_relset_1 :::".:"::: )  (Set (Var "Affn")))  "st" (Bool (Bool (Set (Var "ME"))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k3_matrtop1 :::"Mx2Tran"::: )  (Set (Var "M")) ")" )  ($#k4_finseqop :::"*"::: )  (Set (Var "EN"))))) "holds"  (Bool  "for" (Set (Var "pn")) "being"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  "st" (Bool (Bool (Set (Var "pn"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_rlaffin1 :::"Affin"::: )  (Set (Var "Affn"))))) "holds"  (Bool (Set (Set (Var "pn"))  ($#k1_rlaffin3 :::"|--"::: )  (Set (Var "EN")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k3_matrtop1 :::"Mx2Tran"::: )  (Set (Var "M")) ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "pn")) ")" )  ($#k1_rlaffin3 :::"|--"::: )  (Set (Var "ME")))))))))) ; 
 
theorem :: RLAFFIN3:20 (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "V")) "being"   ($#l1_rlvect_1 :::"RealLinearSpace":::)  (Bool  "for" (Set (Var "Affv")) "being"   ($#v1_finset_1 :::"finite"::: )     ($#v1_rlaffin1 :::"affinely-independent"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V"))  (Bool  "for" (Set (Var "EV")) "being"    ($#m2_rlaffin3 :::"Enumeration"::: )   "of" (Set (Var "Affv"))  (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V"))  "st" (Bool (Bool (Set (Var "A"))  ($#r1_tarski :::"c="::: )  (Set (Var "Affv"))) & (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_rlaffin1 :::"Affin"::: )  (Set (Var "Affv"))))) "holds"  (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_rlaffin1 :::"Affin"::: )  (Set (Var "A")))) "iff" (Bool  "for" (Set (Var "y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set  "(" (Set (Var "x"))  ($#k1_rlaffin3 :::"|--"::: )  (Set (Var "EV")) ")" ))) & (Bool (Bool  "not" (Set (Set (Var "EV"))  ($#k1_funct_1 :::"."::: )  (Set (Var "y")))  ($#r2_hidden :::"in"::: )  (Set (Var "A"))))) "holds"  (Bool (Set (Set  "(" (Set (Var "x"))  ($#k1_rlaffin3 :::"|--"::: )  (Set (Var "EV")) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "y")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"0"::: )  )))  ")" )))))) ; 
 
theorem :: RLAFFIN3:21 (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "V")) "being"   ($#l1_rlvect_1 :::"RealLinearSpace":::)  (Bool  "for" (Set (Var "Affv")) "being"   ($#v1_finset_1 :::"finite"::: )     ($#v1_rlaffin1 :::"affinely-independent"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V"))  (Bool  "for" (Set (Var "EV")) "being"    ($#m2_rlaffin3 :::"Enumeration"::: )   "of" (Set (Var "Affv"))  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_rlaffin1 :::"Affin"::: )  (Set (Var "Affv"))))) "holds"  (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_rlaffin1 :::"Affin"::: )  (Set  "(" (Set (Var "EV"))  ($#k7_relset_1 :::".:"::: )  (Set  "("  ($#k2_finseq_1 :::"Seg"::: )  (Set (Var "k")) ")" ) ")" ))) "iff" (Bool (Set (Set (Var "x"))  ($#k1_rlaffin3 :::"|--"::: )  (Set (Var "EV")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set (Var "x"))  ($#k1_rlaffin3 :::"|--"::: )  (Set (Var "EV")) ")" )  ($#k17_finseq_1 :::"|"::: )  (Set (Var "k")) ")" )  ($#k7_finseq_1 :::"^"::: )  (Set  "(" (Set  "(" (Set  "("  ($#k5_card_1 :::"card"::: )  (Set (Var "Affv")) ")" )  ($#k7_nat_d :::"-'"::: )  (Set (Var "k")) ")" )  ($#k2_finseq_2 :::"|->"::: )  (Set  ($#k1_xboole_0 :::"0"::: ) ) ")" )))  ")" )))))) ; 
 
theorem :: RLAFFIN3:22 (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "V")) "being"   ($#l1_rlvect_1 :::"RealLinearSpace":::)  (Bool  "for" (Set (Var "Affv")) "being"   ($#v1_finset_1 :::"finite"::: )     ($#v1_rlaffin1 :::"affinely-independent"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V"))  (Bool  "for" (Set (Var "EV")) "being"    ($#m2_rlaffin3 :::"Enumeration"::: )   "of" (Set (Var "Affv"))  "st" (Bool (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k5_card_1 :::"card"::: )  (Set (Var "Affv")))) & (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_rlaffin1 :::"Affin"::: )  (Set (Var "Affv"))))) "holds"  (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_rlaffin1 :::"Affin"::: )  (Set  "(" (Set (Var "Affv"))  ($#k7_subset_1 :::"\"::: )  (Set  "(" (Set (Var "EV"))  ($#k7_relset_1 :::".:"::: )  (Set  "("  ($#k2_finseq_1 :::"Seg"::: )  (Set (Var "k")) ")" ) ")" ) ")" ))) "iff" (Bool (Set (Set (Var "x"))  ($#k1_rlaffin3 :::"|--"::: )  (Set (Var "EV")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "k"))  ($#k2_finseq_2 :::"|->"::: )  (Set  ($#k1_xboole_0 :::"0"::: ) ) ")" )  ($#k7_finseq_1 :::"^"::: )  (Set  "(" (Set  "(" (Set (Var "x"))  ($#k1_rlaffin3 :::"|--"::: )  (Set (Var "EV")) ")" )  ($#k2_rfinseq :::"/^"::: )  (Set (Var "k")) ")" )))  ")" )))))) ; 
 
theorem :: RLAFFIN3:23 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "Affn")) "being"   ($#v1_rlaffin1 :::"affinely-independent"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  (Bool  "for" (Set (Var "EN")) "being"    ($#m2_rlaffin3 :::"Enumeration"::: )   "of" (Set (Var "Affn"))  "st" (Bool (Bool (Set   ($#k5_euclid :::"0*"::: )  (Set (Var "n")))  ($#r2_hidden :::"in"::: )  (Set (Var "Affn"))) & (Bool (Set (Set (Var "EN"))  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "EN")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k5_euclid :::"0*"::: )  (Set (Var "n"))))) "holds"  (Bool  "("  (Bool (Set   ($#k2_relset_1 :::"rng"::: )  (Set  "(" (Set (Var "EN"))  ($#k17_finseq_1 :::"|"::: )  (Set  "(" (Set  "("  ($#k5_card_1 :::"card"::: )  (Set (Var "Affn")) ")" )  ($#k7_nat_d :::"-'"::: )  (Num 1) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "Affn"))  ($#k7_subset_1 :::"\"::: )  (Set  ($#k6_domain_1 :::"{"::: ) (Set  "("  ($#k5_euclid :::"0*"::: )  (Set (Var "n")) ")" ) ($#k6_domain_1 :::"}"::: ) ))) & (Bool  "("   "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "(" (Set (Var "n"))  ($#k6_prvect_1 :::"-VectSp_over"::: )  (Set  ($#k2_vectsp_1 :::"F_Real"::: ) ) ")" )  "st" (Bool (Bool (Set (Var "Affn"))  ($#r1_hidden :::"="::: )  (Set (Var "A")))) "holds"  (Bool (Set (Set (Var "EN"))  ($#k17_finseq_1 :::"|"::: )  (Set  "(" (Set  "("  ($#k5_card_1 :::"card"::: )  (Set (Var "Affn")) ")" )  ($#k7_nat_d :::"-'"::: )  (Num 1) ")" )) "is"    ($#m1_matrlin :::"OrdBasis"::: )   "of" (Set   ($#k1_vectsp_7 :::"Lin"::: )  (Set (Var "A"))))  ")" )  ")" )))) ; 
 
theorem :: RLAFFIN3:24 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "Affn")) "being"   ($#v1_rlaffin1 :::"affinely-independent"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  (Bool  "for" (Set (Var "EN")) "being"    ($#m2_rlaffin3 :::"Enumeration"::: )   "of" (Set (Var "Affn"))  (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "(" (Set (Var "n"))  ($#k6_prvect_1 :::"-VectSp_over"::: )  (Set  ($#k2_vectsp_1 :::"F_Real"::: ) ) ")" )  "st" (Bool (Bool (Set (Var "Affn"))  ($#r1_hidden :::"="::: )  (Set (Var "A"))) & (Bool (Set   ($#k5_euclid :::"0*"::: )  (Set (Var "n")))  ($#r2_hidden :::"in"::: )  (Set (Var "Affn"))) & (Bool (Set (Set (Var "EN"))  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "EN")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k5_euclid :::"0*"::: )  (Set (Var "n"))))) "holds"  (Bool  "for" (Set (Var "B")) "being"    ($#m1_matrlin :::"OrdBasis"::: )   "of" (Set   ($#k1_vectsp_7 :::"Lin"::: )  (Set (Var "A")))  "st" (Bool (Bool (Set (Var "B"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "EN"))  ($#k17_finseq_1 :::"|"::: )  (Set  "(" (Set  "("  ($#k5_card_1 :::"card"::: )  (Set (Var "Affn")) ")" )  ($#k7_nat_d :::"-'"::: )  (Num 1) ")" )))) "holds"  (Bool  "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  "("  ($#k1_vectsp_7 :::"Lin"::: )  (Set (Var "A")) ")" ) "holds"  (Bool (Set (Set (Var "v"))  ($#k9_matrlin :::"|--"::: )  (Set (Var "B")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "v"))  ($#k1_rlaffin3 :::"|--"::: )  (Set (Var "EN")) ")" )  ($#k17_finseq_1 :::"|"::: )  (Set  "(" (Set  "("  ($#k5_card_1 :::"card"::: )  (Set (Var "Affn")) ")" )  ($#k7_nat_d :::"-'"::: )  (Num 1) ")" ))))))))) ; 
 
theorem :: RLAFFIN3:25 (Bool  "for" (Set (Var "n")) "," (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "Affn")) "being"   ($#v1_rlaffin1 :::"affinely-independent"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  (Bool  "for" (Set (Var "Ak")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "k")) ")" )  (Bool  "for" (Set (Var "EN")) "being"    ($#m2_rlaffin3 :::"Enumeration"::: )   "of" (Set (Var "Affn"))  (Bool  "for" (Set (Var "An")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  "st" (Bool (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n"))) & (Bool (Set   ($#k5_card_1 :::"card"::: )  (Set (Var "Affn")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "n"))  ($#k23_binop_2 :::"+"::: )  (Num 1))) & (Bool (Set (Var "An"))  ($#r1_hidden :::"="::: )   "{"  (Set (Var "pn")) where pn "is"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" ) : (Bool (Set (Set  "(" (Set (Var "pn"))  ($#k1_rlaffin3 :::"|--"::: )  (Set (Var "EN")) ")" )  ($#k17_finseq_1 :::"|"::: )  (Set (Var "k")))  ($#r2_hidden :::"in"::: )  (Set (Var "Ak")))  "}"  )) "holds"  (Bool  "("  (Bool (Set (Var "Ak")) "is"   ($#v3_pre_topc :::"open"::: )  ) "iff" (Bool (Set (Var "An")) "is"   ($#v3_pre_topc :::"open"::: )  )  ")" )))))) ; 
 
theorem :: RLAFFIN3:26 (Bool  "for" (Set (Var "n")) "," (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "An")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  (Bool  "for" (Set (Var "Affn")) "being"   ($#v1_rlaffin1 :::"affinely-independent"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  (Bool  "for" (Set (Var "Ak")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "k")) ")" )  (Bool  "for" (Set (Var "EN")) "being"    ($#m2_rlaffin3 :::"Enumeration"::: )   "of" (Set (Var "Affn"))  "st" (Bool (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n"))) & (Bool (Set   ($#k5_card_1 :::"card"::: )  (Set (Var "Affn")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "n"))  ($#k23_binop_2 :::"+"::: )  (Num 1))) & (Bool (Set (Var "An"))  ($#r1_hidden :::"="::: )   "{"  (Set (Var "pn")) where pn "is"   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" ) : (Bool (Set (Set  "(" (Set (Var "pn"))  ($#k1_rlaffin3 :::"|--"::: )  (Set (Var "EN")) ")" )  ($#k17_finseq_1 :::"|"::: )  (Set (Var "k")))  ($#r2_hidden :::"in"::: )  (Set (Var "Ak")))  "}"  )) "holds"  (Bool  "("  (Bool (Set (Var "Ak")) "is"   ($#v4_pre_topc :::"closed"::: )  ) "iff" (Bool (Set (Var "An")) "is"   ($#v4_pre_topc :::"closed"::: )  )  ")" )))))) ; 
 registrationlet "n" be   ($#m1_hidden :::"Nat":::); 
cluster   ($#v2_rusub_4 :::"Affine"::: )    ->   ($#v4_pre_topc :::"closed"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_zfmisc_1 :::"bool"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  "n" ")" ))); 
end; 



theorem :: RLAFFIN3:27 (Bool  "for" (Set (Var "n")) "," (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "Affn")) "being"   ($#v1_rlaffin1 :::"affinely-independent"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  (Bool  "for" (Set (Var "Ak")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "k")) ")" )  (Bool  "for" (Set (Var "EN")) "being"    ($#m2_rlaffin3 :::"Enumeration"::: )   "of" (Set (Var "Affn"))  (Bool  "for" (Set (Var "B")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "(" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  ($#k1_pre_topc :::"|"::: )  (Set  "("  ($#k4_rlaffin1 :::"Affin"::: )  (Set (Var "Affn")) ")" ) ")" )  "st" (Bool (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k5_card_1 :::"card"::: )  (Set (Var "Affn")))) & (Bool (Set (Var "B"))  ($#r1_hidden :::"="::: )   "{"  (Set (Var "pnA")) where pnA "is"   ($#m1_subset_1 :::"Element":::) "of" (Set  "(" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  ($#k1_pre_topc :::"|"::: )  (Set  "("  ($#k4_rlaffin1 :::"Affin"::: )  (Set (Var "Affn")) ")" ) ")" ) : (Bool (Set (Set  "(" (Set (Var "pnA"))  ($#k1_rlaffin3 :::"|--"::: )  (Set (Var "EN")) ")" )  ($#k17_finseq_1 :::"|"::: )  (Set (Var "k")))  ($#r2_hidden :::"in"::: )  (Set (Var "Ak")))  "}"  )) "holds"  (Bool  "("  (Bool (Set (Var "Ak")) "is"   ($#v3_pre_topc :::"open"::: )  ) "iff" (Bool (Set (Var "B")) "is"   ($#v3_pre_topc :::"open"::: )  )  ")" )))))) ; 
 
theorem :: RLAFFIN3:28 (Bool  "for" (Set (Var "n")) "," (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "Affn")) "being"   ($#v1_rlaffin1 :::"affinely-independent"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  (Bool  "for" (Set (Var "Ak")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "k")) ")" )  (Bool  "for" (Set (Var "EN")) "being"    ($#m2_rlaffin3 :::"Enumeration"::: )   "of" (Set (Var "Affn"))  (Bool  "for" (Set (Var "B")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  "(" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  ($#k1_pre_topc :::"|"::: )  (Set  "("  ($#k4_rlaffin1 :::"Affin"::: )  (Set (Var "Affn")) ")" ) ")" )  "st" (Bool (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k5_card_1 :::"card"::: )  (Set (Var "Affn")))) & (Bool (Set (Var "B"))  ($#r1_hidden :::"="::: )   "{"  (Set (Var "pnA")) where pnA "is"   ($#m1_subset_1 :::"Element":::) "of" (Set  "(" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  ($#k1_pre_topc :::"|"::: )  (Set  "("  ($#k4_rlaffin1 :::"Affin"::: )  (Set (Var "Affn")) ")" ) ")" ) : (Bool (Set (Set  "(" (Set (Var "pnA"))  ($#k1_rlaffin3 :::"|--"::: )  (Set (Var "EN")) ")" )  ($#k17_finseq_1 :::"|"::: )  (Set (Var "k")))  ($#r2_hidden :::"in"::: )  (Set (Var "Ak")))  "}"  )) "holds"  (Bool  "("  (Bool (Set (Var "Ak")) "is"   ($#v4_pre_topc :::"closed"::: )  ) "iff" (Bool (Set (Var "B")) "is"   ($#v4_pre_topc :::"closed"::: )  )  ")" )))))) ; 
 registrationlet "n" be   ($#m1_hidden :::"Nat":::); let "p", "q" be   ($#m1_subset_1 :::"Point":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Const "n")) ")" ); 
cluster (Set   ($#k4_topreal9 :::"halfline"::: )   "(" "p" "," "q" ")" ) ->   ($#v4_pre_topc :::"closed"::: )   ; 
end; begin  definitionlet "V" be   ($#l1_rlvect_1 :::"RealLinearSpace":::); let "A" be   ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "V")); let "x" be    ($#m1_hidden :::"set"::: )  ; func  :::"|--":::  "(" "A" "," "x" ")"  ->   ($#m1_subset_1 :::"Function":::) "of" "V" "," (Set  ($#k3_topmetr :::"R^1"::: ) ) means :: RLAFFIN3:def 3 (Bool  "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"VECTOR":::) "of" "V" "holds"  (Bool (Set it  ($#k3_funct_2 :::"."::: )  (Set (Var "v")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "v"))  ($#k5_rlaffin1 :::"|--"::: )  "A" ")" )  ($#k1_funct_1 :::"."::: )  "x"))); end; 







:: deftheorem    defines :::"|--"::: RLAFFIN3:def 3 :  (Bool  "for" (Set (Var "V")) "being"   ($#l1_rlvect_1 :::"RealLinearSpace":::)  (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V"))  (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "b4")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "V")) "," (Set  ($#k3_topmetr :::"R^1"::: ) ) "holds"   (Bool  "("  (Bool (Set (Var "b4"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_rlaffin3 :::"|--"::: )   "(" (Set (Var "A")) "," (Set (Var "x")) ")" )) "iff" (Bool  "for" (Set (Var "v")) "being"   ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "holds"  (Bool (Set (Set (Var "b4"))  ($#k3_funct_2 :::"."::: )  (Set (Var "v")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "v"))  ($#k5_rlaffin1 :::"|--"::: )  (Set (Var "A")) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "x")))))  ")" ))))); 
 
theorem :: RLAFFIN3:29 (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "V")) "being"   ($#l1_rlvect_1 :::"RealLinearSpace":::)  (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V"))  "st" (Bool (Bool (Bool  "not" (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "A"))))) "holds"  (Bool (Set   ($#k2_rlaffin3 :::"|--"::: )   "(" (Set (Var "A")) "," (Set (Var "x")) ")" )  ($#r1_funct_2 :::"="::: )  (Set (Set  "("  ($#k2_struct_0 :::"[#]"::: )  (Set (Var "V")) ")" )  ($#k7_funcop_1 :::"-->"::: )  (Set  ($#k1_xboole_0 :::"0"::: ) )))))) ; 
 
theorem :: RLAFFIN3:30 (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "V")) "being"   ($#l1_rlvect_1 :::"RealLinearSpace":::)  (Bool  "for" (Set (Var "A")) "being"   ($#v1_rlaffin1 :::"affinely-independent"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "V"))  "st" (Bool (Bool (Set   ($#k2_rlaffin3 :::"|--"::: )   "(" (Set (Var "A")) "," (Set (Var "x")) ")" )  ($#r1_funct_2 :::"="::: )  (Set (Set  "("  ($#k2_struct_0 :::"[#]"::: )  (Set (Var "V")) ")" )  ($#k7_funcop_1 :::"-->"::: )  (Set  ($#k1_xboole_0 :::"0"::: ) )))) "holds"  (Bool  "not" (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "A"))))))) ; 
 
theorem :: RLAFFIN3:31 (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "Affn")) "being"   ($#v1_rlaffin1 :::"affinely-independent"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" ) "holds"  (Bool (Set (Set  "("  ($#k2_rlaffin3 :::"|--"::: )   "(" (Set (Var "Affn")) "," (Set (Var "x")) ")"  ")" )  ($#k2_partfun1 :::"|"::: )  (Set  "("  ($#k4_rlaffin1 :::"Affin"::: )  (Set (Var "Affn")) ")" )) "is"   ($#v5_pre_topc :::"continuous"::: )    ($#m1_subset_1 :::"Function":::) "of" (Set  "(" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  ($#k1_pre_topc :::"|"::: )  (Set  "("  ($#k4_rlaffin1 :::"Affin"::: )  (Set (Var "Affn")) ")" ) ")" ) "," (Set  ($#k3_topmetr :::"R^1"::: ) ))))) ; 
 
theorem :: RLAFFIN3:32 (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "Affn")) "being"   ($#v1_rlaffin1 :::"affinely-independent"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  "st" (Bool (Bool (Set   ($#k5_card_1 :::"card"::: )  (Set (Var "Affn")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "n"))  ($#k23_binop_2 :::"+"::: )  (Num 1)))) "holds"  (Bool (Set   ($#k2_rlaffin3 :::"|--"::: )   "(" (Set (Var "Affn")) "," (Set (Var "x")) ")" ) "is"   ($#v5_pre_topc :::"continuous"::: )  )))) ; 
 registrationlet "n" be   ($#m1_hidden :::"Nat":::); let "Affn" be   ($#v1_rlaffin1 :::"affinely-independent"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Const "n")) ")" ); 
cluster (Set   ($#k3_convex1 :::"conv"::: )  "Affn") ->   ($#v4_pre_topc :::"closed"::: )   ; 
end; 
theorem :: RLAFFIN3:33 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "Affn")) "being"   ($#v1_rlaffin1 :::"affinely-independent"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_euclid :::"TOP-REAL"::: )  (Set (Var "n")) ")" )  "st" (Bool (Bool (Set   ($#k5_card_1 :::"card"::: )  (Set (Var "Affn")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "n"))  ($#k23_binop_2 :::"+"::: )  (Num 1)))) "holds"  (Bool (Set   ($#k1_rlaffin2 :::"Int"::: )  (Set (Var "Affn"))) "is"   ($#v3_pre_topc :::"open"::: )  ))) ;