:: VFUNCT_1 semantic presentation begin definitionlet "C" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "V" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) ; let "f1", "f2" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "C")) "," (Set (Const "V")); func "f1" :::"+"::: "f2" -> ($#m1_subset_1 :::"PartFunc":::) "of" "C" "," "V" means :: VFUNCT_1:def 1 (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) it) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_relset_1 :::"dom"::: ) "f1" ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) "f2" ")" ))) & (Bool "(" "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "C" "st" (Bool (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) it))) "holds" (Bool (Set it ($#k7_partfun1 :::"/."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set "(" "f1" ($#k7_partfun1 :::"/."::: ) (Set (Var "c")) ")" ) ($#k1_algstr_0 :::"+"::: ) (Set "(" "f2" ($#k7_partfun1 :::"/."::: ) (Set (Var "c")) ")" ))) ")" ) ")" ); func "f1" :::"-"::: "f2" -> ($#m1_subset_1 :::"PartFunc":::) "of" "C" "," "V" means :: VFUNCT_1:def 2 (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) it) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_relset_1 :::"dom"::: ) "f1" ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) "f2" ")" ))) & (Bool "(" "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "C" "st" (Bool (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) it))) "holds" (Bool (Set it ($#k7_partfun1 :::"/."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set "(" "f1" ($#k7_partfun1 :::"/."::: ) (Set (Var "c")) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" "f2" ($#k7_partfun1 :::"/."::: ) (Set (Var "c")) ")" ))) ")" ) ")" ); end; :: deftheorem defines :::"+"::: VFUNCT_1:def 1 : (Bool "for" (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "V")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "," (Set (Var "b5")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f1")) ($#k1_vfunct_1 :::"+"::: ) (Set (Var "f2")))) "iff" (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "b5"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "f1")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "f2")) ")" ))) & (Bool "(" "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "C")) "st" (Bool (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "b5"))))) "holds" (Bool (Set (Set (Var "b5")) ($#k7_partfun1 :::"/."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f1")) ($#k7_partfun1 :::"/."::: ) (Set (Var "c")) ")" ) ($#k1_algstr_0 :::"+"::: ) (Set "(" (Set (Var "f2")) ($#k7_partfun1 :::"/."::: ) (Set (Var "c")) ")" ))) ")" ) ")" ) ")" )))); :: deftheorem defines :::"-"::: VFUNCT_1:def 2 : (Bool "for" (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "V")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "," (Set (Var "b5")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f1")) ($#k2_vfunct_1 :::"-"::: ) (Set (Var "f2")))) "iff" (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "b5"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "f1")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "f2")) ")" ))) & (Bool "(" "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "C")) "st" (Bool (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "b5"))))) "holds" (Bool (Set (Set (Var "b5")) ($#k7_partfun1 :::"/."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f1")) ($#k7_partfun1 :::"/."::: ) (Set (Var "c")) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "f2")) ($#k7_partfun1 :::"/."::: ) (Set (Var "c")) ")" ))) ")" ) ")" ) ")" )))); registrationlet "C" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "V" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) ; let "f1", "f2" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "C")) "," (Set (Const "V")); cluster (Set "f1" ($#k1_vfunct_1 :::"+"::: ) "f2") -> ($#v1_partfun1 :::"total"::: ) ; cluster (Set "f1" ($#k2_vfunct_1 :::"-"::: ) "f2") -> ($#v1_partfun1 :::"total"::: ) ; end; definitionlet "C" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "V" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rlvect_1 :::"RLSStruct"::: ) ; let "f1" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "C")) "," (Set ($#k1_numbers :::"REAL"::: ) ); let "f2" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "C")) "," (Set (Const "V")); func "f1" :::"(#)"::: "f2" -> ($#m1_subset_1 :::"PartFunc":::) "of" "C" "," "V" means :: VFUNCT_1:def 3 (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) it) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_relset_1 :::"dom"::: ) "f1" ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) "f2" ")" ))) & (Bool "(" "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "C" "st" (Bool (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) it))) "holds" (Bool (Set it ($#k7_partfun1 :::"/."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set "(" "f1" ($#k1_seq_1 :::"."::: ) (Set (Var "c")) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set "(" "f2" ($#k7_partfun1 :::"/."::: ) (Set (Var "c")) ")" ))) ")" ) ")" ); end; :: deftheorem defines :::"(#)"::: VFUNCT_1:def 3 : (Bool "for" (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "V")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rlvect_1 :::"RLSStruct"::: ) (Bool "for" (Set (Var "f1")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "f2")) "," (Set (Var "b5")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f1")) ($#k3_vfunct_1 :::"(#)"::: ) (Set (Var "f2")))) "iff" (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "b5"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "f1")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "f2")) ")" ))) & (Bool "(" "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "C")) "st" (Bool (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "b5"))))) "holds" (Bool (Set (Set (Var "b5")) ($#k7_partfun1 :::"/."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f1")) ($#k1_seq_1 :::"."::: ) (Set (Var "c")) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set (Var "f2")) ($#k7_partfun1 :::"/."::: ) (Set (Var "c")) ")" ))) ")" ) ")" ) ")" ))))); registrationlet "C" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "V" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rlvect_1 :::"RLSStruct"::: ) ; let "f1" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "C")) "," (Set ($#k1_numbers :::"REAL"::: ) ); let "f2" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "C")) "," (Set (Const "V")); cluster (Set "f1" ($#k3_vfunct_1 :::"(#)"::: ) "f2") -> ($#v1_partfun1 :::"total"::: ) ; end; definitionlet "C" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "V" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rlvect_1 :::"RLSStruct"::: ) ; let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "C")) "," (Set (Const "V")); let "r" be ($#m1_subset_1 :::"Real":::); func "r" :::"(#)"::: "f" -> ($#m1_subset_1 :::"PartFunc":::) "of" "C" "," "V" means :: VFUNCT_1:def 4 (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k1_relset_1 :::"dom"::: ) "f")) & (Bool "(" "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "C" "st" (Bool (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) it))) "holds" (Bool (Set it ($#k7_partfun1 :::"/."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set "r" ($#k1_rlvect_1 :::"*"::: ) (Set "(" "f" ($#k7_partfun1 :::"/."::: ) (Set (Var "c")) ")" ))) ")" ) ")" ); end; :: deftheorem defines :::"(#)"::: VFUNCT_1:def 4 : (Bool "for" (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "V")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rlvect_1 :::"RLSStruct"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set (Var "V")) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "b5")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k4_vfunct_1 :::"(#)"::: ) (Set (Var "f")))) "iff" (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "b5"))) ($#r1_hidden :::"="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) & (Bool "(" "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "C")) "st" (Bool (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "b5"))))) "holds" (Bool (Set (Set (Var "b5")) ($#k7_partfun1 :::"/."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "c")) ")" ))) ")" ) ")" ) ")" )))))); registrationlet "C" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "V" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rlvect_1 :::"RLSStruct"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "C")) "," (Set (Const "V")); let "r" be ($#m1_subset_1 :::"Real":::); cluster (Set "r" ($#k4_vfunct_1 :::"(#)"::: ) "f") -> ($#v1_partfun1 :::"total"::: ) ; end; definitionlet "C" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "V" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) ; let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "C")) "," (Set (Const "V")); func :::"-"::: "f" -> ($#m1_subset_1 :::"PartFunc":::) "of" "C" "," "V" means :: VFUNCT_1:def 5 (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k1_relset_1 :::"dom"::: ) "f")) & (Bool "(" "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "C" "st" (Bool (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) it))) "holds" (Bool (Set it ($#k7_partfun1 :::"/."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set ($#k4_algstr_0 :::"-"::: ) (Set "(" "f" ($#k7_partfun1 :::"/."::: ) (Set (Var "c")) ")" ))) ")" ) ")" ); end; :: deftheorem defines :::"-"::: VFUNCT_1:def 5 : (Bool "for" (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "V")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "b4")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k5_vfunct_1 :::"-"::: ) (Set (Var "f")))) "iff" (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "b4"))) ($#r1_hidden :::"="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) & (Bool "(" "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "C")) "st" (Bool (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "b4"))))) "holds" (Bool (Set (Set (Var "b4")) ($#k7_partfun1 :::"/."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set ($#k4_algstr_0 :::"-"::: ) (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "c")) ")" ))) ")" ) ")" ) ")" )))); registrationlet "C" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "V" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "C")) "," (Set (Const "V")); cluster (Set ($#k5_vfunct_1 :::"-"::: ) "f") -> ($#v1_partfun1 :::"total"::: ) ; end; theorem :: VFUNCT_1:1 (Bool "for" (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "V")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "f2")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set (Var "V")) (Bool "for" (Set (Var "f1")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "f1")) ($#k3_vfunct_1 :::"(#)"::: ) (Set (Var "f2")) ")" ) ")" ) ($#k7_subset_1 :::"\"::: ) (Set "(" (Set "(" (Set (Var "f1")) ($#k3_vfunct_1 :::"(#)"::: ) (Set (Var "f2")) ")" ) ($#k8_relset_1 :::"""::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "V")) ")" ) ($#k1_tarski :::"}"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "f1")) ")" ) ($#k7_subset_1 :::"\"::: ) (Set "(" (Set (Var "f1")) ($#k8_relset_1 :::"""::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k1_tarski :::"}"::: ) ) ")" ) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "f2")) ")" ) ($#k7_subset_1 :::"\"::: ) (Set "(" (Set (Var "f2")) ($#k8_relset_1 :::"""::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "V")) ")" ) ($#k1_tarski :::"}"::: ) ) ")" ) ")" ))))))) ; theorem :: VFUNCT_1:2 (Bool "for" (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "V")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Set ($#k3_normsp_0 :::"||."::: ) (Set (Var "f")) ($#k3_normsp_0 :::".||"::: ) ) ($#k8_relset_1 :::"""::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k1_tarski :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k8_relset_1 :::"""::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "V")) ")" ) ($#k1_tarski :::"}"::: ) ))) & (Bool (Set (Set "(" ($#k5_vfunct_1 :::"-"::: ) (Set (Var "f")) ")" ) ($#k8_relset_1 :::"""::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "V")) ")" ) ($#k1_tarski :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k8_relset_1 :::"""::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "V")) ")" ) ($#k1_tarski :::"}"::: ) ))) ")" )))) ; theorem :: VFUNCT_1:3 (Bool "for" (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "V")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set (Var "V")) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "r")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set "(" (Set (Var "r")) ($#k4_vfunct_1 :::"(#)"::: ) (Set (Var "f")) ")" ) ($#k8_relset_1 :::"""::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "V")) ")" ) ($#k1_tarski :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k8_relset_1 :::"""::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "V")) ")" ) ($#k1_tarski :::"}"::: ) ))))))) ; theorem :: VFUNCT_1:4 (Bool "for" (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "V")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set (Var "V")) "holds" (Bool (Set (Set (Var "f1")) ($#k1_vfunct_1 :::"+"::: ) (Set (Var "f2"))) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "f2")) ($#k1_vfunct_1 :::"+"::: ) (Set (Var "f1"))))))) ; definitionlet "C" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "V" be ($#l1_normsp_1 :::"RealNormSpace":::); let "f1", "f2" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "C")) "," (Set (Const "V")); :: original: :::"+"::: redefine func "f1" :::"+"::: "f2" -> ($#m1_subset_1 :::"PartFunc":::) "of" "C" "," "V"; commutativity (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "C")) "," (Set (Const "V")) "holds" (Bool (Set (Set (Var "f1")) ($#k1_vfunct_1 :::"+"::: ) (Set (Var "f2"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f2")) ($#k1_vfunct_1 :::"+"::: ) (Set (Var "f1"))))) ; end; theorem :: VFUNCT_1:5 (Bool "for" (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "V")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "," (Set (Var "f3")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set (Var "V")) "holds" (Bool (Set (Set "(" (Set (Var "f1")) ($#k6_vfunct_1 :::"+"::: ) (Set (Var "f2")) ")" ) ($#k6_vfunct_1 :::"+"::: ) (Set (Var "f3"))) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "f1")) ($#k6_vfunct_1 :::"+"::: ) (Set "(" (Set (Var "f2")) ($#k6_vfunct_1 :::"+"::: ) (Set (Var "f3")) ")" )))))) ; theorem :: VFUNCT_1:6 (Bool "for" (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "V")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "f3")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set (Var "V")) "holds" (Bool (Set (Set "(" (Set (Var "f1")) ($#k20_valued_1 :::"(#)"::: ) (Set (Var "f2")) ")" ) ($#k3_vfunct_1 :::"(#)"::: ) (Set (Var "f3"))) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "f1")) ($#k3_vfunct_1 :::"(#)"::: ) (Set "(" (Set (Var "f2")) ($#k3_vfunct_1 :::"(#)"::: ) (Set (Var "f3")) ")" ))))))) ; theorem :: VFUNCT_1:7 (Bool "for" (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "V")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "f3")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set (Var "V")) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set (Set "(" (Set (Var "f1")) ($#k3_valued_1 :::"+"::: ) (Set (Var "f2")) ")" ) ($#k3_vfunct_1 :::"(#)"::: ) (Set (Var "f3"))) ($#r2_relset_1 :::"="::: ) (Set (Set "(" (Set (Var "f1")) ($#k3_vfunct_1 :::"(#)"::: ) (Set (Var "f3")) ")" ) ($#k6_vfunct_1 :::"+"::: ) (Set "(" (Set (Var "f2")) ($#k3_vfunct_1 :::"(#)"::: ) (Set (Var "f3")) ")" ))))))) ; theorem :: VFUNCT_1:8 (Bool "for" (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "V")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set (Var "V")) (Bool "for" (Set (Var "f3")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set (Set (Var "f3")) ($#k3_vfunct_1 :::"(#)"::: ) (Set "(" (Set (Var "f1")) ($#k6_vfunct_1 :::"+"::: ) (Set (Var "f2")) ")" )) ($#r2_relset_1 :::"="::: ) (Set (Set "(" (Set (Var "f3")) ($#k3_vfunct_1 :::"(#)"::: ) (Set (Var "f1")) ")" ) ($#k6_vfunct_1 :::"+"::: ) (Set "(" (Set (Var "f3")) ($#k3_vfunct_1 :::"(#)"::: ) (Set (Var "f2")) ")" ))))))) ; theorem :: VFUNCT_1:9 (Bool "for" (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "V")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "f2")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set (Var "V")) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "f1")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set (Set (Var "r")) ($#k4_vfunct_1 :::"(#)"::: ) (Set "(" (Set (Var "f1")) ($#k3_vfunct_1 :::"(#)"::: ) (Set (Var "f2")) ")" )) ($#r2_relset_1 :::"="::: ) (Set (Set "(" (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "f1")) ")" ) ($#k3_vfunct_1 :::"(#)"::: ) (Set (Var "f2"))))))))) ; theorem :: VFUNCT_1:10 (Bool "for" (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "V")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "f2")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set (Var "V")) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "f1")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set (Set (Var "r")) ($#k4_vfunct_1 :::"(#)"::: ) (Set "(" (Set (Var "f1")) ($#k3_vfunct_1 :::"(#)"::: ) (Set (Var "f2")) ")" )) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "f1")) ($#k3_vfunct_1 :::"(#)"::: ) (Set "(" (Set (Var "r")) ($#k4_vfunct_1 :::"(#)"::: ) (Set (Var "f2")) ")" )))))))) ; theorem :: VFUNCT_1:11 (Bool "for" (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "V")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "f3")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set (Var "V")) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set (Set "(" (Set (Var "f1")) ($#k47_valued_1 :::"-"::: ) (Set (Var "f2")) ")" ) ($#k3_vfunct_1 :::"(#)"::: ) (Set (Var "f3"))) ($#r2_relset_1 :::"="::: ) (Set (Set "(" (Set (Var "f1")) ($#k3_vfunct_1 :::"(#)"::: ) (Set (Var "f3")) ")" ) ($#k2_vfunct_1 :::"-"::: ) (Set "(" (Set (Var "f2")) ($#k3_vfunct_1 :::"(#)"::: ) (Set (Var "f3")) ")" ))))))) ; theorem :: VFUNCT_1:12 (Bool "for" (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "V")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set (Var "V")) (Bool "for" (Set (Var "f3")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set (Set "(" (Set (Var "f3")) ($#k3_vfunct_1 :::"(#)"::: ) (Set (Var "f1")) ")" ) ($#k2_vfunct_1 :::"-"::: ) (Set "(" (Set (Var "f3")) ($#k3_vfunct_1 :::"(#)"::: ) (Set (Var "f2")) ")" )) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "f3")) ($#k3_vfunct_1 :::"(#)"::: ) (Set "(" (Set (Var "f1")) ($#k2_vfunct_1 :::"-"::: ) (Set (Var "f2")) ")" ))))))) ; theorem :: VFUNCT_1:13 (Bool "for" (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "V")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set (Var "V")) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool (Set (Set (Var "r")) ($#k4_vfunct_1 :::"(#)"::: ) (Set "(" (Set (Var "f1")) ($#k6_vfunct_1 :::"+"::: ) (Set (Var "f2")) ")" )) ($#r2_relset_1 :::"="::: ) (Set (Set "(" (Set (Var "r")) ($#k4_vfunct_1 :::"(#)"::: ) (Set (Var "f1")) ")" ) ($#k6_vfunct_1 :::"+"::: ) (Set "(" (Set (Var "r")) ($#k4_vfunct_1 :::"(#)"::: ) (Set (Var "f2")) ")" ))))))) ; theorem :: VFUNCT_1:14 (Bool "for" (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "V")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set (Var "V")) (Bool "for" (Set (Var "r")) "," (Set (Var "p")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool (Set (Set "(" (Set (Var "r")) ($#k8_real_1 :::"*"::: ) (Set (Var "p")) ")" ) ($#k4_vfunct_1 :::"(#)"::: ) (Set (Var "f"))) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "r")) ($#k4_vfunct_1 :::"(#)"::: ) (Set "(" (Set (Var "p")) ($#k4_vfunct_1 :::"(#)"::: ) (Set (Var "f")) ")" ))))))) ; theorem :: VFUNCT_1:15 (Bool "for" (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "V")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set (Var "V")) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool (Set (Set (Var "r")) ($#k4_vfunct_1 :::"(#)"::: ) (Set "(" (Set (Var "f1")) ($#k2_vfunct_1 :::"-"::: ) (Set (Var "f2")) ")" )) ($#r2_relset_1 :::"="::: ) (Set (Set "(" (Set (Var "r")) ($#k4_vfunct_1 :::"(#)"::: ) (Set (Var "f1")) ")" ) ($#k2_vfunct_1 :::"-"::: ) (Set "(" (Set (Var "r")) ($#k4_vfunct_1 :::"(#)"::: ) (Set (Var "f2")) ")" ))))))) ; theorem :: VFUNCT_1:16 (Bool "for" (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "V")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set (Var "V")) "holds" (Bool (Set (Set (Var "f1")) ($#k2_vfunct_1 :::"-"::: ) (Set (Var "f2"))) ($#r2_relset_1 :::"="::: ) (Set (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) ($#k4_vfunct_1 :::"(#)"::: ) (Set "(" (Set (Var "f2")) ($#k2_vfunct_1 :::"-"::: ) (Set (Var "f1")) ")" )))))) ; theorem :: VFUNCT_1:17 (Bool "for" (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "V")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "," (Set (Var "f3")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set (Var "V")) "holds" (Bool (Set (Set (Var "f1")) ($#k2_vfunct_1 :::"-"::: ) (Set "(" (Set (Var "f2")) ($#k6_vfunct_1 :::"+"::: ) (Set (Var "f3")) ")" )) ($#r2_relset_1 :::"="::: ) (Set (Set "(" (Set (Var "f1")) ($#k2_vfunct_1 :::"-"::: ) (Set (Var "f2")) ")" ) ($#k2_vfunct_1 :::"-"::: ) (Set (Var "f3"))))))) ; theorem :: VFUNCT_1:18 (Bool "for" (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "V")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set (Var "V")) "holds" (Bool (Set (Num 1) ($#k4_vfunct_1 :::"(#)"::: ) (Set (Var "f"))) ($#r2_relset_1 :::"="::: ) (Set (Var "f")))))) ; theorem :: VFUNCT_1:19 (Bool "for" (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "V")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "," (Set (Var "f3")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set (Var "V")) "holds" (Bool (Set (Set (Var "f1")) ($#k2_vfunct_1 :::"-"::: ) (Set "(" (Set (Var "f2")) ($#k2_vfunct_1 :::"-"::: ) (Set (Var "f3")) ")" )) ($#r2_relset_1 :::"="::: ) (Set (Set "(" (Set (Var "f1")) ($#k2_vfunct_1 :::"-"::: ) (Set (Var "f2")) ")" ) ($#k6_vfunct_1 :::"+"::: ) (Set (Var "f3"))))))) ; theorem :: VFUNCT_1:20 (Bool "for" (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "V")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "," (Set (Var "f3")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set (Var "V")) "holds" (Bool (Set (Set (Var "f1")) ($#k6_vfunct_1 :::"+"::: ) (Set "(" (Set (Var "f2")) ($#k2_vfunct_1 :::"-"::: ) (Set (Var "f3")) ")" )) ($#r2_relset_1 :::"="::: ) (Set (Set "(" (Set (Var "f1")) ($#k6_vfunct_1 :::"+"::: ) (Set (Var "f2")) ")" ) ($#k2_vfunct_1 :::"-"::: ) (Set (Var "f3"))))))) ; theorem :: VFUNCT_1:21 (Bool "for" (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "V")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "f2")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set (Var "V")) (Bool "for" (Set (Var "f1")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set ($#k3_normsp_0 :::"||."::: ) (Set "(" (Set (Var "f1")) ($#k3_vfunct_1 :::"(#)"::: ) (Set (Var "f2")) ")" ) ($#k3_normsp_0 :::".||"::: ) ) ($#r2_relset_1 :::"="::: ) (Set (Set "(" ($#k56_valued_1 :::"abs"::: ) (Set (Var "f1")) ")" ) ($#k20_valued_1 :::"(#)"::: ) (Set ($#k3_normsp_0 :::"||."::: ) (Set (Var "f2")) ($#k3_normsp_0 :::".||"::: ) ))))))) ; theorem :: VFUNCT_1:22 (Bool "for" (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "V")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set (Var "V")) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool (Set ($#k3_normsp_0 :::"||."::: ) (Set "(" (Set (Var "r")) ($#k4_vfunct_1 :::"(#)"::: ) (Set (Var "f")) ")" ) ($#k3_normsp_0 :::".||"::: ) ) ($#r2_relset_1 :::"="::: ) (Set (Set "(" ($#k18_complex1 :::"abs"::: ) (Set (Var "r")) ")" ) ($#k26_valued_1 :::"(#)"::: ) (Set ($#k3_normsp_0 :::"||."::: ) (Set (Var "f")) ($#k3_normsp_0 :::".||"::: ) ))))))) ; theorem :: VFUNCT_1:23 (Bool "for" (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "V")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set (Var "V")) "holds" (Bool (Set ($#k5_vfunct_1 :::"-"::: ) (Set (Var "f"))) ($#r2_relset_1 :::"="::: ) (Set (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) ($#k4_vfunct_1 :::"(#)"::: ) (Set (Var "f"))))))) ; theorem :: VFUNCT_1:24 (Bool "for" (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "V")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set (Var "V")) "holds" (Bool (Set ($#k5_vfunct_1 :::"-"::: ) (Set "(" ($#k5_vfunct_1 :::"-"::: ) (Set (Var "f")) ")" )) ($#r2_relset_1 :::"="::: ) (Set (Var "f")))))) ; theorem :: VFUNCT_1:25 (Bool "for" (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "V")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set (Var "V")) "holds" (Bool (Set (Set (Var "f1")) ($#k2_vfunct_1 :::"-"::: ) (Set (Var "f2"))) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "f1")) ($#k6_vfunct_1 :::"+"::: ) (Set "(" ($#k5_vfunct_1 :::"-"::: ) (Set (Var "f2")) ")" )))))) ; theorem :: VFUNCT_1:26 (Bool "for" (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "V")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set (Var "V")) "holds" (Bool (Set (Set (Var "f1")) ($#k2_vfunct_1 :::"-"::: ) (Set "(" ($#k5_vfunct_1 :::"-"::: ) (Set (Var "f2")) ")" )) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "f1")) ($#k6_vfunct_1 :::"+"::: ) (Set (Var "f2"))))))) ; theorem :: VFUNCT_1:27 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "V")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "f1")) ($#k6_vfunct_1 :::"+"::: ) (Set (Var "f2")) ")" ) ($#k2_partfun1 :::"|"::: ) (Set (Var "X"))) ($#r2_relset_1 :::"="::: ) (Set (Set "(" (Set (Var "f1")) ($#k2_partfun1 :::"|"::: ) (Set (Var "X")) ")" ) ($#k6_vfunct_1 :::"+"::: ) (Set "(" (Set (Var "f2")) ($#k2_partfun1 :::"|"::: ) (Set (Var "X")) ")" ))) & (Bool (Set (Set "(" (Set (Var "f1")) ($#k6_vfunct_1 :::"+"::: ) (Set (Var "f2")) ")" ) ($#k2_partfun1 :::"|"::: ) (Set (Var "X"))) ($#r2_relset_1 :::"="::: ) (Set (Set "(" (Set (Var "f1")) ($#k2_partfun1 :::"|"::: ) (Set (Var "X")) ")" ) ($#k6_vfunct_1 :::"+"::: ) (Set (Var "f2")))) & (Bool (Set (Set "(" (Set (Var "f1")) ($#k6_vfunct_1 :::"+"::: ) (Set (Var "f2")) ")" ) ($#k2_partfun1 :::"|"::: ) (Set (Var "X"))) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "f1")) ($#k6_vfunct_1 :::"+"::: ) (Set "(" (Set (Var "f2")) ($#k2_partfun1 :::"|"::: ) (Set (Var "X")) ")" ))) ")" ))))) ; theorem :: VFUNCT_1:28 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "V")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "f2")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set (Var "V")) (Bool "for" (Set (Var "f1")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "f1")) ($#k3_vfunct_1 :::"(#)"::: ) (Set (Var "f2")) ")" ) ($#k2_partfun1 :::"|"::: ) (Set (Var "X"))) ($#r2_relset_1 :::"="::: ) (Set (Set "(" (Set (Var "f1")) ($#k2_partfun1 :::"|"::: ) (Set (Var "X")) ")" ) ($#k3_vfunct_1 :::"(#)"::: ) (Set "(" (Set (Var "f2")) ($#k2_partfun1 :::"|"::: ) (Set (Var "X")) ")" ))) & (Bool (Set (Set "(" (Set (Var "f1")) ($#k3_vfunct_1 :::"(#)"::: ) (Set (Var "f2")) ")" ) ($#k2_partfun1 :::"|"::: ) (Set (Var "X"))) ($#r2_relset_1 :::"="::: ) (Set (Set "(" (Set (Var "f1")) ($#k2_partfun1 :::"|"::: ) (Set (Var "X")) ")" ) ($#k3_vfunct_1 :::"(#)"::: ) (Set (Var "f2")))) & (Bool (Set (Set "(" (Set (Var "f1")) ($#k3_vfunct_1 :::"(#)"::: ) (Set (Var "f2")) ")" ) ($#k2_partfun1 :::"|"::: ) (Set (Var "X"))) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "f1")) ($#k3_vfunct_1 :::"(#)"::: ) (Set "(" (Set (Var "f2")) ($#k2_partfun1 :::"|"::: ) (Set (Var "X")) ")" ))) ")" )))))) ; theorem :: VFUNCT_1:29 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "V")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Set "(" ($#k5_vfunct_1 :::"-"::: ) (Set (Var "f")) ")" ) ($#k2_partfun1 :::"|"::: ) (Set (Var "X"))) ($#r2_relset_1 :::"="::: ) (Set ($#k5_vfunct_1 :::"-"::: ) (Set "(" (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "X")) ")" ))) & (Bool (Set (Set ($#k3_normsp_0 :::"||."::: ) (Set (Var "f")) ($#k3_normsp_0 :::".||"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set (Var "X"))) ($#r2_relset_1 :::"="::: ) (Set ($#k3_normsp_0 :::"||."::: ) (Set "(" (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "X")) ")" ) ($#k3_normsp_0 :::".||"::: ) )) ")" ))))) ; theorem :: VFUNCT_1:30 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "V")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "f1")) ($#k2_vfunct_1 :::"-"::: ) (Set (Var "f2")) ")" ) ($#k2_partfun1 :::"|"::: ) (Set (Var "X"))) ($#r2_relset_1 :::"="::: ) (Set (Set "(" (Set (Var "f1")) ($#k2_partfun1 :::"|"::: ) (Set (Var "X")) ")" ) ($#k2_vfunct_1 :::"-"::: ) (Set "(" (Set (Var "f2")) ($#k2_partfun1 :::"|"::: ) (Set (Var "X")) ")" ))) & (Bool (Set (Set "(" (Set (Var "f1")) ($#k2_vfunct_1 :::"-"::: ) (Set (Var "f2")) ")" ) ($#k2_partfun1 :::"|"::: ) (Set (Var "X"))) ($#r2_relset_1 :::"="::: ) (Set (Set "(" (Set (Var "f1")) ($#k2_partfun1 :::"|"::: ) (Set (Var "X")) ")" ) ($#k2_vfunct_1 :::"-"::: ) (Set (Var "f2")))) & (Bool (Set (Set "(" (Set (Var "f1")) ($#k2_vfunct_1 :::"-"::: ) (Set (Var "f2")) ")" ) ($#k2_partfun1 :::"|"::: ) (Set (Var "X"))) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "f1")) ($#k2_vfunct_1 :::"-"::: ) (Set "(" (Set (Var "f2")) ($#k2_partfun1 :::"|"::: ) (Set (Var "X")) ")" ))) ")" ))))) ; theorem :: VFUNCT_1:31 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "V")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set (Var "V")) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool (Set (Set "(" (Set (Var "r")) ($#k4_vfunct_1 :::"(#)"::: ) (Set (Var "f")) ")" ) ($#k2_partfun1 :::"|"::: ) (Set (Var "X"))) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "r")) ($#k4_vfunct_1 :::"(#)"::: ) (Set "(" (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "X")) ")" )))))))) ; theorem :: VFUNCT_1:32 (Bool "for" (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "V")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set (Var "V")) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "f1")) "is" ($#v1_partfun1 :::"total"::: ) ) & (Bool (Set (Var "f2")) "is" ($#v1_partfun1 :::"total"::: ) )) "implies" (Bool (Set (Set (Var "f1")) ($#k6_vfunct_1 :::"+"::: ) (Set (Var "f2"))) "is" ($#v1_partfun1 :::"total"::: ) ) ")" & "(" (Bool (Bool (Set (Set (Var "f1")) ($#k6_vfunct_1 :::"+"::: ) (Set (Var "f2"))) "is" ($#v1_partfun1 :::"total"::: ) )) "implies" (Bool "(" (Bool (Set (Var "f1")) "is" ($#v1_partfun1 :::"total"::: ) ) & (Bool (Set (Var "f2")) "is" ($#v1_partfun1 :::"total"::: ) ) ")" ) ")" & "(" (Bool (Bool (Set (Var "f1")) "is" ($#v1_partfun1 :::"total"::: ) ) & (Bool (Set (Var "f2")) "is" ($#v1_partfun1 :::"total"::: ) )) "implies" (Bool (Set (Set (Var "f1")) ($#k2_vfunct_1 :::"-"::: ) (Set (Var "f2"))) "is" ($#v1_partfun1 :::"total"::: ) ) ")" & "(" (Bool (Bool (Set (Set (Var "f1")) ($#k2_vfunct_1 :::"-"::: ) (Set (Var "f2"))) "is" ($#v1_partfun1 :::"total"::: ) )) "implies" (Bool "(" (Bool (Set (Var "f1")) "is" ($#v1_partfun1 :::"total"::: ) ) & (Bool (Set (Var "f2")) "is" ($#v1_partfun1 :::"total"::: ) ) ")" ) ")" ")" )))) ; theorem :: VFUNCT_1:33 (Bool "for" (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "V")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "f2")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set (Var "V")) (Bool "for" (Set (Var "f1")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool "(" (Bool (Set (Var "f1")) "is" ($#v1_partfun1 :::"total"::: ) ) & (Bool (Set (Var "f2")) "is" ($#v1_partfun1 :::"total"::: ) ) ")" ) "iff" (Bool (Set (Set (Var "f1")) ($#k3_vfunct_1 :::"(#)"::: ) (Set (Var "f2"))) "is" ($#v1_partfun1 :::"total"::: ) ) ")" ))))) ; theorem :: VFUNCT_1:34 (Bool "for" (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "V")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set (Var "V")) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v1_partfun1 :::"total"::: ) ) "iff" (Bool (Set (Set (Var "r")) ($#k4_vfunct_1 :::"(#)"::: ) (Set (Var "f"))) "is" ($#v1_partfun1 :::"total"::: ) ) ")" ))))) ; theorem :: VFUNCT_1:35 (Bool "for" (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "V")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v1_partfun1 :::"total"::: ) ) "iff" (Bool (Set ($#k5_vfunct_1 :::"-"::: ) (Set (Var "f"))) "is" ($#v1_partfun1 :::"total"::: ) ) ")" )))) ; theorem :: VFUNCT_1:36 (Bool "for" (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "V")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v1_partfun1 :::"total"::: ) ) "iff" (Bool (Set ($#k3_normsp_0 :::"||."::: ) (Set (Var "f")) ($#k3_normsp_0 :::".||"::: ) ) "is" ($#v1_partfun1 :::"total"::: ) ) ")" )))) ; theorem :: VFUNCT_1:37 (Bool "for" (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "C")) (Bool "for" (Set (Var "V")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set (Var "V")) "st" (Bool (Bool (Set (Var "f1")) "is" ($#v1_partfun1 :::"total"::: ) ) & (Bool (Set (Var "f2")) "is" ($#v1_partfun1 :::"total"::: ) )) "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "f1")) ($#k6_vfunct_1 :::"+"::: ) (Set (Var "f2")) ")" ) ($#k7_partfun1 :::"/."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f1")) ($#k7_partfun1 :::"/."::: ) (Set (Var "c")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "f2")) ($#k7_partfun1 :::"/."::: ) (Set (Var "c")) ")" ))) & (Bool (Set (Set "(" (Set (Var "f1")) ($#k2_vfunct_1 :::"-"::: ) (Set (Var "f2")) ")" ) ($#k7_partfun1 :::"/."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f1")) ($#k7_partfun1 :::"/."::: ) (Set (Var "c")) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "f2")) ($#k7_partfun1 :::"/."::: ) (Set (Var "c")) ")" ))) ")" ))))) ; theorem :: VFUNCT_1:38 (Bool "for" (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "C")) (Bool "for" (Set (Var "V")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "f2")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set (Var "V")) (Bool "for" (Set (Var "f1")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "f1")) "is" ($#v1_partfun1 :::"total"::: ) ) & (Bool (Set (Var "f2")) "is" ($#v1_partfun1 :::"total"::: ) )) "holds" (Bool (Set (Set "(" (Set (Var "f1")) ($#k3_vfunct_1 :::"(#)"::: ) (Set (Var "f2")) ")" ) ($#k7_partfun1 :::"/."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f1")) ($#k1_seq_1 :::"."::: ) (Set (Var "c")) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set (Var "f2")) ($#k7_partfun1 :::"/."::: ) (Set (Var "c")) ")" )))))))) ; theorem :: VFUNCT_1:39 (Bool "for" (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "C")) (Bool "for" (Set (Var "V")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set (Var "V")) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "f")) "is" ($#v1_partfun1 :::"total"::: ) )) "holds" (Bool (Set (Set "(" (Set (Var "r")) ($#k4_vfunct_1 :::"(#)"::: ) (Set (Var "f")) ")" ) ($#k7_partfun1 :::"/."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "c")) ")" )))))))) ; theorem :: VFUNCT_1:40 (Bool "for" (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "C")) (Bool "for" (Set (Var "V")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set (Var "V")) "st" (Bool (Bool (Set (Var "f")) "is" ($#v1_partfun1 :::"total"::: ) )) "holds" (Bool "(" (Bool (Set (Set "(" ($#k5_vfunct_1 :::"-"::: ) (Set (Var "f")) ")" ) ($#k7_partfun1 :::"/."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set ($#k4_algstr_0 :::"-"::: ) (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "c")) ")" ))) & (Bool (Set (Set ($#k3_normsp_0 :::"||."::: ) (Set (Var "f")) ($#k3_normsp_0 :::".||"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set ($#k1_normsp_0 :::"||."::: ) (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "c")) ")" ) ($#k1_normsp_0 :::".||"::: ) )) ")" ))))) ; definitionlet "C" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "V" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_normsp_1 :::"NORMSTR"::: ) ; let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "C")) "," (Set (Const "V")); let "Y" be ($#m1_hidden :::"set"::: ) ; pred "f" :::"is_bounded_on"::: "Y" means :: VFUNCT_1:def 6 (Bool "ex" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "C" "st" (Bool (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set "Y" ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) "f" ")" )))) "holds" (Bool (Set ($#k1_normsp_0 :::"||."::: ) (Set "(" "f" ($#k7_partfun1 :::"/."::: ) (Set (Var "c")) ")" ) ($#k1_normsp_0 :::".||"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r"))))); end; :: deftheorem defines :::"is_bounded_on"::: VFUNCT_1:def 6 : (Bool "for" (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "V")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_normsp_1 :::"NORMSTR"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set (Var "V")) (Bool "for" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r1_vfunct_1 :::"is_bounded_on"::: ) (Set (Var "Y"))) "iff" (Bool "ex" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "C")) "st" (Bool (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "Y")) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")) ")" )))) "holds" (Bool (Set ($#k1_normsp_0 :::"||."::: ) (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "c")) ")" ) ($#k1_normsp_0 :::".||"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r"))))) ")" ))))); theorem :: VFUNCT_1:41 (Bool "for" (Set (Var "Y")) "," (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "V")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set (Var "V")) "st" (Bool (Bool (Set (Var "Y")) ($#r1_tarski :::"c="::: ) (Set (Var "X"))) & (Bool (Set (Var "f")) ($#r1_vfunct_1 :::"is_bounded_on"::: ) (Set (Var "X")))) "holds" (Bool (Set (Var "f")) ($#r1_vfunct_1 :::"is_bounded_on"::: ) (Set (Var "Y"))))))) ; theorem :: VFUNCT_1:42 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "V")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set (Var "V")) "st" (Bool (Bool (Set (Var "X")) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Var "f")) ($#r1_vfunct_1 :::"is_bounded_on"::: ) (Set (Var "X"))))))) ; theorem :: VFUNCT_1:43 (Bool "for" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "V")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set (Var "V")) "holds" (Bool (Set (Set ($#k6_numbers :::"0"::: ) ) ($#k4_vfunct_1 :::"(#)"::: ) (Set (Var "f"))) ($#r1_vfunct_1 :::"is_bounded_on"::: ) (Set (Var "Y"))))))) ; theorem :: VFUNCT_1:44 (Bool "for" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "V")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set (Var "V")) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "f")) ($#r1_vfunct_1 :::"is_bounded_on"::: ) (Set (Var "Y")))) "holds" (Bool (Set (Set (Var "r")) ($#k4_vfunct_1 :::"(#)"::: ) (Set (Var "f"))) ($#r1_vfunct_1 :::"is_bounded_on"::: ) (Set (Var "Y")))))))) ; theorem :: VFUNCT_1:45 (Bool "for" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "V")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set (Var "V")) "st" (Bool (Bool (Set (Var "f")) ($#r1_vfunct_1 :::"is_bounded_on"::: ) (Set (Var "Y")))) "holds" (Bool "(" (Bool (Set (Set ($#k3_normsp_0 :::"||."::: ) (Set (Var "f")) ($#k3_normsp_0 :::".||"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set (Var "Y"))) "is" ($#v1_comseq_2 :::"bounded"::: ) ) & (Bool (Set ($#k5_vfunct_1 :::"-"::: ) (Set (Var "f"))) ($#r1_vfunct_1 :::"is_bounded_on"::: ) (Set (Var "Y"))) ")" ))))) ; theorem :: VFUNCT_1:46 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "V")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set (Var "V")) "st" (Bool (Bool (Set (Var "f1")) ($#r1_vfunct_1 :::"is_bounded_on"::: ) (Set (Var "X"))) & (Bool (Set (Var "f2")) ($#r1_vfunct_1 :::"is_bounded_on"::: ) (Set (Var "Y")))) "holds" (Bool (Set (Set (Var "f1")) ($#k6_vfunct_1 :::"+"::: ) (Set (Var "f2"))) ($#r1_vfunct_1 :::"is_bounded_on"::: ) (Set (Set (Var "X")) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "Y")))))))) ; theorem :: VFUNCT_1:47 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "V")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "f2")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set (Var "V")) (Bool "for" (Set (Var "f1")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Set (Var "f1")) ($#k2_partfun1 :::"|"::: ) (Set (Var "X"))) "is" ($#v1_comseq_2 :::"bounded"::: ) ) & (Bool (Set (Var "f2")) ($#r1_vfunct_1 :::"is_bounded_on"::: ) (Set (Var "Y")))) "holds" (Bool (Set (Set (Var "f1")) ($#k3_vfunct_1 :::"(#)"::: ) (Set (Var "f2"))) ($#r1_vfunct_1 :::"is_bounded_on"::: ) (Set (Set (Var "X")) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "Y"))))))))) ; theorem :: VFUNCT_1:48 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "V")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set (Var "V")) "st" (Bool (Bool (Set (Var "f1")) ($#r1_vfunct_1 :::"is_bounded_on"::: ) (Set (Var "X"))) & (Bool (Set (Var "f2")) ($#r1_vfunct_1 :::"is_bounded_on"::: ) (Set (Var "Y")))) "holds" (Bool (Set (Set (Var "f1")) ($#k2_vfunct_1 :::"-"::: ) (Set (Var "f2"))) ($#r1_vfunct_1 :::"is_bounded_on"::: ) (Set (Set (Var "X")) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "Y")))))))) ; theorem :: VFUNCT_1:49 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "V")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set (Var "V")) "st" (Bool (Bool (Set (Var "f")) ($#r1_vfunct_1 :::"is_bounded_on"::: ) (Set (Var "X"))) & (Bool (Set (Var "f")) ($#r1_vfunct_1 :::"is_bounded_on"::: ) (Set (Var "Y")))) "holds" (Bool (Set (Var "f")) ($#r1_vfunct_1 :::"is_bounded_on"::: ) (Set (Set (Var "X")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "Y")))))))) ; theorem :: VFUNCT_1:50 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "V")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set (Var "V")) "st" (Bool (Bool (Set (Set (Var "f1")) ($#k2_partfun1 :::"|"::: ) (Set (Var "X"))) "is" bbbadV3_FUNCT_1()) & (Bool (Set (Set (Var "f2")) ($#k2_partfun1 :::"|"::: ) (Set (Var "Y"))) "is" bbbadV3_FUNCT_1())) "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "f1")) ($#k6_vfunct_1 :::"+"::: ) (Set (Var "f2")) ")" ) ($#k2_partfun1 :::"|"::: ) (Set "(" (Set (Var "X")) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "Y")) ")" )) "is" bbbadV3_FUNCT_1()) & (Bool (Set (Set "(" (Set (Var "f1")) ($#k2_vfunct_1 :::"-"::: ) (Set (Var "f2")) ")" ) ($#k2_partfun1 :::"|"::: ) (Set "(" (Set (Var "X")) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "Y")) ")" )) "is" bbbadV3_FUNCT_1()) ")" ))))) ; theorem :: VFUNCT_1:51 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "V")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "f2")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set (Var "V")) (Bool "for" (Set (Var "f1")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Set (Var "f1")) ($#k2_partfun1 :::"|"::: ) (Set (Var "X"))) "is" bbbadV3_FUNCT_1()) & (Bool (Set (Set (Var "f2")) ($#k2_partfun1 :::"|"::: ) (Set (Var "Y"))) "is" bbbadV3_FUNCT_1())) "holds" (Bool (Set (Set "(" (Set (Var "f1")) ($#k3_vfunct_1 :::"(#)"::: ) (Set (Var "f2")) ")" ) ($#k2_partfun1 :::"|"::: ) (Set "(" (Set (Var "X")) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "Y")) ")" )) "is" bbbadV3_FUNCT_1())))))) ; theorem :: VFUNCT_1:52 (Bool "for" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "V")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set (Var "V")) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "Y"))) "is" bbbadV3_FUNCT_1())) "holds" (Bool (Set (Set "(" (Set (Var "p")) ($#k4_vfunct_1 :::"(#)"::: ) (Set (Var "f")) ")" ) ($#k2_partfun1 :::"|"::: ) (Set (Var "Y"))) "is" bbbadV3_FUNCT_1())))))) ; theorem :: VFUNCT_1:53 (Bool "for" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "V")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set (Var "V")) "st" (Bool (Bool (Set (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "Y"))) "is" bbbadV3_FUNCT_1())) "holds" (Bool "(" (Bool (Set (Set ($#k3_normsp_0 :::"||."::: ) (Set (Var "f")) ($#k3_normsp_0 :::".||"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set (Var "Y"))) "is" bbbadV3_FUNCT_1()) & (Bool (Set (Set "(" ($#k5_vfunct_1 :::"-"::: ) (Set (Var "f")) ")" ) ($#k2_partfun1 :::"|"::: ) (Set (Var "Y"))) "is" bbbadV3_FUNCT_1()) ")" ))))) ; theorem :: VFUNCT_1:54 (Bool "for" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "V")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set (Var "V")) "st" (Bool (Bool (Set (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "Y"))) "is" bbbadV3_FUNCT_1())) "holds" (Bool (Set (Var "f")) ($#r1_vfunct_1 :::"is_bounded_on"::: ) (Set (Var "Y"))))))) ; theorem :: VFUNCT_1:55 (Bool "for" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "V")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set (Var "V")) "st" (Bool (Bool (Set (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "Y"))) "is" bbbadV3_FUNCT_1())) "holds" (Bool "(" (Bool "(" "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool (Set (Set (Var "r")) ($#k4_vfunct_1 :::"(#)"::: ) (Set (Var "f"))) ($#r1_vfunct_1 :::"is_bounded_on"::: ) (Set (Var "Y"))) ")" ) & (Bool (Set ($#k5_vfunct_1 :::"-"::: ) (Set (Var "f"))) ($#r1_vfunct_1 :::"is_bounded_on"::: ) (Set (Var "Y"))) & (Bool (Set (Set ($#k3_normsp_0 :::"||."::: ) (Set (Var "f")) ($#k3_normsp_0 :::".||"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set (Var "Y"))) "is" ($#v1_comseq_2 :::"bounded"::: ) ) ")" ))))) ; theorem :: VFUNCT_1:56 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "V")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set (Var "V")) "st" (Bool (Bool (Set (Var "f1")) ($#r1_vfunct_1 :::"is_bounded_on"::: ) (Set (Var "X"))) & (Bool (Set (Set (Var "f2")) ($#k2_partfun1 :::"|"::: ) (Set (Var "Y"))) "is" bbbadV3_FUNCT_1())) "holds" (Bool (Set (Set (Var "f1")) ($#k6_vfunct_1 :::"+"::: ) (Set (Var "f2"))) ($#r1_vfunct_1 :::"is_bounded_on"::: ) (Set (Set (Var "X")) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "Y")))))))) ; theorem :: VFUNCT_1:57 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "V")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set (Var "V")) "st" (Bool (Bool (Set (Var "f1")) ($#r1_vfunct_1 :::"is_bounded_on"::: ) (Set (Var "X"))) & (Bool (Set (Set (Var "f2")) ($#k2_partfun1 :::"|"::: ) (Set (Var "Y"))) "is" bbbadV3_FUNCT_1())) "holds" (Bool "(" (Bool (Set (Set (Var "f1")) ($#k2_vfunct_1 :::"-"::: ) (Set (Var "f2"))) ($#r1_vfunct_1 :::"is_bounded_on"::: ) (Set (Set (Var "X")) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "Y")))) & (Bool (Set (Set (Var "f2")) ($#k2_vfunct_1 :::"-"::: ) (Set (Var "f1"))) ($#r1_vfunct_1 :::"is_bounded_on"::: ) (Set (Set (Var "X")) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "Y")))) ")" ))))) ;