:: HAHNBAN semantic presentation begin theorem :: HAHNBAN:1 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_rlsub_1 :::"Subspace"::: ) "of" (Set (Var "V")) "holds" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "W1"))) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" (Set (Var "W1")) ($#k1_rlsub_2 :::"+"::: ) (Set (Var "W2")) ")" ))))) ; theorem :: HAHNBAN:2 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_rlsub_1 :::"Subspace"::: ) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "V")) ($#r1_rlsub_2 :::"is_the_direct_sum_of"::: ) (Set (Var "W1")) "," (Set (Var "W2")))) "holds" (Bool "for" (Set (Var "v")) "," (Set (Var "v1")) "," (Set (Var "v2")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "v1")) ($#r1_struct_0 :::"in"::: ) (Set (Var "W1"))) & (Bool (Set (Var "v2")) ($#r1_struct_0 :::"in"::: ) (Set (Var "W2"))) & (Bool (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set (Set (Var "v1")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "v2"))))) "holds" (Bool (Set (Set (Var "v")) ($#k4_rlsub_2 :::"|--"::: ) "(" (Set (Var "W1")) "," (Set (Var "W2")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "v1")) "," (Set (Var "v2")) ($#k1_domain_1 :::"]"::: ) ))))) ; theorem :: HAHNBAN:3 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_rlsub_1 :::"Subspace"::: ) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "V")) ($#r1_rlsub_2 :::"is_the_direct_sum_of"::: ) (Set (Var "W1")) "," (Set (Var "W2")))) "holds" (Bool "for" (Set (Var "v")) "," (Set (Var "v1")) "," (Set (Var "v2")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Set (Var "v")) ($#k4_rlsub_2 :::"|--"::: ) "(" (Set (Var "W1")) "," (Set (Var "W2")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "v1")) "," (Set (Var "v2")) ($#k1_domain_1 :::"]"::: ) ))) "holds" (Bool (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set (Set (Var "v1")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "v2"))))))) ; theorem :: HAHNBAN:4 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_rlsub_1 :::"Subspace"::: ) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "V")) ($#r1_rlsub_2 :::"is_the_direct_sum_of"::: ) (Set (Var "W1")) "," (Set (Var "W2")))) "holds" (Bool "for" (Set (Var "v")) "," (Set (Var "v1")) "," (Set (Var "v2")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Set (Var "v")) ($#k4_rlsub_2 :::"|--"::: ) "(" (Set (Var "W1")) "," (Set (Var "W2")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "v1")) "," (Set (Var "v2")) ($#k1_domain_1 :::"]"::: ) ))) "holds" (Bool "(" (Bool (Set (Var "v1")) ($#r1_struct_0 :::"in"::: ) (Set (Var "W1"))) & (Bool (Set (Var "v2")) ($#r1_struct_0 :::"in"::: ) (Set (Var "W2"))) ")" )))) ; theorem :: HAHNBAN:5 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_rlsub_1 :::"Subspace"::: ) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "V")) ($#r1_rlsub_2 :::"is_the_direct_sum_of"::: ) (Set (Var "W1")) "," (Set (Var "W2")))) "holds" (Bool "for" (Set (Var "v")) "," (Set (Var "v1")) "," (Set (Var "v2")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Set (Var "v")) ($#k4_rlsub_2 :::"|--"::: ) "(" (Set (Var "W1")) "," (Set (Var "W2")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "v1")) "," (Set (Var "v2")) ($#k1_domain_1 :::"]"::: ) ))) "holds" (Bool (Set (Set (Var "v")) ($#k4_rlsub_2 :::"|--"::: ) "(" (Set (Var "W2")) "," (Set (Var "W1")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "v2")) "," (Set (Var "v1")) ($#k1_domain_1 :::"]"::: ) ))))) ; theorem :: HAHNBAN:6 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_rlsub_1 :::"Subspace"::: ) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "V")) ($#r1_rlsub_2 :::"is_the_direct_sum_of"::: ) (Set (Var "W1")) "," (Set (Var "W2")))) "holds" (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "v")) ($#r1_struct_0 :::"in"::: ) (Set (Var "W1")))) "holds" (Bool (Set (Set (Var "v")) ($#k4_rlsub_2 :::"|--"::: ) "(" (Set (Var "W1")) "," (Set (Var "W2")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "v")) "," (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "V")) ")" ) ($#k1_domain_1 :::"]"::: ) ))))) ; theorem :: HAHNBAN:7 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_rlsub_1 :::"Subspace"::: ) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "V")) ($#r1_rlsub_2 :::"is_the_direct_sum_of"::: ) (Set (Var "W1")) "," (Set (Var "W2")))) "holds" (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "v")) ($#r1_struct_0 :::"in"::: ) (Set (Var "W2")))) "holds" (Bool (Set (Set (Var "v")) ($#k4_rlsub_2 :::"|--"::: ) "(" (Set (Var "W1")) "," (Set (Var "W2")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "V")) ")" ) "," (Set (Var "v")) ($#k1_domain_1 :::"]"::: ) ))))) ; theorem :: HAHNBAN:8 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "V1")) "being" ($#m1_rlsub_1 :::"Subspace"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "W1")) "being" ($#m1_rlsub_1 :::"Subspace"::: ) "of" (Set (Var "V1")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "v")) ($#r1_struct_0 :::"in"::: ) (Set (Var "W1")))) "holds" (Bool (Set (Var "v")) "is" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V1"))))))) ; theorem :: HAHNBAN:9 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "V1")) "," (Set (Var "V2")) "," (Set (Var "W")) "being" ($#m1_rlsub_1 :::"Subspace"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_rlsub_1 :::"Subspace"::: ) "of" (Set (Var "W")) "st" (Bool (Bool (Set (Var "W1")) ($#r1_hidden :::"="::: ) (Set (Var "V1"))) & (Bool (Set (Var "W2")) ($#r1_hidden :::"="::: ) (Set (Var "V2")))) "holds" (Bool (Set (Set (Var "W1")) ($#k1_rlsub_2 :::"+"::: ) (Set (Var "W2"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "V1")) ($#k1_rlsub_2 :::"+"::: ) (Set (Var "V2"))))))) ; theorem :: HAHNBAN:10 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "W")) "being" ($#m1_rlsub_1 :::"Subspace"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "W")) "st" (Bool (Bool (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set (Var "w")))) "holds" (Bool (Set ($#k1_rlvect_3 :::"Lin"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "w")) ($#k6_domain_1 :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_rlvect_3 :::"Lin"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "v")) ($#k6_domain_1 :::"}"::: ) ))))))) ; theorem :: HAHNBAN:11 (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 "X")) "being" ($#m1_rlsub_1 :::"Subspace"::: ) "of" (Set (Var "V")) "st" (Bool (Bool (Bool "not" (Set (Var "v")) ($#r1_struct_0 :::"in"::: ) (Set (Var "X"))))) "holds" (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set "(" (Set (Var "X")) ($#k1_rlsub_2 :::"+"::: ) (Set "(" ($#k1_rlvect_3 :::"Lin"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "v")) ($#k6_domain_1 :::"}"::: ) ) ")" ) ")" ) (Bool "for" (Set (Var "W")) "being" ($#m1_rlsub_1 :::"Subspace"::: ) "of" (Set (Set (Var "X")) ($#k1_rlsub_2 :::"+"::: ) (Set "(" ($#k1_rlvect_3 :::"Lin"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "v")) ($#k6_domain_1 :::"}"::: ) ) ")" )) "st" (Bool (Bool (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set (Var "y"))) & (Bool (Set (Var "W")) ($#r1_hidden :::"="::: ) (Set (Var "X")))) "holds" (Bool (Set (Set (Var "X")) ($#k1_rlsub_2 :::"+"::: ) (Set "(" ($#k1_rlvect_3 :::"Lin"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "v")) ($#k6_domain_1 :::"}"::: ) ) ")" )) ($#r1_rlsub_2 :::"is_the_direct_sum_of"::: ) (Set (Var "W")) "," (Set ($#k1_rlvect_3 :::"Lin"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "y")) ($#k6_domain_1 :::"}"::: ) )))))))) ; theorem :: HAHNBAN:12 (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 "X")) "being" ($#m1_rlsub_1 :::"Subspace"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set "(" (Set (Var "X")) ($#k1_rlsub_2 :::"+"::: ) (Set "(" ($#k1_rlvect_3 :::"Lin"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "v")) ($#k6_domain_1 :::"}"::: ) ) ")" ) ")" ) (Bool "for" (Set (Var "W")) "being" ($#m1_rlsub_1 :::"Subspace"::: ) "of" (Set (Set (Var "X")) ($#k1_rlsub_2 :::"+"::: ) (Set "(" ($#k1_rlvect_3 :::"Lin"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "v")) ($#k6_domain_1 :::"}"::: ) ) ")" )) "st" (Bool (Bool (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set (Var "y"))) & (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set (Var "W"))) & (Bool (Bool "not" (Set (Var "v")) ($#r1_struct_0 :::"in"::: ) (Set (Var "X"))))) "holds" (Bool (Set (Set (Var "y")) ($#k4_rlsub_2 :::"|--"::: ) "(" (Set (Var "W")) "," (Set "(" ($#k1_rlvect_3 :::"Lin"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "y")) ($#k6_domain_1 :::"}"::: ) ) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "W")) ")" ) "," (Set (Var "y")) ($#k1_domain_1 :::"]"::: ) ))))))) ; theorem :: HAHNBAN:13 (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 "X")) "being" ($#m1_rlsub_1 :::"Subspace"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set "(" (Set (Var "X")) ($#k1_rlsub_2 :::"+"::: ) (Set "(" ($#k1_rlvect_3 :::"Lin"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "v")) ($#k6_domain_1 :::"}"::: ) ) ")" ) ")" ) (Bool "for" (Set (Var "W")) "being" ($#m1_rlsub_1 :::"Subspace"::: ) "of" (Set (Set (Var "X")) ($#k1_rlsub_2 :::"+"::: ) (Set "(" ($#k1_rlvect_3 :::"Lin"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "v")) ($#k6_domain_1 :::"}"::: ) ) ")" )) "st" (Bool (Bool (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set (Var "y"))) & (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set (Var "W"))) & (Bool (Bool "not" (Set (Var "v")) ($#r1_struct_0 :::"in"::: ) (Set (Var "X"))))) "holds" (Bool "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set "(" (Set (Var "X")) ($#k1_rlsub_2 :::"+"::: ) (Set "(" ($#k1_rlvect_3 :::"Lin"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "v")) ($#k6_domain_1 :::"}"::: ) ) ")" ) ")" ) "st" (Bool (Bool (Set (Var "w")) ($#r1_struct_0 :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Set (Var "w")) ($#k4_rlsub_2 :::"|--"::: ) "(" (Set (Var "W")) "," (Set "(" ($#k1_rlvect_3 :::"Lin"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "y")) ($#k6_domain_1 :::"}"::: ) ) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "w")) "," (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "V")) ")" ) ($#k1_domain_1 :::"]"::: ) )))))))) ; theorem :: HAHNBAN:14 (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 "W1")) "," (Set (Var "W2")) "being" ($#m1_rlsub_1 :::"Subspace"::: ) "of" (Set (Var "V")) (Bool "ex" (Set (Var "v1")) "," (Set (Var "v2")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Set (Set (Var "v")) ($#k4_rlsub_2 :::"|--"::: ) "(" (Set (Var "W1")) "," (Set (Var "W2")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "v1")) "," (Set (Var "v2")) ($#k1_domain_1 :::"]"::: ) )))))) ; theorem :: HAHNBAN:15 (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 "X")) "being" ($#m1_rlsub_1 :::"Subspace"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set "(" (Set (Var "X")) ($#k1_rlsub_2 :::"+"::: ) (Set "(" ($#k1_rlvect_3 :::"Lin"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "v")) ($#k6_domain_1 :::"}"::: ) ) ")" ) ")" ) (Bool "for" (Set (Var "W")) "being" ($#m1_rlsub_1 :::"Subspace"::: ) "of" (Set (Set (Var "X")) ($#k1_rlsub_2 :::"+"::: ) (Set "(" ($#k1_rlvect_3 :::"Lin"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "v")) ($#k6_domain_1 :::"}"::: ) ) ")" )) "st" (Bool (Bool (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set (Var "y"))) & (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set (Var "W"))) & (Bool (Bool "not" (Set (Var "v")) ($#r1_struct_0 :::"in"::: ) (Set (Var "X"))))) "holds" (Bool "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set "(" (Set (Var "X")) ($#k1_rlsub_2 :::"+"::: ) (Set "(" ($#k1_rlvect_3 :::"Lin"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "v")) ($#k6_domain_1 :::"}"::: ) ) ")" ) ")" ) (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "X"))(Bool "ex" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Set (Set (Var "w")) ($#k4_rlsub_2 :::"|--"::: ) "(" (Set (Var "W")) "," (Set "(" ($#k1_rlvect_3 :::"Lin"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "y")) ($#k6_domain_1 :::"}"::: ) ) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "x")) "," (Set "(" (Set (Var "r")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "v")) ")" ) ($#k1_domain_1 :::"]"::: ) )))))))))) ; theorem :: HAHNBAN:16 (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 "X")) "being" ($#m1_rlsub_1 :::"Subspace"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set "(" (Set (Var "X")) ($#k1_rlsub_2 :::"+"::: ) (Set "(" ($#k1_rlvect_3 :::"Lin"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "v")) ($#k6_domain_1 :::"}"::: ) ) ")" ) ")" ) (Bool "for" (Set (Var "W")) "being" ($#m1_rlsub_1 :::"Subspace"::: ) "of" (Set (Set (Var "X")) ($#k1_rlsub_2 :::"+"::: ) (Set "(" ($#k1_rlvect_3 :::"Lin"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "v")) ($#k6_domain_1 :::"}"::: ) ) ")" )) "st" (Bool (Bool (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set (Var "y"))) & (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set (Var "W"))) & (Bool (Bool "not" (Set (Var "v")) ($#r1_struct_0 :::"in"::: ) (Set (Var "X"))))) "holds" (Bool "for" (Set (Var "w1")) "," (Set (Var "w2")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set "(" (Set (Var "X")) ($#k1_rlsub_2 :::"+"::: ) (Set "(" ($#k1_rlvect_3 :::"Lin"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "v")) ($#k6_domain_1 :::"}"::: ) ) ")" ) ")" ) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "r1")) "," (Set (Var "r2")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Set (Var "w1")) ($#k4_rlsub_2 :::"|--"::: ) "(" (Set (Var "W")) "," (Set "(" ($#k1_rlvect_3 :::"Lin"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "y")) ($#k6_domain_1 :::"}"::: ) ) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "x1")) "," (Set "(" (Set (Var "r1")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "v")) ")" ) ($#k1_domain_1 :::"]"::: ) )) & (Bool (Set (Set (Var "w2")) ($#k4_rlsub_2 :::"|--"::: ) "(" (Set (Var "W")) "," (Set "(" ($#k1_rlvect_3 :::"Lin"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "y")) ($#k6_domain_1 :::"}"::: ) ) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "x2")) "," (Set "(" (Set (Var "r2")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "v")) ")" ) ($#k1_domain_1 :::"]"::: ) ))) "holds" (Bool (Set (Set "(" (Set (Var "w1")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "w2")) ")" ) ($#k4_rlsub_2 :::"|--"::: ) "(" (Set (Var "W")) "," (Set "(" ($#k1_rlvect_3 :::"Lin"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "y")) ($#k6_domain_1 :::"}"::: ) ) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set "(" (Set (Var "x1")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "x2")) ")" ) "," (Set "(" (Set "(" (Set (Var "r1")) ($#k7_real_1 :::"+"::: ) (Set (Var "r2")) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "v")) ")" ) ($#k1_domain_1 :::"]"::: ) )))))))))) ; theorem :: HAHNBAN:17 (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 "X")) "being" ($#m1_rlsub_1 :::"Subspace"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set "(" (Set (Var "X")) ($#k1_rlsub_2 :::"+"::: ) (Set "(" ($#k1_rlvect_3 :::"Lin"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "v")) ($#k6_domain_1 :::"}"::: ) ) ")" ) ")" ) (Bool "for" (Set (Var "W")) "being" ($#m1_rlsub_1 :::"Subspace"::: ) "of" (Set (Set (Var "X")) ($#k1_rlsub_2 :::"+"::: ) (Set "(" ($#k1_rlvect_3 :::"Lin"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "v")) ($#k6_domain_1 :::"}"::: ) ) ")" )) "st" (Bool (Bool (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set (Var "y"))) & (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set (Var "W"))) & (Bool (Bool "not" (Set (Var "v")) ($#r1_struct_0 :::"in"::: ) (Set (Var "X"))))) "holds" (Bool "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set "(" (Set (Var "X")) ($#k1_rlsub_2 :::"+"::: ) (Set "(" ($#k1_rlvect_3 :::"Lin"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "v")) ($#k6_domain_1 :::"}"::: ) ) ")" ) ")" ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "t")) "," (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Set (Var "w")) ($#k4_rlsub_2 :::"|--"::: ) "(" (Set (Var "W")) "," (Set "(" ($#k1_rlvect_3 :::"Lin"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "y")) ($#k6_domain_1 :::"}"::: ) ) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "x")) "," (Set "(" (Set (Var "r")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "v")) ")" ) ($#k1_domain_1 :::"]"::: ) ))) "holds" (Bool (Set (Set "(" (Set (Var "t")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "w")) ")" ) ($#k4_rlsub_2 :::"|--"::: ) "(" (Set (Var "W")) "," (Set "(" ($#k1_rlvect_3 :::"Lin"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "y")) ($#k6_domain_1 :::"}"::: ) ) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set "(" (Set (Var "t")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "x")) ")" ) "," (Set "(" (Set "(" (Set (Var "t")) ($#k8_real_1 :::"*"::: ) (Set (Var "r")) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "v")) ")" ) ($#k1_domain_1 :::"]"::: ) )))))))))) ; begin definitionlet "V" be ($#l1_rlvect_1 :::"RLSStruct"::: ) ; mode Functional of "V" is ($#m1_subset_1 :::"Function":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "V") "," (Set ($#k1_numbers :::"REAL"::: ) ); end; definitionlet "V" be ($#l1_rlvect_1 :::"RealLinearSpace":::); let "IT" be ($#m1_subset_1 :::"Functional":::) "of" (Set (Const "V")); attr "IT" is :::"subadditive"::: means :: HAHNBAN:def 1 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" "V" "holds" (Bool (Set "IT" ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "x")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "y")) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" "IT" ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" "IT" ($#k3_funct_2 :::"."::: ) (Set (Var "y")) ")" )))); attr "IT" is :::"additive"::: means :: HAHNBAN:def 2 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" "V" "holds" (Bool (Set "IT" ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "x")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "y")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" "IT" ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" "IT" ($#k3_funct_2 :::"."::: ) (Set (Var "y")) ")" )))); attr "IT" is :::"homogeneous"::: means :: HAHNBAN:def 3 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" "V" (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool (Set "IT" ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "r")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k8_real_1 :::"*"::: ) (Set "(" "IT" ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ))))); attr "IT" is :::"positively_homogeneous"::: means :: HAHNBAN:def 4 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" "V" (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "r")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set "IT" ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "r")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k8_real_1 :::"*"::: ) (Set "(" "IT" ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ))))); attr "IT" is :::"semi-homogeneous"::: means :: HAHNBAN:def 5 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" "V" (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "r")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set "IT" ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "r")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k8_real_1 :::"*"::: ) (Set "(" "IT" ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ))))); attr "IT" is :::"absolutely_homogeneous"::: means :: HAHNBAN:def 6 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" "V" (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool (Set "IT" ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "r")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k18_complex1 :::"abs"::: ) (Set (Var "r")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" "IT" ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ))))); attr "IT" is :::"0-preserving"::: means :: HAHNBAN:def 7 (Bool (Set "IT" ($#k3_funct_2 :::"."::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) "V" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )); end; :: deftheorem defines :::"subadditive"::: HAHNBAN:def 1 : (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "IT")) "being" ($#m1_subset_1 :::"Functional":::) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v1_hahnban :::"subadditive"::: ) ) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "holds" (Bool (Set (Set (Var "IT")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "x")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "y")) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" (Set (Var "IT")) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "IT")) ($#k3_funct_2 :::"."::: ) (Set (Var "y")) ")" )))) ")" ))); :: deftheorem defines :::"additive"::: HAHNBAN:def 2 : (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "IT")) "being" ($#m1_subset_1 :::"Functional":::) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v2_hahnban :::"additive"::: ) ) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "holds" (Bool (Set (Set (Var "IT")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "x")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "y")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "IT")) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "IT")) ($#k3_funct_2 :::"."::: ) (Set (Var "y")) ")" )))) ")" ))); :: deftheorem defines :::"homogeneous"::: HAHNBAN:def 3 : (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "IT")) "being" ($#m1_subset_1 :::"Functional":::) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v3_hahnban :::"homogeneous"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool (Set (Set (Var "IT")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "r")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k8_real_1 :::"*"::: ) (Set "(" (Set (Var "IT")) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ))))) ")" ))); :: deftheorem defines :::"positively_homogeneous"::: HAHNBAN:def 4 : (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "IT")) "being" ($#m1_subset_1 :::"Functional":::) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v4_hahnban :::"positively_homogeneous"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "r")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set (Var "IT")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "r")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k8_real_1 :::"*"::: ) (Set "(" (Set (Var "IT")) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ))))) ")" ))); :: deftheorem defines :::"semi-homogeneous"::: HAHNBAN:def 5 : (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "IT")) "being" ($#m1_subset_1 :::"Functional":::) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v5_hahnban :::"semi-homogeneous"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "r")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set (Var "IT")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "r")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k8_real_1 :::"*"::: ) (Set "(" (Set (Var "IT")) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ))))) ")" ))); :: deftheorem defines :::"absolutely_homogeneous"::: HAHNBAN:def 6 : (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "IT")) "being" ($#m1_subset_1 :::"Functional":::) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v6_hahnban :::"absolutely_homogeneous"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool (Set (Set (Var "IT")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "r")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k18_complex1 :::"abs"::: ) (Set (Var "r")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set (Var "IT")) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ))))) ")" ))); :: deftheorem defines :::"0-preserving"::: HAHNBAN:def 7 : (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "IT")) "being" ($#m1_subset_1 :::"Functional":::) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v7_hahnban :::"0-preserving"::: ) ) "iff" (Bool (Set (Set (Var "IT")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "V")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ))); registrationlet "V" be ($#l1_rlvect_1 :::"RealLinearSpace":::); cluster ($#v1_funct_1 :::"Function-like"::: ) bbbadV1_FUNCT_2((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "V") "," (Set ($#k1_numbers :::"REAL"::: ) )) ($#v2_hahnban :::"additive"::: ) -> ($#v1_hahnban :::"subadditive"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "V") "," (Set ($#k1_numbers :::"REAL"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) )); cluster ($#v1_funct_1 :::"Function-like"::: ) bbbadV1_FUNCT_2((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "V") "," (Set ($#k1_numbers :::"REAL"::: ) )) ($#v3_hahnban :::"homogeneous"::: ) -> ($#v4_hahnban :::"positively_homogeneous"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "V") "," (Set ($#k1_numbers :::"REAL"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) )); cluster ($#v1_funct_1 :::"Function-like"::: ) bbbadV1_FUNCT_2((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "V") "," (Set ($#k1_numbers :::"REAL"::: ) )) ($#v5_hahnban :::"semi-homogeneous"::: ) -> ($#v4_hahnban :::"positively_homogeneous"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "V") "," (Set ($#k1_numbers :::"REAL"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) )); cluster ($#v1_funct_1 :::"Function-like"::: ) bbbadV1_FUNCT_2((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "V") "," (Set ($#k1_numbers :::"REAL"::: ) )) ($#v5_hahnban :::"semi-homogeneous"::: ) -> ($#v7_hahnban :::"0-preserving"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "V") "," (Set ($#k1_numbers :::"REAL"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) )); cluster ($#v1_funct_1 :::"Function-like"::: ) bbbadV1_FUNCT_2((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "V") "," (Set ($#k1_numbers :::"REAL"::: ) )) ($#v6_hahnban :::"absolutely_homogeneous"::: ) -> ($#v5_hahnban :::"semi-homogeneous"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "V") "," (Set ($#k1_numbers :::"REAL"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) )); cluster ($#v1_funct_1 :::"Function-like"::: ) bbbadV1_FUNCT_2((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "V") "," (Set ($#k1_numbers :::"REAL"::: ) )) ($#v4_hahnban :::"positively_homogeneous"::: ) ($#v7_hahnban :::"0-preserving"::: ) -> ($#v5_hahnban :::"semi-homogeneous"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "V") "," (Set ($#k1_numbers :::"REAL"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) )); end; registrationlet "V" be ($#l1_rlvect_1 :::"RealLinearSpace":::); cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "V") ($#v4_relat_1 :::"-defined"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_partfun1 :::"total"::: ) bbbadV1_FUNCT_2((Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "V") "," (Set ($#k1_numbers :::"REAL"::: ) )) ($#v2_hahnban :::"additive"::: ) ($#v3_hahnban :::"homogeneous"::: ) ($#v6_hahnban :::"absolutely_homogeneous"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "V") "," (Set ($#k1_numbers :::"REAL"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) )); end; definitionlet "V" be ($#l1_rlvect_1 :::"RealLinearSpace":::); mode Banach-Functional of "V" is ($#v1_hahnban :::"subadditive"::: ) ($#v4_hahnban :::"positively_homogeneous"::: ) ($#m1_subset_1 :::"Functional":::) "of" "V"; mode linear-Functional of "V" is ($#v2_hahnban :::"additive"::: ) ($#v3_hahnban :::"homogeneous"::: ) ($#m1_subset_1 :::"Functional":::) "of" "V"; end; theorem :: HAHNBAN:18 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "L")) "being" ($#v3_hahnban :::"homogeneous"::: ) ($#m1_subset_1 :::"Functional":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "holds" (Bool (Set (Set (Var "L")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "v")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Set "(" (Set (Var "L")) ($#k3_funct_2 :::"."::: ) (Set (Var "v")) ")" )))))) ; theorem :: HAHNBAN:19 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "L")) "being" ($#m1_subset_1 :::"linear-Functional":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "v1")) "," (Set (Var "v2")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "holds" (Bool (Set (Set (Var "L")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "v1")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "v2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "L")) ($#k3_funct_2 :::"."::: ) (Set (Var "v1")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "L")) ($#k3_funct_2 :::"."::: ) (Set (Var "v2")) ")" )))))) ; theorem :: HAHNBAN:20 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "L")) "being" ($#v2_hahnban :::"additive"::: ) ($#m1_subset_1 :::"Functional":::) "of" (Set (Var "V")) "holds" (Bool (Set (Set (Var "L")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "V")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )))) ; theorem :: HAHNBAN:21 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "X")) "being" ($#m1_rlsub_1 :::"Subspace"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "fi")) "being" ($#m1_subset_1 :::"linear-Functional":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set "(" (Set (Var "X")) ($#k1_rlsub_2 :::"+"::: ) (Set "(" ($#k1_rlvect_3 :::"Lin"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "v")) ($#k6_domain_1 :::"}"::: ) ) ")" ) ")" ) "st" (Bool (Bool (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set (Var "y"))) & (Bool (Bool "not" (Set (Var "v")) ($#r1_struct_0 :::"in"::: ) (Set (Var "X"))))) "holds" (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "ex" (Set (Var "psi")) "being" ($#m1_subset_1 :::"linear-Functional":::) "of" (Set "(" (Set (Var "X")) ($#k1_rlsub_2 :::"+"::: ) (Set "(" ($#k1_rlvect_3 :::"Lin"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "v")) ($#k6_domain_1 :::"}"::: ) ) ")" ) ")" ) "st" (Bool "(" (Bool (Set (Set (Var "psi")) ($#k2_partfun1 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X")))) ($#r1_hidden :::"="::: ) (Set (Var "fi"))) & (Bool (Set (Set (Var "psi")) ($#k3_funct_2 :::"."::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Var "r"))) ")" )))))))) ; begin theorem :: HAHNBAN:22 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "X")) "being" ($#m1_rlsub_1 :::"Subspace"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "q")) "being" ($#m1_subset_1 :::"Banach-Functional":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "fi")) "being" ($#m1_subset_1 :::"linear-Functional":::) "of" (Set (Var "X")) "st" (Bool (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "v")))) "holds" (Bool (Set (Set (Var "fi")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "q")) ($#k3_funct_2 :::"."::: ) (Set (Var "v"))))) ")" )) "holds" (Bool "ex" (Set (Var "psi")) "being" ($#m1_subset_1 :::"linear-Functional":::) "of" (Set (Var "V")) "st" (Bool "(" (Bool (Set (Set (Var "psi")) ($#k2_partfun1 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X")))) ($#r1_hidden :::"="::: ) (Set (Var "fi"))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "holds" (Bool (Set (Set (Var "psi")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "q")) ($#k3_funct_2 :::"."::: ) (Set (Var "x")))) ")" ) ")" )))))) ; theorem :: HAHNBAN:23 (Bool "for" (Set (Var "V")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) "holds" (Bool (Set "the" ($#u1_normsp_0 :::"normF"::: ) "of" (Set (Var "V"))) "is" ($#v1_hahnban :::"subadditive"::: ) ($#v6_hahnban :::"absolutely_homogeneous"::: ) ($#m1_subset_1 :::"Functional":::) "of" (Set (Var "V")))) ; theorem :: HAHNBAN:24 (Bool "for" (Set (Var "V")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "X")) "being" ($#m1_rlsub_1 :::"Subspace"::: ) "of" (Set (Var "V")) (Bool "for" (Set (Var "fi")) "being" ($#m1_subset_1 :::"linear-Functional":::) "of" (Set (Var "X")) "st" (Bool (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "v")))) "holds" (Bool (Set (Set (Var "fi")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k1_normsp_0 :::"||."::: ) (Set (Var "v")) ($#k1_normsp_0 :::".||"::: ) ))) ")" )) "holds" (Bool "ex" (Set (Var "psi")) "being" ($#m1_subset_1 :::"linear-Functional":::) "of" (Set (Var "V")) "st" (Bool "(" (Bool (Set (Set (Var "psi")) ($#k2_partfun1 :::"|"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "X")))) ($#r1_hidden :::"="::: ) (Set (Var "fi"))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "holds" (Bool (Set (Set (Var "psi")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k1_normsp_0 :::"||."::: ) (Set (Var "x")) ($#k1_normsp_0 :::".||"::: ) )) ")" ) ")" ))))) ;