:: FUNCSDOM semantic presentation begin definitionlet "A" be ($#m1_hidden :::"set"::: ) ; let "B" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "F" be ($#m1_subset_1 :::"BinOp":::) "of" (Set "(" ($#k9_funct_2 :::"Funcs"::: ) "(" (Set (Const "A")) "," (Set (Const "B")) ")" ")" ); let "f", "g" be ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set (Const "A")) "," (Set (Const "B")) ")" ); :: original: :::"."::: redefine func "F" :::"."::: "(" "f" "," "g" ")" -> ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" "A" "," "B" ")" ); end; definitionlet "A", "B", "C", "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "F" be ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Const "C")) "," (Set (Const "D")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "(" ($#k9_funct_2 :::"Funcs"::: ) "(" (Set (Const "A")) "," (Set (Const "B")) ")" ")" ); let "cd" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Const "C")) "," (Set (Const "D")) ($#k2_zfmisc_1 :::":]"::: ) ); :: original: :::"."::: redefine func "F" :::"."::: "cd" -> ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" "A" "," "B" ")" ); end; definitionlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "Z" be ($#m1_hidden :::"set"::: ) ; let "F" be ($#m1_subset_1 :::"BinOp":::) "of" (Set (Const "X")); let "f", "g" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "Z")) "," (Set (Const "X")); :: original: :::".:"::: redefine func "F" :::".:"::: "(" "f" "," "g" ")" -> ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" "Z" "," "X" ")" ); end; definitionlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "Z" be ($#m1_hidden :::"set"::: ) ; let "F" be ($#m1_subset_1 :::"BinOp":::) "of" (Set (Const "X")); let "a" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "X")); let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "Z")) "," (Set (Const "X")); :: original: :::"[;]"::: redefine func "F" :::"[;]"::: "(" "a" "," "f" ")" -> ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" "Z" "," "X" ")" ); end; definitionlet "A" be ($#m1_hidden :::"set"::: ) ; func :::"RealFuncAdd"::: "A" -> ($#m1_subset_1 :::"BinOp":::) "of" (Set "(" ($#k9_funct_2 :::"Funcs"::: ) "(" "A" "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ")" ) means :: FUNCSDOM:def 1 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" "A" "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ) "holds" (Bool (Set it ($#k1_funcsdom :::"."::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ) ($#r2_funct_2 :::"="::: ) (Set (Set ($#k33_binop_2 :::"addreal"::: ) ) ($#k3_funcsdom :::".:"::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ))); end; :: deftheorem defines :::"RealFuncAdd"::: FUNCSDOM:def 1 : (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set "(" ($#k9_funct_2 :::"Funcs"::: ) "(" (Set (Var "A")) "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ")" ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k5_funcsdom :::"RealFuncAdd"::: ) (Set (Var "A")))) "iff" (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set (Var "A")) "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ) "holds" (Bool (Set (Set (Var "b2")) ($#k1_funcsdom :::"."::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ) ($#r2_funct_2 :::"="::: ) (Set (Set ($#k33_binop_2 :::"addreal"::: ) ) ($#k3_funcsdom :::".:"::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ))) ")" ))); definitionlet "A" be ($#m1_hidden :::"set"::: ) ; func :::"RealFuncMult"::: "A" -> ($#m1_subset_1 :::"BinOp":::) "of" (Set "(" ($#k9_funct_2 :::"Funcs"::: ) "(" "A" "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ")" ) means :: FUNCSDOM:def 2 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" "A" "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ) "holds" (Bool (Set it ($#k1_funcsdom :::"."::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ) ($#r2_funct_2 :::"="::: ) (Set (Set ($#k35_binop_2 :::"multreal"::: ) ) ($#k3_funcsdom :::".:"::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ))); end; :: deftheorem defines :::"RealFuncMult"::: FUNCSDOM:def 2 : (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set "(" ($#k9_funct_2 :::"Funcs"::: ) "(" (Set (Var "A")) "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ")" ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k6_funcsdom :::"RealFuncMult"::: ) (Set (Var "A")))) "iff" (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set (Var "A")) "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ) "holds" (Bool (Set (Set (Var "b2")) ($#k1_funcsdom :::"."::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ) ($#r2_funct_2 :::"="::: ) (Set (Set ($#k35_binop_2 :::"multreal"::: ) ) ($#k3_funcsdom :::".:"::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ))) ")" ))); definitionlet "A" be ($#m1_hidden :::"set"::: ) ; func :::"RealFuncExtMult"::: "A" -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set "(" ($#k9_funct_2 :::"Funcs"::: ) "(" "A" "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "(" ($#k9_funct_2 :::"Funcs"::: ) "(" "A" "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ")" ) means :: FUNCSDOM:def 3 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "f")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" "A" "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ) "holds" (Bool (Set it ($#k2_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "f")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set ($#k35_binop_2 :::"multreal"::: ) ) ($#k4_funcsdom :::"[;]"::: ) "(" (Set (Var "a")) "," (Set (Var "f")) ")" )))); end; :: deftheorem defines :::"RealFuncExtMult"::: FUNCSDOM:def 3 : (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set "(" ($#k9_funct_2 :::"Funcs"::: ) "(" (Set (Var "A")) "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "(" ($#k9_funct_2 :::"Funcs"::: ) "(" (Set (Var "A")) "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ")" ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k7_funcsdom :::"RealFuncExtMult"::: ) (Set (Var "A")))) "iff" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "f")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set (Var "A")) "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ) "holds" (Bool (Set (Set (Var "b2")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "f")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set ($#k35_binop_2 :::"multreal"::: ) ) ($#k4_funcsdom :::"[;]"::: ) "(" (Set (Var "a")) "," (Set (Var "f")) ")" )))) ")" ))); definitionlet "A" be ($#m1_hidden :::"set"::: ) ; func :::"RealFuncZero"::: "A" -> ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" "A" "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ) equals :: FUNCSDOM:def 4 (Set "A" ($#k8_funcop_1 :::"-->"::: ) (Set ($#k6_numbers :::"0"::: ) )); end; :: deftheorem defines :::"RealFuncZero"::: FUNCSDOM:def 4 : (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k8_funcsdom :::"RealFuncZero"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k8_funcop_1 :::"-->"::: ) (Set ($#k6_numbers :::"0"::: ) )))); definitionlet "A" be ($#m1_hidden :::"set"::: ) ; func :::"RealFuncUnit"::: "A" -> ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" "A" "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ) equals :: FUNCSDOM:def 5 (Set "A" ($#k8_funcop_1 :::"-->"::: ) (Num 1)); end; :: deftheorem defines :::"RealFuncUnit"::: FUNCSDOM:def 5 : (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k9_funcsdom :::"RealFuncUnit"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k8_funcop_1 :::"-->"::: ) (Num 1)))); theorem :: FUNCSDOM:1 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "h")) "," (Set (Var "f")) "," (Set (Var "g")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set (Var "A")) "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ) "holds" (Bool "(" (Bool (Set (Var "h")) ($#r2_funct_2 :::"="::: ) (Set (Set "(" ($#k5_funcsdom :::"RealFuncAdd"::: ) (Set (Var "A")) ")" ) ($#k1_funcsdom :::"."::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" )) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "A")) "holds" (Bool (Set (Set (Var "h")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "g")) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" )))) ")" ))) ; theorem :: FUNCSDOM:2 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "h")) "," (Set (Var "f")) "," (Set (Var "g")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set (Var "A")) "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ) "holds" (Bool "(" (Bool (Set (Var "h")) ($#r2_funct_2 :::"="::: ) (Set (Set "(" ($#k6_funcsdom :::"RealFuncMult"::: ) (Set (Var "A")) ")" ) ($#k1_funcsdom :::"."::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" )) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "A")) "holds" (Bool (Set (Set (Var "h")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set (Var "g")) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" )))) ")" ))) ; theorem :: FUNCSDOM:3 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k8_funcsdom :::"RealFuncZero"::: ) (Set (Var "A"))) ($#r1_hidden :::"<>"::: ) (Set ($#k9_funcsdom :::"RealFuncUnit"::: ) (Set (Var "A"))))) ; theorem :: FUNCSDOM:4 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "h")) "," (Set (Var "f")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set (Var "A")) "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool "(" (Bool (Set (Var "h")) ($#r2_funct_2 :::"="::: ) (Set (Set "(" ($#k7_funcsdom :::"RealFuncExtMult"::: ) (Set (Var "A")) ")" ) ($#k2_funcsdom :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "a")) "," (Set (Var "f")) ($#k1_domain_1 :::"]"::: ) ))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "A")) "holds" (Bool (Set (Set (Var "h")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k8_real_1 :::"*"::: ) (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" )))) ")" )))) ; theorem :: FUNCSDOM:5 (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set (Var "A")) "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ) "holds" (Bool (Set (Set "(" ($#k5_funcsdom :::"RealFuncAdd"::: ) (Set (Var "A")) ")" ) ($#k1_funcsdom :::"."::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ) ($#r2_funct_2 :::"="::: ) (Set (Set "(" ($#k5_funcsdom :::"RealFuncAdd"::: ) (Set (Var "A")) ")" ) ($#k1_funcsdom :::"."::: ) "(" (Set (Var "g")) "," (Set (Var "f")) ")" )))) ; theorem :: FUNCSDOM:6 (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set (Var "A")) "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ) "holds" (Bool (Set (Set "(" ($#k5_funcsdom :::"RealFuncAdd"::: ) (Set (Var "A")) ")" ) ($#k1_funcsdom :::"."::: ) "(" (Set (Var "f")) "," (Set "(" (Set "(" ($#k5_funcsdom :::"RealFuncAdd"::: ) (Set (Var "A")) ")" ) ($#k1_funcsdom :::"."::: ) "(" (Set (Var "g")) "," (Set (Var "h")) ")" ")" ) ")" ) ($#r2_funct_2 :::"="::: ) (Set (Set "(" ($#k5_funcsdom :::"RealFuncAdd"::: ) (Set (Var "A")) ")" ) ($#k1_funcsdom :::"."::: ) "(" (Set "(" (Set "(" ($#k5_funcsdom :::"RealFuncAdd"::: ) (Set (Var "A")) ")" ) ($#k1_funcsdom :::"."::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ")" ) "," (Set (Var "h")) ")" )))) ; theorem :: FUNCSDOM:7 (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set (Var "A")) "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ) "holds" (Bool (Set (Set "(" ($#k6_funcsdom :::"RealFuncMult"::: ) (Set (Var "A")) ")" ) ($#k1_funcsdom :::"."::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ) ($#r2_funct_2 :::"="::: ) (Set (Set "(" ($#k6_funcsdom :::"RealFuncMult"::: ) (Set (Var "A")) ")" ) ($#k1_funcsdom :::"."::: ) "(" (Set (Var "g")) "," (Set (Var "f")) ")" )))) ; theorem :: FUNCSDOM:8 (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set (Var "A")) "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ) "holds" (Bool (Set (Set "(" ($#k6_funcsdom :::"RealFuncMult"::: ) (Set (Var "A")) ")" ) ($#k1_funcsdom :::"."::: ) "(" (Set (Var "f")) "," (Set "(" (Set "(" ($#k6_funcsdom :::"RealFuncMult"::: ) (Set (Var "A")) ")" ) ($#k1_funcsdom :::"."::: ) "(" (Set (Var "g")) "," (Set (Var "h")) ")" ")" ) ")" ) ($#r2_funct_2 :::"="::: ) (Set (Set "(" ($#k6_funcsdom :::"RealFuncMult"::: ) (Set (Var "A")) ")" ) ($#k1_funcsdom :::"."::: ) "(" (Set "(" (Set "(" ($#k6_funcsdom :::"RealFuncMult"::: ) (Set (Var "A")) ")" ) ($#k1_funcsdom :::"."::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ")" ) "," (Set (Var "h")) ")" )))) ; theorem :: FUNCSDOM:9 (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set (Var "A")) "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ) "holds" (Bool (Set (Set "(" ($#k6_funcsdom :::"RealFuncMult"::: ) (Set (Var "A")) ")" ) ($#k1_funcsdom :::"."::: ) "(" (Set "(" ($#k9_funcsdom :::"RealFuncUnit"::: ) (Set (Var "A")) ")" ) "," (Set (Var "f")) ")" ) ($#r2_funct_2 :::"="::: ) (Set (Var "f"))))) ; theorem :: FUNCSDOM:10 (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set (Var "A")) "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ) "holds" (Bool (Set (Set "(" ($#k5_funcsdom :::"RealFuncAdd"::: ) (Set (Var "A")) ")" ) ($#k1_funcsdom :::"."::: ) "(" (Set "(" ($#k8_funcsdom :::"RealFuncZero"::: ) (Set (Var "A")) ")" ) "," (Set (Var "f")) ")" ) ($#r2_funct_2 :::"="::: ) (Set (Var "f"))))) ; theorem :: FUNCSDOM:11 (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set (Var "A")) "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ) "holds" (Bool (Set (Set "(" ($#k5_funcsdom :::"RealFuncAdd"::: ) (Set (Var "A")) ")" ) ($#k1_funcsdom :::"."::: ) "(" (Set (Var "f")) "," (Set "(" (Set "(" ($#k7_funcsdom :::"RealFuncExtMult"::: ) (Set (Var "A")) ")" ) ($#k3_funct_2 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) "," (Set (Var "f")) ($#k1_domain_1 :::"]"::: ) ) ")" ) ")" ) ($#r2_funct_2 :::"="::: ) (Set ($#k8_funcsdom :::"RealFuncZero"::: ) (Set (Var "A")))))) ; theorem :: FUNCSDOM:12 (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set (Var "A")) "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ) "holds" (Bool (Set (Set "(" ($#k7_funcsdom :::"RealFuncExtMult"::: ) (Set (Var "A")) ")" ) ($#k2_binop_1 :::"."::: ) "(" (Num 1) "," (Set (Var "f")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "f"))))) ; theorem :: FUNCSDOM:13 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set (Var "A")) "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ) "holds" (Bool (Set (Set "(" ($#k7_funcsdom :::"RealFuncExtMult"::: ) (Set (Var "A")) ")" ) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set "(" (Set "(" ($#k7_funcsdom :::"RealFuncExtMult"::: ) (Set (Var "A")) ")" ) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "b")) "," (Set (Var "f")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k7_funcsdom :::"RealFuncExtMult"::: ) (Set (Var "A")) ")" ) ($#k2_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "a")) ($#k8_real_1 :::"*"::: ) (Set (Var "b")) ")" ) "," (Set (Var "f")) ")" ))))) ; theorem :: FUNCSDOM:14 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set (Var "A")) "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ) "holds" (Bool (Set (Set "(" ($#k5_funcsdom :::"RealFuncAdd"::: ) (Set (Var "A")) ")" ) ($#k1_funcsdom :::"."::: ) "(" (Set "(" (Set "(" ($#k7_funcsdom :::"RealFuncExtMult"::: ) (Set (Var "A")) ")" ) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "f")) ")" ")" ) "," (Set "(" (Set "(" ($#k7_funcsdom :::"RealFuncExtMult"::: ) (Set (Var "A")) ")" ) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "b")) "," (Set (Var "f")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k7_funcsdom :::"RealFuncExtMult"::: ) (Set (Var "A")) ")" ) ($#k2_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "a")) ($#k7_real_1 :::"+"::: ) (Set (Var "b")) ")" ) "," (Set (Var "f")) ")" ))))) ; theorem :: FUNCSDOM:15 (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set (Var "A")) "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ) "holds" (Bool (Set (Set "(" ($#k6_funcsdom :::"RealFuncMult"::: ) (Set (Var "A")) ")" ) ($#k1_funcsdom :::"."::: ) "(" (Set (Var "f")) "," (Set "(" (Set "(" ($#k5_funcsdom :::"RealFuncAdd"::: ) (Set (Var "A")) ")" ) ($#k1_funcsdom :::"."::: ) "(" (Set (Var "g")) "," (Set (Var "h")) ")" ")" ) ")" ) ($#r2_funct_2 :::"="::: ) (Set (Set "(" ($#k5_funcsdom :::"RealFuncAdd"::: ) (Set (Var "A")) ")" ) ($#k1_funcsdom :::"."::: ) "(" (Set "(" (Set "(" ($#k6_funcsdom :::"RealFuncMult"::: ) (Set (Var "A")) ")" ) ($#k1_funcsdom :::"."::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ")" ) "," (Set "(" (Set "(" ($#k6_funcsdom :::"RealFuncMult"::: ) (Set (Var "A")) ")" ) ($#k1_funcsdom :::"."::: ) "(" (Set (Var "f")) "," (Set (Var "h")) ")" ")" ) ")" )))) ; theorem :: FUNCSDOM:16 (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set (Var "A")) "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool (Set (Set "(" ($#k6_funcsdom :::"RealFuncMult"::: ) (Set (Var "A")) ")" ) ($#k1_funcsdom :::"."::: ) "(" (Set "(" (Set "(" ($#k7_funcsdom :::"RealFuncExtMult"::: ) (Set (Var "A")) ")" ) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "f")) ")" ")" ) "," (Set (Var "g")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k7_funcsdom :::"RealFuncExtMult"::: ) (Set (Var "A")) ")" ) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set "(" (Set "(" ($#k6_funcsdom :::"RealFuncMult"::: ) (Set (Var "A")) ")" ) ($#k1_funcsdom :::"."::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ")" ) ")" ))))) ; theorem :: FUNCSDOM:17 (Bool "for" (Set (Var "x1")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "ex" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set (Var "A")) "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ) "st" (Bool "(" (Bool "(" "for" (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set (Var "x1")))) "implies" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Num 1)) ")" & "(" (Bool (Bool (Set (Var "z")) ($#r1_hidden :::"<>"::: ) (Set (Var "x1")))) "implies" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ")" ) ")" ) & (Bool "(" "for" (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set (Var "x1")))) "implies" (Bool (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" & "(" (Bool (Bool (Set (Var "z")) ($#r1_hidden :::"<>"::: ) (Set (Var "x1")))) "implies" (Bool (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Num 1)) ")" ")" ) ")" ) ")" )))) ; theorem :: FUNCSDOM:18 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set (Var "A")) "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ) "st" (Bool (Bool (Set (Var "x1")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "x2")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "x1")) ($#r1_hidden :::"<>"::: ) (Set (Var "x2"))) & (Bool "(" "for" (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set (Var "x1")))) "implies" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Num 1)) ")" & "(" (Bool (Bool (Set (Var "z")) ($#r1_hidden :::"<>"::: ) (Set (Var "x1")))) "implies" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ")" ) ")" ) & (Bool "(" "for" (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set (Var "x1")))) "implies" (Bool (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" & "(" (Bool (Bool (Set (Var "z")) ($#r1_hidden :::"<>"::: ) (Set (Var "x1")))) "implies" (Bool (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Num 1)) ")" ")" ) ")" )) "holds" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Set "(" ($#k5_funcsdom :::"RealFuncAdd"::: ) (Set (Var "A")) ")" ) ($#k1_funcsdom :::"."::: ) "(" (Set "(" (Set "(" ($#k7_funcsdom :::"RealFuncExtMult"::: ) (Set (Var "A")) ")" ) ($#k2_funcsdom :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "a")) "," (Set (Var "f")) ($#k1_domain_1 :::"]"::: ) ) ")" ) "," (Set "(" (Set "(" ($#k7_funcsdom :::"RealFuncExtMult"::: ) (Set (Var "A")) ")" ) ($#k2_funcsdom :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "b")) "," (Set (Var "g")) ($#k1_domain_1 :::"]"::: ) ) ")" ) ")" ) ($#r2_funct_2 :::"="::: ) (Set ($#k8_funcsdom :::"RealFuncZero"::: ) (Set (Var "A"))))) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ))))) ; theorem :: FUNCSDOM:19 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x1")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "x2")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "x1")) ($#r1_hidden :::"<>"::: ) (Set (Var "x2")))) "holds" (Bool "ex" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set (Var "A")) "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ) "st" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Set "(" ($#k5_funcsdom :::"RealFuncAdd"::: ) (Set (Var "A")) ")" ) ($#k1_funcsdom :::"."::: ) "(" (Set "(" (Set "(" ($#k7_funcsdom :::"RealFuncExtMult"::: ) (Set (Var "A")) ")" ) ($#k2_funcsdom :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "a")) "," (Set (Var "f")) ($#k1_domain_1 :::"]"::: ) ) ")" ) "," (Set "(" (Set "(" ($#k7_funcsdom :::"RealFuncExtMult"::: ) (Set (Var "A")) ")" ) ($#k2_funcsdom :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "b")) "," (Set (Var "g")) ($#k1_domain_1 :::"]"::: ) ) ")" ) ")" ) ($#r2_funct_2 :::"="::: ) (Set ($#k8_funcsdom :::"RealFuncZero"::: ) (Set (Var "A"))))) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ))))) ; theorem :: FUNCSDOM:20 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set (Var "A")) "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k2_tarski :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k2_tarski :::"}"::: ) )) & (Bool (Set (Var "x1")) ($#r1_hidden :::"<>"::: ) (Set (Var "x2"))) & (Bool "(" "for" (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set (Var "x1")))) "implies" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Num 1)) ")" & "(" (Bool (Bool (Set (Var "z")) ($#r1_hidden :::"<>"::: ) (Set (Var "x1")))) "implies" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ")" ) ")" ) & (Bool "(" "for" (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set (Var "x1")))) "implies" (Bool (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" & "(" (Bool (Bool (Set (Var "z")) ($#r1_hidden :::"<>"::: ) (Set (Var "x1")))) "implies" (Bool (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Num 1)) ")" ")" ) ")" )) "holds" (Bool "for" (Set (Var "h")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set (Var "A")) "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ) (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Set (Var "h")) ($#r2_funct_2 :::"="::: ) (Set (Set "(" ($#k5_funcsdom :::"RealFuncAdd"::: ) (Set (Var "A")) ")" ) ($#k1_funcsdom :::"."::: ) "(" (Set "(" (Set "(" ($#k7_funcsdom :::"RealFuncExtMult"::: ) (Set (Var "A")) ")" ) ($#k2_funcsdom :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "a")) "," (Set (Var "f")) ($#k1_domain_1 :::"]"::: ) ) ")" ) "," (Set "(" (Set "(" ($#k7_funcsdom :::"RealFuncExtMult"::: ) (Set (Var "A")) ")" ) ($#k2_funcsdom :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "b")) "," (Set (Var "g")) ($#k1_domain_1 :::"]"::: ) ) ")" ) ")" ))))))) ; theorem :: FUNCSDOM:21 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k2_tarski :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k2_tarski :::"}"::: ) )) & (Bool (Set (Var "x1")) ($#r1_hidden :::"<>"::: ) (Set (Var "x2")))) "holds" (Bool "ex" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set (Var "A")) "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ) "st" (Bool "for" (Set (Var "h")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set (Var "A")) "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ) (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Set (Var "h")) ($#r2_funct_2 :::"="::: ) (Set (Set "(" ($#k5_funcsdom :::"RealFuncAdd"::: ) (Set (Var "A")) ")" ) ($#k1_funcsdom :::"."::: ) "(" (Set "(" (Set "(" ($#k7_funcsdom :::"RealFuncExtMult"::: ) (Set (Var "A")) ")" ) ($#k2_funcsdom :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "a")) "," (Set (Var "f")) ($#k1_domain_1 :::"]"::: ) ) ")" ) "," (Set "(" (Set "(" ($#k7_funcsdom :::"RealFuncExtMult"::: ) (Set (Var "A")) ")" ) ($#k2_funcsdom :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "b")) "," (Set (Var "g")) ($#k1_domain_1 :::"]"::: ) ) ")" ) ")" ))))))) ; theorem :: FUNCSDOM:22 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k2_tarski :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k2_tarski :::"}"::: ) )) & (Bool (Set (Var "x1")) ($#r1_hidden :::"<>"::: ) (Set (Var "x2")))) "holds" (Bool "ex" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set (Var "A")) "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ) "st" (Bool "(" (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Set "(" ($#k5_funcsdom :::"RealFuncAdd"::: ) (Set (Var "A")) ")" ) ($#k1_funcsdom :::"."::: ) "(" (Set "(" (Set "(" ($#k7_funcsdom :::"RealFuncExtMult"::: ) (Set (Var "A")) ")" ) ($#k2_funcsdom :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "a")) "," (Set (Var "f")) ($#k1_domain_1 :::"]"::: ) ) ")" ) "," (Set "(" (Set "(" ($#k7_funcsdom :::"RealFuncExtMult"::: ) (Set (Var "A")) ")" ) ($#k2_funcsdom :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "b")) "," (Set (Var "g")) ($#k1_domain_1 :::"]"::: ) ) ")" ) ")" ) ($#r2_funct_2 :::"="::: ) (Set ($#k8_funcsdom :::"RealFuncZero"::: ) (Set (Var "A"))))) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) ")" ) & (Bool "(" "for" (Set (Var "h")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set (Var "A")) "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ) (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Set (Var "h")) ($#r2_funct_2 :::"="::: ) (Set (Set "(" ($#k5_funcsdom :::"RealFuncAdd"::: ) (Set (Var "A")) ")" ) ($#k1_funcsdom :::"."::: ) "(" (Set "(" (Set "(" ($#k7_funcsdom :::"RealFuncExtMult"::: ) (Set (Var "A")) ")" ) ($#k2_funcsdom :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "a")) "," (Set (Var "f")) ($#k1_domain_1 :::"]"::: ) ) ")" ) "," (Set "(" (Set "(" ($#k7_funcsdom :::"RealFuncExtMult"::: ) (Set (Var "A")) ")" ) ($#k2_funcsdom :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "b")) "," (Set (Var "g")) ($#k1_domain_1 :::"]"::: ) ) ")" ) ")" ))) ")" ) ")" )))) ; definitionlet "A" be ($#m1_hidden :::"set"::: ) ; func :::"RealVectSpace"::: "A" -> ($#v1_rlvect_1 :::"strict"::: ) ($#l1_rlvect_1 :::"RealLinearSpace":::) equals :: FUNCSDOM:def 6 (Set ($#g1_rlvect_1 :::"RLSStruct"::: ) "(#" (Set "(" ($#k9_funct_2 :::"Funcs"::: ) "(" "A" "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ")" ) "," (Set "(" ($#k8_funcsdom :::"RealFuncZero"::: ) "A" ")" ) "," (Set "(" ($#k5_funcsdom :::"RealFuncAdd"::: ) "A" ")" ) "," (Set "(" ($#k7_funcsdom :::"RealFuncExtMult"::: ) "A" ")" ) "#)" ); end; :: deftheorem defines :::"RealVectSpace"::: FUNCSDOM:def 6 : (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k10_funcsdom :::"RealVectSpace"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#g1_rlvect_1 :::"RLSStruct"::: ) "(#" (Set "(" ($#k9_funct_2 :::"Funcs"::: ) "(" (Set (Var "A")) "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ")" ) "," (Set "(" ($#k8_funcsdom :::"RealFuncZero"::: ) (Set (Var "A")) ")" ) "," (Set "(" ($#k5_funcsdom :::"RealFuncAdd"::: ) (Set (Var "A")) ")" ) "," (Set "(" ($#k7_funcsdom :::"RealFuncExtMult"::: ) (Set (Var "A")) ")" ) "#)" ))); theorem :: FUNCSDOM:23 (Bool "ex" (Set (Var "V")) "being" ($#v1_rlvect_1 :::"strict"::: ) ($#l1_rlvect_1 :::"RealLinearSpace":::)(Bool "ex" (Set (Var "u")) "," (Set (Var "v")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "st" (Bool "(" (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Set "(" (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "u")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "v")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "V"))))) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) ")" ) & (Bool "(" "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Set (Var "w")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "u")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "v")) ")" )))) ")" ) ")" ))) ; definitionlet "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; func :::"RRing"::: "A" -> ($#v36_algstr_0 :::"strict"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) equals :: FUNCSDOM:def 7 (Set ($#g6_algstr_0 :::"doubleLoopStr"::: ) "(#" (Set "(" ($#k9_funct_2 :::"Funcs"::: ) "(" "A" "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ")" ) "," (Set "(" ($#k5_funcsdom :::"RealFuncAdd"::: ) "A" ")" ) "," (Set "(" ($#k6_funcsdom :::"RealFuncMult"::: ) "A" ")" ) "," (Set "(" ($#k9_funcsdom :::"RealFuncUnit"::: ) "A" ")" ) "," (Set "(" ($#k8_funcsdom :::"RealFuncZero"::: ) "A" ")" ) "#)" ); end; :: deftheorem defines :::"RRing"::: FUNCSDOM:def 7 : (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k11_funcsdom :::"RRing"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#g6_algstr_0 :::"doubleLoopStr"::: ) "(#" (Set "(" ($#k9_funct_2 :::"Funcs"::: ) "(" (Set (Var "A")) "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ")" ) "," (Set "(" ($#k5_funcsdom :::"RealFuncAdd"::: ) (Set (Var "A")) ")" ) "," (Set "(" ($#k6_funcsdom :::"RealFuncMult"::: ) (Set (Var "A")) ")" ) "," (Set "(" ($#k9_funcsdom :::"RealFuncUnit"::: ) (Set (Var "A")) ")" ) "," (Set "(" ($#k8_funcsdom :::"RealFuncZero"::: ) (Set (Var "A")) ")" ) "#)" ))); registrationlet "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k11_funcsdom :::"RRing"::: ) "A") -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v36_algstr_0 :::"strict"::: ) ; end; registrationlet "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k11_funcsdom :::"RRing"::: ) "A") -> ($#v36_algstr_0 :::"strict"::: ) ($#v1_group_1 :::"unital"::: ) ; end; theorem :: FUNCSDOM:24 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k5_struct_0 :::"1."::: ) (Set "(" ($#k11_funcsdom :::"RRing"::: ) (Set (Var "A")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k9_funcsdom :::"RealFuncUnit"::: ) (Set (Var "A"))))) ; theorem :: FUNCSDOM:25 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k11_funcsdom :::"RRing"::: ) (Set (Var "A")) ")" ) "holds" (Bool "(" (Bool (Set (Set (Var "x")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "y")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "x")))) & (Bool (Set (Set "(" (Set (Var "x")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "y")) ")" ) ($#k1_algstr_0 :::"+"::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k1_algstr_0 :::"+"::: ) (Set "(" (Set (Var "y")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "z")) ")" ))) & (Bool (Set (Set (Var "x")) ($#k1_algstr_0 :::"+"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k11_funcsdom :::"RRing"::: ) (Set (Var "A")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "x"))) & (Bool "ex" (Set (Var "t")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k11_funcsdom :::"RRing"::: ) (Set (Var "A")) ")" ) "st" (Bool (Set (Set (Var "x")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "t"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k11_funcsdom :::"RRing"::: ) (Set (Var "A")) ")" )))) & (Bool (Set (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "y")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "x")))) & (Bool (Set (Set "(" (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y")) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set (Var "y")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "z")) ")" ))) & (Bool (Set (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set "(" ($#k5_struct_0 :::"1."::: ) (Set "(" ($#k11_funcsdom :::"RRing"::: ) (Set (Var "A")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "x"))) & (Bool (Set (Set "(" ($#k5_struct_0 :::"1."::: ) (Set "(" ($#k11_funcsdom :::"RRing"::: ) (Set (Var "A")) ")" ) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Var "x"))) & (Bool (Set (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set (Var "y")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "z")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y")) ")" ) ($#k1_algstr_0 :::"+"::: ) (Set "(" (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "z")) ")" ))) & (Bool (Set (Set "(" (Set (Var "y")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "z")) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "y")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "x")) ")" ) ($#k1_algstr_0 :::"+"::: ) (Set "(" (Set (Var "z")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "x")) ")" ))) ")" ))) ; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v7_struct_0 :::"trivial"::: ) bbbadV8_STRUCT_0() (Num 1) ($#v13_struct_0 :::"-element"::: ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v36_algstr_0 :::"strict"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v1_vectsp_1 :::"right-distributive"::: ) ($#v3_vectsp_1 :::"right_unital"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) for ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; end; definitionmode Ring is ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; end; theorem :: FUNCSDOM:26 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k11_funcsdom :::"RRing"::: ) (Set (Var "A"))) "is" ($#v5_group_1 :::"commutative"::: ) ($#l6_algstr_0 :::"Ring":::))) ; definitionattr "c1" is :::"strict"::: ; struct :::"AlgebraStr"::: -> ($#l6_algstr_0 :::"doubleLoopStr"::: ) "," ($#l1_rlvect_1 :::"RLSStruct"::: ) ; aggr :::"AlgebraStr":::(# :::"carrier":::, :::"multF":::, :::"addF":::, :::"Mult":::, :::"OneF":::, :::"ZeroF"::: #) -> ($#l1_funcsdom :::"AlgebraStr"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) for ($#l1_funcsdom :::"AlgebraStr"::: ) ; end; definitionlet "A" be ($#m1_hidden :::"set"::: ) ; func :::"RAlgebra"::: "A" -> ($#v1_funcsdom :::"strict"::: ) ($#l1_funcsdom :::"AlgebraStr"::: ) equals :: FUNCSDOM:def 8 (Set ($#g1_funcsdom :::"AlgebraStr"::: ) "(#" (Set "(" ($#k9_funct_2 :::"Funcs"::: ) "(" "A" "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ")" ) "," (Set "(" ($#k6_funcsdom :::"RealFuncMult"::: ) "A" ")" ) "," (Set "(" ($#k5_funcsdom :::"RealFuncAdd"::: ) "A" ")" ) "," (Set "(" ($#k7_funcsdom :::"RealFuncExtMult"::: ) "A" ")" ) "," (Set "(" ($#k9_funcsdom :::"RealFuncUnit"::: ) "A" ")" ) "," (Set "(" ($#k8_funcsdom :::"RealFuncZero"::: ) "A" ")" ) "#)" ); end; :: deftheorem defines :::"RAlgebra"::: FUNCSDOM:def 8 : (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k12_funcsdom :::"RAlgebra"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#g1_funcsdom :::"AlgebraStr"::: ) "(#" (Set "(" ($#k9_funct_2 :::"Funcs"::: ) "(" (Set (Var "A")) "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ")" ) "," (Set "(" ($#k6_funcsdom :::"RealFuncMult"::: ) (Set (Var "A")) ")" ) "," (Set "(" ($#k5_funcsdom :::"RealFuncAdd"::: ) (Set (Var "A")) ")" ) "," (Set "(" ($#k7_funcsdom :::"RealFuncExtMult"::: ) (Set (Var "A")) ")" ) "," (Set "(" ($#k9_funcsdom :::"RealFuncUnit"::: ) (Set (Var "A")) ")" ) "," (Set "(" ($#k8_funcsdom :::"RealFuncZero"::: ) (Set (Var "A")) ")" ) "#)" ))); registrationlet "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k12_funcsdom :::"RAlgebra"::: ) "A") -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_funcsdom :::"strict"::: ) ; end; registrationlet "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k12_funcsdom :::"RAlgebra"::: ) "A") -> ($#v1_group_1 :::"unital"::: ) ($#v1_funcsdom :::"strict"::: ) ; end; theorem :: FUNCSDOM:27 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k5_struct_0 :::"1."::: ) (Set "(" ($#k12_funcsdom :::"RAlgebra"::: ) (Set (Var "A")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k9_funcsdom :::"RealFuncUnit"::: ) (Set (Var "A"))))) ; definitionlet "IT" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_funcsdom :::"AlgebraStr"::: ) ; attr "IT" is :::"vector-associative"::: means :: FUNCSDOM:def 9 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool (Set (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "x")) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y")))))); end; :: deftheorem defines :::"vector-associative"::: FUNCSDOM:def 9 : (Bool "for" (Set (Var "IT")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_funcsdom :::"AlgebraStr"::: ) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v2_funcsdom :::"vector-associative"::: ) ) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool (Set (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "x")) ")" ) ($#k6_algstr_0 :::"*"::: ) (Set (Var "y")))))) ")" )); registrationlet "A" be ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k12_funcsdom :::"RAlgebra"::: ) "A") -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_funcsdom :::"strict"::: ) ; end; registrationlet "A" be ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k12_funcsdom :::"RAlgebra"::: ) "A") -> ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v1_vectsp_1 :::"right-distributive"::: ) ($#v3_vectsp_1 :::"right_unital"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v5_rlvect_1 :::"vector-distributive"::: ) ($#v6_rlvect_1 :::"scalar-distributive"::: ) ($#v7_rlvect_1 :::"scalar-associative"::: ) ($#v1_funcsdom :::"strict"::: ) ($#v2_funcsdom :::"vector-associative"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v1_vectsp_1 :::"right-distributive"::: ) ($#v3_vectsp_1 :::"right_unital"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v5_rlvect_1 :::"vector-distributive"::: ) ($#v6_rlvect_1 :::"scalar-distributive"::: ) ($#v7_rlvect_1 :::"scalar-associative"::: ) ($#v1_funcsdom :::"strict"::: ) ($#v2_funcsdom :::"vector-associative"::: ) for ($#l1_funcsdom :::"AlgebraStr"::: ) ; end; definitionmode Algebra is ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v1_vectsp_1 :::"right-distributive"::: ) ($#v3_vectsp_1 :::"right_unital"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v5_rlvect_1 :::"vector-distributive"::: ) ($#v6_rlvect_1 :::"scalar-distributive"::: ) ($#v7_rlvect_1 :::"scalar-associative"::: ) ($#v2_funcsdom :::"vector-associative"::: ) ($#l1_funcsdom :::"AlgebraStr"::: ) ; end;