:: QUATERNI semantic presentation begin definitionfunc :::"QUATERNION"::: -> ($#m1_hidden :::"set"::: ) equals :: QUATERNI:def 1 (Set (Set "(" (Set "(" ($#k9_funct_2 :::"Funcs"::: ) "(" (Num 4) "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ")" ) ($#k6_subset_1 :::"\"::: ) "{" (Set (Var "x")) where x "is" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Num 4) "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ) : (Bool "(" (Bool (Set (Set (Var "x")) ($#k1_seq_1 :::"."::: ) (Num 2)) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set (Var "x")) ($#k1_seq_1 :::"."::: ) (Num 3)) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) "}" ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k2_numbers :::"COMPLEX"::: ) )); end; :: deftheorem defines :::"QUATERNION"::: QUATERNI:def 1 : (Bool (Set ($#k1_quaterni :::"QUATERNION"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k9_funct_2 :::"Funcs"::: ) "(" (Num 4) "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ")" ) ($#k6_subset_1 :::"\"::: ) "{" (Set (Var "x")) where x "is" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Num 4) "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ) : (Bool "(" (Bool (Set (Set (Var "x")) ($#k1_seq_1 :::"."::: ) (Num 2)) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set (Var "x")) ($#k1_seq_1 :::"."::: ) (Num 3)) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) "}" ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k2_numbers :::"COMPLEX"::: ) ))); definitionlet "x" be ($#m1_hidden :::"number"::: ) ; attr "x" is :::"quaternion"::: means :: QUATERNI:def 2 (Bool "x" ($#r2_hidden :::"in"::: ) (Set ($#k1_quaterni :::"QUATERNION"::: ) )); end; :: deftheorem defines :::"quaternion"::: QUATERNI:def 2 : (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) "is" ($#v1_quaterni :::"quaternion"::: ) ) "iff" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_quaterni :::"QUATERNION"::: ) )) ")" )); registration cluster (Set ($#k1_quaterni :::"QUATERNION"::: ) ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; definitionlet "x", "y", "w", "z", "a", "b", "c", "d" be ($#m1_hidden :::"set"::: ) ; func "(" "x" "," "y" "," "w" "," "z" ")" :::"-->"::: "(" "a" "," "b" "," "c" "," "d" ")" -> ($#m1_hidden :::"set"::: ) equals :: QUATERNI:def 3 (Set (Set "(" "(" "x" "," "y" ")" ($#k4_funct_4 :::"-->"::: ) "(" "a" "," "b" ")" ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" "(" "w" "," "z" ")" ($#k4_funct_4 :::"-->"::: ) "(" "c" "," "d" ")" ")" )); end; :: deftheorem defines :::"-->"::: QUATERNI:def 3 : (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "w")) "," (Set (Var "z")) "," (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "w")) "," (Set (Var "z")) ")" ($#k2_quaterni :::"-->"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" "(" (Set (Var "x")) "," (Set (Var "y")) ")" ($#k4_funct_4 :::"-->"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" "(" (Set (Var "w")) "," (Set (Var "z")) ")" ($#k4_funct_4 :::"-->"::: ) "(" (Set (Var "c")) "," (Set (Var "d")) ")" ")" )))); registrationlet "x", "y", "w", "z", "a", "b", "c", "d" be ($#m1_hidden :::"set"::: ) ; cluster (Set "(" "x" "," "y" "," "w" "," "z" ")" ($#k2_quaterni :::"-->"::: ) "(" "a" "," "b" "," "c" "," "d" ")" ) -> ($#v1_relat_1 :::"Relation-like"::: ) ($#v1_funct_1 :::"Function-like"::: ) ; end; theorem :: QUATERNI:1 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "w")) "," (Set (Var "z")) "," (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "w")) "," (Set (Var "z")) ")" ($#k2_quaterni :::"-->"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_enumset1 :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "w")) "," (Set (Var "z")) ($#k2_enumset1 :::"}"::: ) ))) ; theorem :: QUATERNI:2 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "w")) "," (Set (Var "z")) "," (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "w")) "," (Set (Var "z")) ")" ($#k2_quaterni :::"-->"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) ")" ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k2_enumset1 :::"{"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) ($#k2_enumset1 :::"}"::: ) ))) ; theorem :: QUATERNI:3 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "w")) "," (Set (Var "z")) "," (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "w")) "," (Set (Var "z")) ($#r2_zfmisc_1 :::"are_mutually_different"::: ) )) "holds" (Bool "(" (Bool (Set (Set "(" "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "w")) "," (Set (Var "z")) ")" ($#k2_quaterni :::"-->"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Var "a"))) & (Bool (Set (Set "(" "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "w")) "," (Set (Var "z")) ")" ($#k2_quaterni :::"-->"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Var "b"))) & (Bool (Set (Set "(" "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "w")) "," (Set (Var "z")) ")" ($#k2_quaterni :::"-->"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "w"))) ($#r1_hidden :::"="::: ) (Set (Var "c"))) & (Bool (Set (Set "(" "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "w")) "," (Set (Var "z")) ")" ($#k2_quaterni :::"-->"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set (Var "d"))) ")" )) ; theorem :: QUATERNI:4 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "w")) "," (Set (Var "z")) "," (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "w")) "," (Set (Var "z")) ($#r2_zfmisc_1 :::"are_mutually_different"::: ) )) "holds" (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "w")) "," (Set (Var "z")) ")" ($#k2_quaterni :::"-->"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_enumset1 :::"{"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) ($#k2_enumset1 :::"}"::: ) ))) ; theorem :: QUATERNI:5 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set ($#k2_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) ($#k2_enumset1 :::"}"::: ) ) ($#r1_tarski :::"c="::: ) (Set (Var "X"))) "iff" (Bool "(" (Bool (Set (Var "x1")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "x2")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "x3")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "x4")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) ")" ) ")" )) ; definitionlet "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "x", "y", "w", "z" be ($#m1_hidden :::"set"::: ) ; let "a", "b", "c", "d" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "A")); :: original: :::"-->"::: redefine func "(" "x" "," "y" "," "w" "," "z" ")" :::"-->"::: "(" "a" "," "b" "," "c" "," "d" ")" -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_enumset1 :::"{"::: ) "x" "," "y" "," "w" "," "z" ($#k2_enumset1 :::"}"::: ) ) "," "A"; end; definitionfunc :::""::: -> ($#m1_hidden :::"set"::: ) equals :: QUATERNI:def 4 (Set "(" (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) "," (Num 2) "," (Num 3) ")" ($#k3_quaterni :::"-->"::: ) "(" (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ); func :::""::: -> ($#m1_hidden :::"set"::: ) equals :: QUATERNI:def 5 (Set "(" (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) "," (Num 2) "," (Num 3) ")" ($#k3_quaterni :::"-->"::: ) "(" (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ")" ); end; :: deftheorem defines :::""::: QUATERNI:def 4 : (Bool (Set ($#k4_quaterni :::""::: ) ) ($#r1_hidden :::"="::: ) (Set "(" (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) "," (Num 2) "," (Num 3) ")" ($#k3_quaterni :::"-->"::: ) "(" (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ")" )); :: deftheorem defines :::""::: QUATERNI:def 5 : (Bool (Set ($#k5_quaterni :::""::: ) ) ($#r1_hidden :::"="::: ) (Set "(" (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) "," (Num 2) "," (Num 3) ")" ($#k3_quaterni :::"-->"::: ) "(" (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ")" )); registration cluster (Set ($#k1_xcmplx_0 :::""::: ) ) -> ($#v1_quaterni :::"quaternion"::: ) ; cluster (Set ($#k4_quaterni :::""::: ) ) -> ($#v1_quaterni :::"quaternion"::: ) ; cluster (Set ($#k5_quaterni :::""::: ) ) -> ($#v1_quaterni :::"quaternion"::: ) ; end; registration cluster ($#v1_quaterni :::"quaternion"::: ) for ($#m1_hidden :::"set"::: ) ; end; registration cluster -> ($#v1_quaterni :::"quaternion"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_quaterni :::"QUATERNION"::: ) ); end; definitionlet "x", "y", "w", "z" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; func :::"[*":::"x" "," "y" "," "w" "," "z":::"*]"::: -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_quaterni :::"QUATERNION"::: ) ) means :: QUATERNI:def 6 (Bool "ex" (Set (Var "x9")) "," (Set (Var "y9")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool "(" (Bool (Set (Var "x9")) ($#r1_hidden :::"="::: ) "x") & (Bool (Set (Var "y9")) ($#r1_hidden :::"="::: ) "y") & (Bool it ($#r1_hidden :::"="::: ) (Set ($#k5_arytm_0 :::"[*"::: ) (Set (Var "x9")) "," (Set (Var "y9")) ($#k5_arytm_0 :::"*]"::: ) )) ")" )) if (Bool "(" (Bool "w" ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool "z" ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) otherwise (Bool it ($#r1_hidden :::"="::: ) (Set "(" (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) "," (Num 2) "," (Num 3) ")" ($#k2_quaterni :::"-->"::: ) "(" "x" "," "y" "," "w" "," "z" ")" )); end; :: deftheorem defines :::"[*"::: QUATERNI:def 6 : (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "w")) "," (Set (Var "z")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "b5")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_quaterni :::"QUATERNION"::: ) ) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "w")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set ($#k6_quaterni :::"[*"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "w")) "," (Set (Var "z")) ($#k6_quaterni :::"*]"::: ) )) "iff" (Bool "ex" (Set (Var "x9")) "," (Set (Var "y9")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool "(" (Bool (Set (Var "x9")) ($#r1_hidden :::"="::: ) (Set (Var "x"))) & (Bool (Set (Var "y9")) ($#r1_hidden :::"="::: ) (Set (Var "y"))) & (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set ($#k5_arytm_0 :::"[*"::: ) (Set (Var "x9")) "," (Set (Var "y9")) ($#k5_arytm_0 :::"*]"::: ) )) ")" )) ")" ) ")" & "(" (Bool (Bool "(" "not" (Bool (Set (Var "w")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) "or" "not" (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )) "implies" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set ($#k6_quaterni :::"[*"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "w")) "," (Set (Var "z")) ($#k6_quaterni :::"*]"::: ) )) "iff" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set "(" (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) "," (Num 2) "," (Num 3) ")" ($#k2_quaterni :::"-->"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "w")) "," (Set (Var "z")) ")" )) ")" ) ")" ")" ))); theorem :: QUATERNI:6 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "e")) "," (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "k")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b"))) & (Bool (Set (Var "c")) ($#r1_hidden :::"<>"::: ) (Set (Var "d"))) & (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set ($#k2_enumset1 :::"{"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) ($#k2_enumset1 :::"}"::: ) )) & (Bool (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Var "e"))) & (Bool (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Var "i"))) & (Bool (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Var "j"))) & (Bool (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "d"))) ($#r1_hidden :::"="::: ) (Set (Var "k")))) "holds" (Bool (Set (Var "g")) ($#r1_hidden :::"="::: ) (Set "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) ")" ($#k2_quaterni :::"-->"::: ) "(" (Set (Var "e")) "," (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "k")) ")" )))) ; theorem :: QUATERNI:7 (Bool "for" (Set (Var "g")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) (Bool "ex" (Set (Var "r")) "," (Set (Var "s")) "," (Set (Var "t")) "," (Set (Var "u")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Set (Var "g")) ($#r1_hidden :::"="::: ) (Set ($#k6_quaterni :::"[*"::: ) (Set (Var "r")) "," (Set (Var "s")) "," (Set (Var "t")) "," (Set (Var "u")) ($#k6_quaterni :::"*]"::: ) )))) ; theorem :: QUATERNI:8 (Bool "for" (Set (Var "a")) "," (Set (Var "c")) "," (Set (Var "x")) "," (Set (Var "w")) "," (Set (Var "b")) "," (Set (Var "d")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "c")) "," (Set (Var "x")) "," (Set (Var "w")) ($#r2_zfmisc_1 :::"are_mutually_different"::: ) )) "holds" (Bool (Set "(" (Set (Var "a")) "," (Set (Var "c")) "," (Set (Var "x")) "," (Set (Var "w")) ")" ($#k2_quaterni :::"-->"::: ) "(" (Set (Var "b")) "," (Set (Var "d")) "," (Set (Var "y")) "," (Set (Var "z")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k2_enumset1 :::"{"::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set (Var "c")) "," (Set (Var "d")) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set (Var "w")) "," (Set (Var "z")) ($#k4_tarski :::"]"::: ) ) ($#k2_enumset1 :::"}"::: ) ))) ; theorem :: QUATERNI:9 (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k5_arytm_3 :::"RAT+"::: ) ) "st" (Bool (Bool "ex" (Set (Var "t")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_arytm_3 :::"RAT+"::: ) ) "st" (Bool "(" (Bool (Set (Var "t")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "t")) ($#r1_hidden :::"<>"::: ) (Set ($#k11_arytm_3 :::"{}"::: ) )) ")" )) & (Bool "(" "for" (Set (Var "r")) "," (Set (Var "s")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_arytm_3 :::"RAT+"::: ) ) "st" (Bool (Bool (Set (Var "r")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "s")) ($#r3_arytm_3 :::"<='"::: ) (Set (Var "r")))) "holds" (Bool (Set (Var "s")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) ")" )) "holds" (Bool "ex" (Set (Var "r1")) "," (Set (Var "r2")) "," (Set (Var "r3")) "," (Set (Var "r4")) "," (Set (Var "r5")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_arytm_3 :::"RAT+"::: ) ) "st" (Bool "(" (Bool (Set (Var "r1")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "r2")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "r3")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "r4")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "r5")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "r1")) ($#r1_hidden :::"<>"::: ) (Set (Var "r2"))) & (Bool (Set (Var "r1")) ($#r1_hidden :::"<>"::: ) (Set (Var "r3"))) & (Bool (Set (Var "r1")) ($#r1_hidden :::"<>"::: ) (Set (Var "r4"))) & (Bool (Set (Var "r1")) ($#r1_hidden :::"<>"::: ) (Set (Var "r5"))) & (Bool (Set (Var "r2")) ($#r1_hidden :::"<>"::: ) (Set (Var "r3"))) & (Bool (Set (Var "r2")) ($#r1_hidden :::"<>"::: ) (Set (Var "r4"))) & (Bool (Set (Var "r2")) ($#r1_hidden :::"<>"::: ) (Set (Var "r5"))) & (Bool (Set (Var "r3")) ($#r1_hidden :::"<>"::: ) (Set (Var "r4"))) & (Bool (Set (Var "r3")) ($#r1_hidden :::"<>"::: ) (Set (Var "r5"))) & (Bool (Set (Var "r4")) ($#r1_hidden :::"<>"::: ) (Set (Var "r5"))) ")" ))) ; theorem :: QUATERNI:10 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Bool "not" (Set "(" (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) "," (Num 2) "," (Num 3) ")" ($#k3_quaterni :::"-->"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k2_numbers :::"COMPLEX"::: ) )))) ; theorem :: QUATERNI:11 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "w")) "," (Set (Var "x9")) "," (Set (Var "y9")) "," (Set (Var "z9")) "," (Set (Var "w9")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) ($#r2_zfmisc_1 :::"are_mutually_different"::: ) ) & (Bool (Set "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) ")" ($#k2_quaterni :::"-->"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "w")) ")" ) ($#r1_hidden :::"="::: ) (Set "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) ")" ($#k2_quaterni :::"-->"::: ) "(" (Set (Var "x9")) "," (Set (Var "y9")) "," (Set (Var "z9")) "," (Set (Var "w9")) ")" ))) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "x9"))) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Var "y9"))) & (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set (Var "z9"))) & (Bool (Set (Var "w")) ($#r1_hidden :::"="::: ) (Set (Var "w9"))) ")" )) ; theorem :: QUATERNI:12 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "y1")) "," (Set (Var "y2")) "," (Set (Var "y3")) "," (Set (Var "y4")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set ($#k6_quaterni :::"[*"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) ($#k6_quaterni :::"*]"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_quaterni :::"[*"::: ) (Set (Var "y1")) "," (Set (Var "y2")) "," (Set (Var "y3")) "," (Set (Var "y4")) ($#k6_quaterni :::"*]"::: ) ))) "holds" (Bool "(" (Bool (Set (Var "x1")) ($#r1_hidden :::"="::: ) (Set (Var "y1"))) & (Bool (Set (Var "x2")) ($#r1_hidden :::"="::: ) (Set (Var "y2"))) & (Bool (Set (Var "x3")) ($#r1_hidden :::"="::: ) (Set (Var "y3"))) & (Bool (Set (Var "x4")) ($#r1_hidden :::"="::: ) (Set (Var "y4"))) ")" )) ; definitionlet "x", "y" be ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) ; func "x" :::"+"::: "y" -> ($#m1_hidden :::"set"::: ) means :: QUATERNI:def 7 (Bool "ex" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "y1")) "," (Set (Var "y2")) "," (Set (Var "y3")) "," (Set (Var "y4")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool "(" (Bool "x" ($#r1_hidden :::"="::: ) (Set ($#k6_quaterni :::"[*"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) ($#k6_quaterni :::"*]"::: ) )) & (Bool "y" ($#r1_hidden :::"="::: ) (Set ($#k6_quaterni :::"[*"::: ) (Set (Var "y1")) "," (Set (Var "y2")) "," (Set (Var "y3")) "," (Set (Var "y4")) ($#k6_quaterni :::"*]"::: ) )) & (Bool it ($#r1_hidden :::"="::: ) (Set ($#k6_quaterni :::"[*"::: ) (Set "(" (Set (Var "x1")) ($#k7_real_1 :::"+"::: ) (Set (Var "y1")) ")" ) "," (Set "(" (Set (Var "x2")) ($#k7_real_1 :::"+"::: ) (Set (Var "y2")) ")" ) "," (Set "(" (Set (Var "x3")) ($#k7_real_1 :::"+"::: ) (Set (Var "y3")) ")" ) "," (Set "(" (Set (Var "x4")) ($#k7_real_1 :::"+"::: ) (Set (Var "y4")) ")" ) ($#k6_quaterni :::"*]"::: ) )) ")" )); commutativity (Bool "for" (Set (Var "b1")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool "ex" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "y1")) "," (Set (Var "y2")) "," (Set (Var "y3")) "," (Set (Var "y4")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k6_quaterni :::"[*"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) ($#k6_quaterni :::"*]"::: ) )) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set ($#k6_quaterni :::"[*"::: ) (Set (Var "y1")) "," (Set (Var "y2")) "," (Set (Var "y3")) "," (Set (Var "y4")) ($#k6_quaterni :::"*]"::: ) )) & (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k6_quaterni :::"[*"::: ) (Set "(" (Set (Var "x1")) ($#k7_real_1 :::"+"::: ) (Set (Var "y1")) ")" ) "," (Set "(" (Set (Var "x2")) ($#k7_real_1 :::"+"::: ) (Set (Var "y2")) ")" ) "," (Set "(" (Set (Var "x3")) ($#k7_real_1 :::"+"::: ) (Set (Var "y3")) ")" ) "," (Set "(" (Set (Var "x4")) ($#k7_real_1 :::"+"::: ) (Set (Var "y4")) ")" ) ($#k6_quaterni :::"*]"::: ) )) ")" ))) "holds" (Bool "ex" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "y1")) "," (Set (Var "y2")) "," (Set (Var "y3")) "," (Set (Var "y4")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool "(" (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set ($#k6_quaterni :::"[*"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) ($#k6_quaterni :::"*]"::: ) )) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k6_quaterni :::"[*"::: ) (Set (Var "y1")) "," (Set (Var "y2")) "," (Set (Var "y3")) "," (Set (Var "y4")) ($#k6_quaterni :::"*]"::: ) )) & (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k6_quaterni :::"[*"::: ) (Set "(" (Set (Var "x1")) ($#k7_real_1 :::"+"::: ) (Set (Var "y1")) ")" ) "," (Set "(" (Set (Var "x2")) ($#k7_real_1 :::"+"::: ) (Set (Var "y2")) ")" ) "," (Set "(" (Set (Var "x3")) ($#k7_real_1 :::"+"::: ) (Set (Var "y3")) ")" ) "," (Set "(" (Set (Var "x4")) ($#k7_real_1 :::"+"::: ) (Set (Var "y4")) ")" ) ($#k6_quaterni :::"*]"::: ) )) ")" )))) ; end; :: deftheorem defines :::"+"::: QUATERNI:def 7 : (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "b3")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k7_quaterni :::"+"::: ) (Set (Var "y")))) "iff" (Bool "ex" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "y1")) "," (Set (Var "y2")) "," (Set (Var "y3")) "," (Set (Var "y4")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k6_quaterni :::"[*"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) ($#k6_quaterni :::"*]"::: ) )) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set ($#k6_quaterni :::"[*"::: ) (Set (Var "y1")) "," (Set (Var "y2")) "," (Set (Var "y3")) "," (Set (Var "y4")) ($#k6_quaterni :::"*]"::: ) )) & (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k6_quaterni :::"[*"::: ) (Set "(" (Set (Var "x1")) ($#k7_real_1 :::"+"::: ) (Set (Var "y1")) ")" ) "," (Set "(" (Set (Var "x2")) ($#k7_real_1 :::"+"::: ) (Set (Var "y2")) ")" ) "," (Set "(" (Set (Var "x3")) ($#k7_real_1 :::"+"::: ) (Set (Var "y3")) ")" ) "," (Set "(" (Set (Var "x4")) ($#k7_real_1 :::"+"::: ) (Set (Var "y4")) ")" ) ($#k6_quaterni :::"*]"::: ) )) ")" )) ")" ))); definitionlet "z" be ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) ; func :::"-"::: "z" -> ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) means :: QUATERNI:def 8 (Bool (Set "z" ($#k7_quaterni :::"+"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )); involutiveness (Bool "for" (Set (Var "b1")) "," (Set (Var "b2")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Set (Var "b2")) ($#k7_quaterni :::"+"::: ) (Set (Var "b1"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set (Var "b1")) ($#k7_quaterni :::"+"::: ) (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) ; end; :: deftheorem defines :::"-"::: QUATERNI:def 8 : (Bool "for" (Set (Var "z")) "," (Set (Var "b2")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k8_quaterni :::"-"::: ) (Set (Var "z")))) "iff" (Bool (Set (Set (Var "z")) ($#k7_quaterni :::"+"::: ) (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )); definitionlet "x", "y" be ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) ; func "x" :::"-"::: "y" -> ($#m1_hidden :::"set"::: ) equals :: QUATERNI:def 9 (Set "x" ($#k7_quaterni :::"+"::: ) (Set "(" ($#k8_quaterni :::"-"::: ) "y" ")" )); end; :: deftheorem defines :::"-"::: QUATERNI:def 9 : (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "x")) ($#k9_quaterni :::"-"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k7_quaterni :::"+"::: ) (Set "(" ($#k8_quaterni :::"-"::: ) (Set (Var "y")) ")" )))); definitionlet "x", "y" be ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) ; func "x" :::"*"::: "y" -> ($#m1_hidden :::"set"::: ) means :: QUATERNI:def 10 (Bool "ex" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "y1")) "," (Set (Var "y2")) "," (Set (Var "y3")) "," (Set (Var "y4")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool "(" (Bool "x" ($#r1_hidden :::"="::: ) (Set ($#k6_quaterni :::"[*"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) ($#k6_quaterni :::"*]"::: ) )) & (Bool "y" ($#r1_hidden :::"="::: ) (Set ($#k6_quaterni :::"[*"::: ) (Set (Var "y1")) "," (Set (Var "y2")) "," (Set (Var "y3")) "," (Set (Var "y4")) ($#k6_quaterni :::"*]"::: ) )) & (Bool it ($#r1_hidden :::"="::: ) (Set ($#k6_quaterni :::"[*"::: ) (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "x1")) ($#k8_real_1 :::"*"::: ) (Set (Var "y1")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "x2")) ($#k8_real_1 :::"*"::: ) (Set (Var "y2")) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "x3")) ($#k8_real_1 :::"*"::: ) (Set (Var "y3")) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "x4")) ($#k8_real_1 :::"*"::: ) (Set (Var "y4")) ")" ) ")" ) "," (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "x1")) ($#k8_real_1 :::"*"::: ) (Set (Var "y2")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "x2")) ($#k8_real_1 :::"*"::: ) (Set (Var "y1")) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "x3")) ($#k8_real_1 :::"*"::: ) (Set (Var "y4")) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "x4")) ($#k8_real_1 :::"*"::: ) (Set (Var "y3")) ")" ) ")" ) "," (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "x1")) ($#k8_real_1 :::"*"::: ) (Set (Var "y3")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "y1")) ($#k8_real_1 :::"*"::: ) (Set (Var "x3")) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "y2")) ($#k8_real_1 :::"*"::: ) (Set (Var "x4")) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "y4")) ($#k8_real_1 :::"*"::: ) (Set (Var "x2")) ")" ) ")" ) "," (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "x1")) ($#k8_real_1 :::"*"::: ) (Set (Var "y4")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "x4")) ($#k8_real_1 :::"*"::: ) (Set (Var "y1")) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "x2")) ($#k8_real_1 :::"*"::: ) (Set (Var "y3")) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "x3")) ($#k8_real_1 :::"*"::: ) (Set (Var "y2")) ")" ) ")" ) ($#k6_quaterni :::"*]"::: ) )) ")" )); end; :: deftheorem defines :::"*"::: QUATERNI:def 10 : (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "b3")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k10_quaterni :::"*"::: ) (Set (Var "y")))) "iff" (Bool "ex" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "y1")) "," (Set (Var "y2")) "," (Set (Var "y3")) "," (Set (Var "y4")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k6_quaterni :::"[*"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) ($#k6_quaterni :::"*]"::: ) )) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set ($#k6_quaterni :::"[*"::: ) (Set (Var "y1")) "," (Set (Var "y2")) "," (Set (Var "y3")) "," (Set (Var "y4")) ($#k6_quaterni :::"*]"::: ) )) & (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k6_quaterni :::"[*"::: ) (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "x1")) ($#k8_real_1 :::"*"::: ) (Set (Var "y1")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "x2")) ($#k8_real_1 :::"*"::: ) (Set (Var "y2")) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "x3")) ($#k8_real_1 :::"*"::: ) (Set (Var "y3")) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "x4")) ($#k8_real_1 :::"*"::: ) (Set (Var "y4")) ")" ) ")" ) "," (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "x1")) ($#k8_real_1 :::"*"::: ) (Set (Var "y2")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "x2")) ($#k8_real_1 :::"*"::: ) (Set (Var "y1")) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "x3")) ($#k8_real_1 :::"*"::: ) (Set (Var "y4")) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "x4")) ($#k8_real_1 :::"*"::: ) (Set (Var "y3")) ")" ) ")" ) "," (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "x1")) ($#k8_real_1 :::"*"::: ) (Set (Var "y3")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "y1")) ($#k8_real_1 :::"*"::: ) (Set (Var "x3")) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "y2")) ($#k8_real_1 :::"*"::: ) (Set (Var "x4")) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "y4")) ($#k8_real_1 :::"*"::: ) (Set (Var "x2")) ")" ) ")" ) "," (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "x1")) ($#k8_real_1 :::"*"::: ) (Set (Var "y4")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "x4")) ($#k8_real_1 :::"*"::: ) (Set (Var "y1")) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "x2")) ($#k8_real_1 :::"*"::: ) (Set (Var "y3")) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "x3")) ($#k8_real_1 :::"*"::: ) (Set (Var "y2")) ")" ) ")" ) ($#k6_quaterni :::"*]"::: ) )) ")" )) ")" ))); registrationlet "z", "z9" be ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set "z" ($#k7_quaterni :::"+"::: ) "z9") -> ($#v1_quaterni :::"quaternion"::: ) ; cluster (Set "z" ($#k10_quaterni :::"*"::: ) "z9") -> ($#v1_quaterni :::"quaternion"::: ) ; end; definition:: original: :::""::: redefine func :::""::: -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_quaterni :::"QUATERNION"::: ) ) equals :: QUATERNI:def 11 (Set ($#k6_quaterni :::"[*"::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k6_quaterni :::"*]"::: ) ); :: original: :::""::: redefine func :::""::: -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_quaterni :::"QUATERNION"::: ) ) equals :: QUATERNI:def 12 (Set ($#k6_quaterni :::"[*"::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k6_quaterni :::"*]"::: ) ); end; :: deftheorem defines :::""::: QUATERNI:def 11 : (Bool (Set ($#k11_quaterni :::""::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_quaterni :::"[*"::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k6_quaterni :::"*]"::: ) )); :: deftheorem defines :::""::: QUATERNI:def 12 : (Bool (Set ($#k12_quaterni :::""::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_quaterni :::"[*"::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k6_quaterni :::"*]"::: ) )); theorem :: QUATERNI:13 (Bool (Set (Set ($#k1_xcmplx_0 :::""::: ) ) ($#k10_quaterni :::"*"::: ) (Set ($#k1_xcmplx_0 :::""::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Num 1))) ; theorem :: QUATERNI:14 (Bool (Set (Set ($#k11_quaterni :::""::: ) ) ($#k10_quaterni :::"*"::: ) (Set ($#k11_quaterni :::""::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Num 1))) ; theorem :: QUATERNI:15 (Bool (Set (Set ($#k12_quaterni :::""::: ) ) ($#k10_quaterni :::"*"::: ) (Set ($#k12_quaterni :::""::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Num 1))) ; theorem :: QUATERNI:16 (Bool (Set (Set ($#k1_xcmplx_0 :::""::: ) ) ($#k10_quaterni :::"*"::: ) (Set ($#k11_quaterni :::""::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k12_quaterni :::""::: ) )) ; theorem :: QUATERNI:17 (Bool (Set (Set ($#k11_quaterni :::""::: ) ) ($#k10_quaterni :::"*"::: ) (Set ($#k12_quaterni :::""::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_xcmplx_0 :::""::: ) )) ; theorem :: QUATERNI:18 (Bool (Set (Set ($#k12_quaterni :::""::: ) ) ($#k10_quaterni :::"*"::: ) (Set ($#k1_xcmplx_0 :::""::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k11_quaterni :::""::: ) )) ; theorem :: QUATERNI:19 (Bool (Set (Set ($#k1_xcmplx_0 :::""::: ) ) ($#k10_quaterni :::"*"::: ) (Set ($#k11_quaterni :::""::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k8_quaterni :::"-"::: ) (Set "(" (Set ($#k11_quaterni :::""::: ) ) ($#k10_quaterni :::"*"::: ) (Set ($#k1_xcmplx_0 :::""::: ) ) ")" ))) ; theorem :: QUATERNI:20 (Bool (Set (Set ($#k11_quaterni :::""::: ) ) ($#k10_quaterni :::"*"::: ) (Set ($#k12_quaterni :::""::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k8_quaterni :::"-"::: ) (Set "(" (Set ($#k12_quaterni :::""::: ) ) ($#k10_quaterni :::"*"::: ) (Set ($#k11_quaterni :::""::: ) ) ")" ))) ; theorem :: QUATERNI:21 (Bool (Set (Set ($#k12_quaterni :::""::: ) ) ($#k10_quaterni :::"*"::: ) (Set ($#k1_xcmplx_0 :::""::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k8_quaterni :::"-"::: ) (Set "(" (Set ($#k1_xcmplx_0 :::""::: ) ) ($#k10_quaterni :::"*"::: ) (Set ($#k12_quaterni :::""::: ) ) ")" ))) ; definitionlet "z" be ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) ; func :::"Rea"::: "z" -> ($#m1_hidden :::"set"::: ) means :: QUATERNI:def 13 (Bool "ex" (Set (Var "z9")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool "(" (Bool "z" ($#r1_hidden :::"="::: ) (Set (Var "z9"))) & (Bool it ($#r1_hidden :::"="::: ) (Set ($#k3_complex1 :::"Re"::: ) (Set (Var "z9")))) ")" )) if (Bool "z" ($#r2_hidden :::"in"::: ) (Set ($#k2_numbers :::"COMPLEX"::: ) )) otherwise (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Num 4) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool "(" (Bool "z" ($#r1_hidden :::"="::: ) (Set (Var "f"))) & (Bool it ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ))) ")" )); func :::"Im1"::: "z" -> ($#m1_hidden :::"set"::: ) means :: QUATERNI:def 14 (Bool "ex" (Set (Var "z9")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool "(" (Bool "z" ($#r1_hidden :::"="::: ) (Set (Var "z9"))) & (Bool it ($#r1_hidden :::"="::: ) (Set ($#k4_complex1 :::"Im"::: ) (Set (Var "z9")))) ")" )) if (Bool "z" ($#r2_hidden :::"in"::: ) (Set ($#k2_numbers :::"COMPLEX"::: ) )) otherwise (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Num 4) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool "(" (Bool "z" ($#r1_hidden :::"="::: ) (Set (Var "f"))) & (Bool it ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Num 1))) ")" )); func :::"Im2"::: "z" -> ($#m1_hidden :::"set"::: ) means :: QUATERNI:def 15 (Bool it ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) if (Bool "z" ($#r2_hidden :::"in"::: ) (Set ($#k2_numbers :::"COMPLEX"::: ) )) otherwise (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Num 4) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool "(" (Bool "z" ($#r1_hidden :::"="::: ) (Set (Var "f"))) & (Bool it ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Num 2))) ")" )); func :::"Im3"::: "z" -> ($#m1_hidden :::"set"::: ) means :: QUATERNI:def 16 (Bool it ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) if (Bool "z" ($#r2_hidden :::"in"::: ) (Set ($#k2_numbers :::"COMPLEX"::: ) )) otherwise (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Num 4) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool "(" (Bool "z" ($#r1_hidden :::"="::: ) (Set (Var "f"))) & (Bool it ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Num 3))) ")" )); end; :: deftheorem defines :::"Rea"::: QUATERNI:def 13 : (Bool "for" (Set (Var "z")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "b2")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set ($#k2_numbers :::"COMPLEX"::: ) ))) "implies" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k13_quaterni :::"Rea"::: ) (Set (Var "z")))) "iff" (Bool "ex" (Set (Var "z9")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool "(" (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set (Var "z9"))) & (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k3_complex1 :::"Re"::: ) (Set (Var "z9")))) ")" )) ")" ) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set ($#k2_numbers :::"COMPLEX"::: ) )))) "implies" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k13_quaterni :::"Rea"::: ) (Set (Var "z")))) "iff" (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Num 4) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool "(" (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set (Var "f"))) & (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ))) ")" )) ")" ) ")" ")" ))); :: deftheorem defines :::"Im1"::: QUATERNI:def 14 : (Bool "for" (Set (Var "z")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "b2")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set ($#k2_numbers :::"COMPLEX"::: ) ))) "implies" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k14_quaterni :::"Im1"::: ) (Set (Var "z")))) "iff" (Bool "ex" (Set (Var "z9")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool "(" (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set (Var "z9"))) & (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k4_complex1 :::"Im"::: ) (Set (Var "z9")))) ")" )) ")" ) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set ($#k2_numbers :::"COMPLEX"::: ) )))) "implies" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k14_quaterni :::"Im1"::: ) (Set (Var "z")))) "iff" (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Num 4) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool "(" (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set (Var "f"))) & (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Num 1))) ")" )) ")" ) ")" ")" ))); :: deftheorem defines :::"Im2"::: QUATERNI:def 15 : (Bool "for" (Set (Var "z")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "b2")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set ($#k2_numbers :::"COMPLEX"::: ) ))) "implies" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k15_quaterni :::"Im2"::: ) (Set (Var "z")))) "iff" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set ($#k2_numbers :::"COMPLEX"::: ) )))) "implies" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k15_quaterni :::"Im2"::: ) (Set (Var "z")))) "iff" (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Num 4) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool "(" (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set (Var "f"))) & (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Num 2))) ")" )) ")" ) ")" ")" ))); :: deftheorem defines :::"Im3"::: QUATERNI:def 16 : (Bool "for" (Set (Var "z")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "b2")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set ($#k2_numbers :::"COMPLEX"::: ) ))) "implies" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k16_quaterni :::"Im3"::: ) (Set (Var "z")))) "iff" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set ($#k2_numbers :::"COMPLEX"::: ) )))) "implies" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k16_quaterni :::"Im3"::: ) (Set (Var "z")))) "iff" (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Num 4) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool "(" (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set (Var "f"))) & (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Num 3))) ")" )) ")" ) ")" ")" ))); registrationlet "z" be ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set ($#k13_quaterni :::"Rea"::: ) "z") -> ($#v1_xreal_0 :::"real"::: ) ; cluster (Set ($#k14_quaterni :::"Im1"::: ) "z") -> ($#v1_xreal_0 :::"real"::: ) ; cluster (Set ($#k15_quaterni :::"Im2"::: ) "z") -> ($#v1_xreal_0 :::"real"::: ) ; cluster (Set ($#k16_quaterni :::"Im3"::: ) "z") -> ($#v1_xreal_0 :::"real"::: ) ; end; definitionlet "z" be ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) ; :: original: :::"Rea"::: redefine func :::"Rea"::: "z" -> ($#m1_subset_1 :::"Real":::); :: original: :::"Im1"::: redefine func :::"Im1"::: "z" -> ($#m1_subset_1 :::"Real":::); :: original: :::"Im2"::: redefine func :::"Im2"::: "z" -> ($#m1_subset_1 :::"Real":::); :: original: :::"Im3"::: redefine func :::"Im3"::: "z" -> ($#m1_subset_1 :::"Real":::); end; theorem :: QUATERNI:22 (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Num 4) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "ex" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Set (Var "f")) ($#r1_funct_2 :::"="::: ) (Set "(" (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) "," (Num 2) "," (Num 3) ")" ($#k3_quaterni :::"-->"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) ")" )))) ; theorem :: QUATERNI:23 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set ($#k17_quaterni :::"Rea"::: ) (Set ($#k6_quaterni :::"[*"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) ($#k6_quaterni :::"*]"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "a"))) & (Bool (Set ($#k18_quaterni :::"Im1"::: ) (Set ($#k6_quaterni :::"[*"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) ($#k6_quaterni :::"*]"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "b"))) & (Bool (Set ($#k19_quaterni :::"Im2"::: ) (Set ($#k6_quaterni :::"[*"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) ($#k6_quaterni :::"*]"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "c"))) & (Bool (Set ($#k20_quaterni :::"Im3"::: ) (Set ($#k6_quaterni :::"[*"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) ($#k6_quaterni :::"*]"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "d"))) ")" )) ; theorem :: QUATERNI:24 (Bool "for" (Set (Var "z")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set ($#k6_quaterni :::"[*"::: ) (Set "(" ($#k17_quaterni :::"Rea"::: ) (Set (Var "z")) ")" ) "," (Set "(" ($#k18_quaterni :::"Im1"::: ) (Set (Var "z")) ")" ) "," (Set "(" ($#k19_quaterni :::"Im2"::: ) (Set (Var "z")) ")" ) "," (Set "(" ($#k20_quaterni :::"Im3"::: ) (Set (Var "z")) ")" ) ($#k6_quaterni :::"*]"::: ) ))) ; theorem :: QUATERNI:25 (Bool "for" (Set (Var "z1")) "," (Set (Var "z2")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set ($#k17_quaterni :::"Rea"::: ) (Set (Var "z1"))) ($#r1_hidden :::"="::: ) (Set ($#k17_quaterni :::"Rea"::: ) (Set (Var "z2")))) & (Bool (Set ($#k18_quaterni :::"Im1"::: ) (Set (Var "z1"))) ($#r1_hidden :::"="::: ) (Set ($#k18_quaterni :::"Im1"::: ) (Set (Var "z2")))) & (Bool (Set ($#k19_quaterni :::"Im2"::: ) (Set (Var "z1"))) ($#r1_hidden :::"="::: ) (Set ($#k19_quaterni :::"Im2"::: ) (Set (Var "z2")))) & (Bool (Set ($#k20_quaterni :::"Im3"::: ) (Set (Var "z1"))) ($#r1_hidden :::"="::: ) (Set ($#k20_quaterni :::"Im3"::: ) (Set (Var "z2"))))) "holds" (Bool (Set (Var "z1")) ($#r1_hidden :::"="::: ) (Set (Var "z2")))) ; definitionfunc :::"0q"::: -> ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) equals :: QUATERNI:def 17 (Set ($#k6_numbers :::"0"::: ) ); func :::"1q"::: -> ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) equals :: QUATERNI:def 18 (Num 1); end; :: deftheorem defines :::"0q"::: QUATERNI:def 17 : (Bool (Set ($#k21_quaterni :::"0q"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )); :: deftheorem defines :::"1q"::: QUATERNI:def 18 : (Bool (Set ($#k22_quaterni :::"1q"::: ) ) ($#r1_hidden :::"="::: ) (Num 1)); theorem :: QUATERNI:26 (Bool "for" (Set (Var "z")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set ($#k17_quaterni :::"Rea"::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k18_quaterni :::"Im1"::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k19_quaterni :::"Im2"::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k20_quaterni :::"Im3"::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set ($#k21_quaterni :::"0q"::: ) ))) ; theorem :: QUATERNI:27 (Bool "for" (Set (Var "z")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set "(" (Set "(" (Set "(" (Set "(" ($#k17_quaterni :::"Rea"::: ) (Set (Var "z")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" ($#k18_quaterni :::"Im1"::: ) (Set (Var "z")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" ($#k19_quaterni :::"Im2"::: ) (Set (Var "z")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" ($#k20_quaterni :::"Im3"::: ) (Set (Var "z")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) ; theorem :: QUATERNI:28 (Bool "for" (Set (Var "z")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Set "(" (Set "(" (Set "(" (Set "(" ($#k17_quaterni :::"Rea"::: ) (Set (Var "z")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" ($#k18_quaterni :::"Im1"::: ) (Set (Var "z")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" ($#k19_quaterni :::"Im2"::: ) (Set (Var "z")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" ($#k20_quaterni :::"Im3"::: ) (Set (Var "z")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set ($#k21_quaterni :::"0q"::: ) ))) ; theorem :: QUATERNI:29 (Bool "(" (Bool (Set ($#k17_quaterni :::"Rea"::: ) (Set ($#k22_quaterni :::"1q"::: ) )) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set ($#k18_quaterni :::"Im1"::: ) (Set ($#k22_quaterni :::"1q"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k19_quaterni :::"Im2"::: ) (Set ($#k22_quaterni :::"1q"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k20_quaterni :::"Im3"::: ) (Set ($#k22_quaterni :::"1q"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) ; theorem :: QUATERNI:30 (Bool "(" (Bool (Set ($#k17_quaterni :::"Rea"::: ) (Set ($#k1_xcmplx_0 :::""::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k18_quaterni :::"Im1"::: ) (Set ($#k1_xcmplx_0 :::""::: ) )) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set ($#k19_quaterni :::"Im2"::: ) (Set ($#k1_xcmplx_0 :::""::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k20_quaterni :::"Im3"::: ) (Set ($#k1_xcmplx_0 :::""::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) ; theorem :: QUATERNI:31 (Bool "(" (Bool (Set ($#k17_quaterni :::"Rea"::: ) (Set ($#k11_quaterni :::""::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k18_quaterni :::"Im1"::: ) (Set ($#k11_quaterni :::""::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k19_quaterni :::"Im2"::: ) (Set ($#k11_quaterni :::""::: ) )) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set ($#k20_quaterni :::"Im3"::: ) (Set ($#k11_quaterni :::""::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k17_quaterni :::"Rea"::: ) (Set ($#k12_quaterni :::""::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k18_quaterni :::"Im1"::: ) (Set ($#k12_quaterni :::""::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k19_quaterni :::"Im2"::: ) (Set ($#k12_quaterni :::""::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k20_quaterni :::"Im3"::: ) (Set ($#k12_quaterni :::""::: ) )) ($#r1_hidden :::"="::: ) (Num 1)) ")" ) ; theorem :: QUATERNI:32 (Bool "for" (Set (Var "z1")) "," (Set (Var "z2")) "," (Set (Var "z3")) "," (Set (Var "z4")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set ($#k17_quaterni :::"Rea"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "z1")) ($#k7_quaterni :::"+"::: ) (Set (Var "z2")) ")" ) ($#k7_quaterni :::"+"::: ) (Set (Var "z3")) ")" ) ($#k7_quaterni :::"+"::: ) (Set (Var "z4")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" ($#k17_quaterni :::"Rea"::: ) (Set (Var "z1")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k17_quaterni :::"Rea"::: ) (Set (Var "z2")) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k17_quaterni :::"Rea"::: ) (Set (Var "z3")) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k17_quaterni :::"Rea"::: ) (Set (Var "z4")) ")" ))) & (Bool (Set ($#k18_quaterni :::"Im1"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "z1")) ($#k7_quaterni :::"+"::: ) (Set (Var "z2")) ")" ) ($#k7_quaterni :::"+"::: ) (Set (Var "z3")) ")" ) ($#k7_quaterni :::"+"::: ) (Set (Var "z4")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" ($#k18_quaterni :::"Im1"::: ) (Set (Var "z1")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k18_quaterni :::"Im1"::: ) (Set (Var "z2")) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k18_quaterni :::"Im1"::: ) (Set (Var "z3")) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k18_quaterni :::"Im1"::: ) (Set (Var "z4")) ")" ))) & (Bool (Set ($#k19_quaterni :::"Im2"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "z1")) ($#k7_quaterni :::"+"::: ) (Set (Var "z2")) ")" ) ($#k7_quaterni :::"+"::: ) (Set (Var "z3")) ")" ) ($#k7_quaterni :::"+"::: ) (Set (Var "z4")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" ($#k19_quaterni :::"Im2"::: ) (Set (Var "z1")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k19_quaterni :::"Im2"::: ) (Set (Var "z2")) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k19_quaterni :::"Im2"::: ) (Set (Var "z3")) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k19_quaterni :::"Im2"::: ) (Set (Var "z4")) ")" ))) & (Bool (Set ($#k20_quaterni :::"Im3"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "z1")) ($#k7_quaterni :::"+"::: ) (Set (Var "z2")) ")" ) ($#k7_quaterni :::"+"::: ) (Set (Var "z3")) ")" ) ($#k7_quaterni :::"+"::: ) (Set (Var "z4")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" ($#k20_quaterni :::"Im3"::: ) (Set (Var "z1")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k20_quaterni :::"Im3"::: ) (Set (Var "z2")) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k20_quaterni :::"Im3"::: ) (Set (Var "z3")) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k20_quaterni :::"Im3"::: ) (Set (Var "z4")) ")" ))) ")" )) ; theorem :: QUATERNI:33 (Bool "for" (Set (Var "z1")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "z1")) ($#r1_hidden :::"="::: ) (Set (Var "x")))) "holds" (Bool "(" (Bool (Set ($#k17_quaterni :::"Rea"::: ) (Set "(" (Set (Var "z1")) ($#k10_quaterni :::"*"::: ) (Set ($#k1_xcmplx_0 :::""::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k18_quaterni :::"Im1"::: ) (Set "(" (Set (Var "z1")) ($#k10_quaterni :::"*"::: ) (Set ($#k1_xcmplx_0 :::""::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "x"))) & (Bool (Set ($#k19_quaterni :::"Im2"::: ) (Set "(" (Set (Var "z1")) ($#k10_quaterni :::"*"::: ) (Set ($#k1_xcmplx_0 :::""::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k20_quaterni :::"Im3"::: ) (Set "(" (Set (Var "z1")) ($#k10_quaterni :::"*"::: ) (Set ($#k1_xcmplx_0 :::""::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ))) ; theorem :: QUATERNI:34 (Bool "for" (Set (Var "z1")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "z1")) ($#r1_hidden :::"="::: ) (Set (Var "x")))) "holds" (Bool "(" (Bool (Set ($#k17_quaterni :::"Rea"::: ) (Set "(" (Set (Var "z1")) ($#k10_quaterni :::"*"::: ) (Set ($#k11_quaterni :::""::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k18_quaterni :::"Im1"::: ) (Set "(" (Set (Var "z1")) ($#k10_quaterni :::"*"::: ) (Set ($#k11_quaterni :::""::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k19_quaterni :::"Im2"::: ) (Set "(" (Set (Var "z1")) ($#k10_quaterni :::"*"::: ) (Set ($#k11_quaterni :::""::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "x"))) & (Bool (Set ($#k20_quaterni :::"Im3"::: ) (Set "(" (Set (Var "z1")) ($#k10_quaterni :::"*"::: ) (Set ($#k11_quaterni :::""::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ))) ; theorem :: QUATERNI:35 (Bool "for" (Set (Var "z1")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "z1")) ($#r1_hidden :::"="::: ) (Set (Var "x")))) "holds" (Bool "(" (Bool (Set ($#k17_quaterni :::"Rea"::: ) (Set "(" (Set (Var "z1")) ($#k10_quaterni :::"*"::: ) (Set ($#k12_quaterni :::""::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k18_quaterni :::"Im1"::: ) (Set "(" (Set (Var "z1")) ($#k10_quaterni :::"*"::: ) (Set ($#k12_quaterni :::""::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k19_quaterni :::"Im2"::: ) (Set "(" (Set (Var "z1")) ($#k10_quaterni :::"*"::: ) (Set ($#k12_quaterni :::""::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k20_quaterni :::"Im3"::: ) (Set "(" (Set (Var "z1")) ($#k10_quaterni :::"*"::: ) (Set ($#k12_quaterni :::""::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "x"))) ")" ))) ; definitionlet "x" be ($#m1_subset_1 :::"Real":::); let "y" be ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) ; func "x" :::"+"::: "y" -> ($#m1_hidden :::"set"::: ) means :: QUATERNI:def 19 (Bool "ex" (Set (Var "y1")) "," (Set (Var "y2")) "," (Set (Var "y3")) "," (Set (Var "y4")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool "(" (Bool "y" ($#r1_hidden :::"="::: ) (Set ($#k6_quaterni :::"[*"::: ) (Set (Var "y1")) "," (Set (Var "y2")) "," (Set (Var "y3")) "," (Set (Var "y4")) ($#k6_quaterni :::"*]"::: ) )) & (Bool it ($#r1_hidden :::"="::: ) (Set ($#k6_quaterni :::"[*"::: ) (Set "(" "x" ($#k7_real_1 :::"+"::: ) (Set (Var "y1")) ")" ) "," (Set (Var "y2")) "," (Set (Var "y3")) "," (Set (Var "y4")) ($#k6_quaterni :::"*]"::: ) )) ")" )); end; :: deftheorem defines :::"+"::: QUATERNI:def 19 : (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "y")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "b3")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k23_quaterni :::"+"::: ) (Set (Var "y")))) "iff" (Bool "ex" (Set (Var "y1")) "," (Set (Var "y2")) "," (Set (Var "y3")) "," (Set (Var "y4")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool "(" (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set ($#k6_quaterni :::"[*"::: ) (Set (Var "y1")) "," (Set (Var "y2")) "," (Set (Var "y3")) "," (Set (Var "y4")) ($#k6_quaterni :::"*]"::: ) )) & (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k6_quaterni :::"[*"::: ) (Set "(" (Set (Var "x")) ($#k7_real_1 :::"+"::: ) (Set (Var "y1")) ")" ) "," (Set (Var "y2")) "," (Set (Var "y3")) "," (Set (Var "y4")) ($#k6_quaterni :::"*]"::: ) )) ")" )) ")" )))); definitionlet "x" be ($#m1_subset_1 :::"Real":::); let "y" be ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) ; func "x" :::"-"::: "y" -> ($#m1_hidden :::"set"::: ) equals :: QUATERNI:def 20 (Set "x" ($#k23_quaterni :::"+"::: ) (Set "(" ($#k8_quaterni :::"-"::: ) "y" ")" )); end; :: deftheorem defines :::"-"::: QUATERNI:def 20 : (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "y")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "x")) ($#k24_quaterni :::"-"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k23_quaterni :::"+"::: ) (Set "(" ($#k8_quaterni :::"-"::: ) (Set (Var "y")) ")" ))))); definitionlet "x" be ($#m1_subset_1 :::"Real":::); let "y" be ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) ; func "x" :::"*"::: "y" -> ($#m1_hidden :::"set"::: ) means :: QUATERNI:def 21 (Bool "ex" (Set (Var "y1")) "," (Set (Var "y2")) "," (Set (Var "y3")) "," (Set (Var "y4")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool "(" (Bool "y" ($#r1_hidden :::"="::: ) (Set ($#k6_quaterni :::"[*"::: ) (Set (Var "y1")) "," (Set (Var "y2")) "," (Set (Var "y3")) "," (Set (Var "y4")) ($#k6_quaterni :::"*]"::: ) )) & (Bool it ($#r1_hidden :::"="::: ) (Set ($#k6_quaterni :::"[*"::: ) (Set "(" "x" ($#k8_real_1 :::"*"::: ) (Set (Var "y1")) ")" ) "," (Set "(" "x" ($#k8_real_1 :::"*"::: ) (Set (Var "y2")) ")" ) "," (Set "(" "x" ($#k8_real_1 :::"*"::: ) (Set (Var "y3")) ")" ) "," (Set "(" "x" ($#k8_real_1 :::"*"::: ) (Set (Var "y4")) ")" ) ($#k6_quaterni :::"*]"::: ) )) ")" )); end; :: deftheorem defines :::"*"::: QUATERNI:def 21 : (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "y")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "b3")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k25_quaterni :::"*"::: ) (Set (Var "y")))) "iff" (Bool "ex" (Set (Var "y1")) "," (Set (Var "y2")) "," (Set (Var "y3")) "," (Set (Var "y4")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool "(" (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set ($#k6_quaterni :::"[*"::: ) (Set (Var "y1")) "," (Set (Var "y2")) "," (Set (Var "y3")) "," (Set (Var "y4")) ($#k6_quaterni :::"*]"::: ) )) & (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k6_quaterni :::"[*"::: ) (Set "(" (Set (Var "x")) ($#k8_real_1 :::"*"::: ) (Set (Var "y1")) ")" ) "," (Set "(" (Set (Var "x")) ($#k8_real_1 :::"*"::: ) (Set (Var "y2")) ")" ) "," (Set "(" (Set (Var "x")) ($#k8_real_1 :::"*"::: ) (Set (Var "y3")) ")" ) "," (Set "(" (Set (Var "x")) ($#k8_real_1 :::"*"::: ) (Set (Var "y4")) ")" ) ($#k6_quaterni :::"*]"::: ) )) ")" )) ")" )))); registrationlet "x" be ($#m1_subset_1 :::"Real":::); let "z9" be ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set "x" ($#k23_quaterni :::"+"::: ) "z9") -> ($#v1_quaterni :::"quaternion"::: ) ; cluster (Set "x" ($#k25_quaterni :::"*"::: ) "z9") -> ($#v1_quaterni :::"quaternion"::: ) ; cluster (Set "x" ($#k24_quaterni :::"-"::: ) "z9") -> ($#v1_quaterni :::"quaternion"::: ) ; end; definitionlet "z1", "z2" be ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) ; :: original: :::"+"::: redefine func "z1" :::"+"::: "z2" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_quaterni :::"QUATERNION"::: ) ); end; theorem :: QUATERNI:36 (Bool "for" (Set (Var "z1")) "," (Set (Var "z2")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set ($#k17_quaterni :::"Rea"::: ) (Set "(" (Set (Var "z1")) ($#k26_quaterni :::"+"::: ) (Set (Var "z2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k17_quaterni :::"Rea"::: ) (Set (Var "z1")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k17_quaterni :::"Rea"::: ) (Set (Var "z2")) ")" ))) & (Bool (Set ($#k18_quaterni :::"Im1"::: ) (Set "(" (Set (Var "z1")) ($#k26_quaterni :::"+"::: ) (Set (Var "z2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k18_quaterni :::"Im1"::: ) (Set (Var "z1")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k18_quaterni :::"Im1"::: ) (Set (Var "z2")) ")" ))) & (Bool (Set ($#k19_quaterni :::"Im2"::: ) (Set "(" (Set (Var "z1")) ($#k26_quaterni :::"+"::: ) (Set (Var "z2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k19_quaterni :::"Im2"::: ) (Set (Var "z1")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k19_quaterni :::"Im2"::: ) (Set (Var "z2")) ")" ))) & (Bool (Set ($#k20_quaterni :::"Im3"::: ) (Set "(" (Set (Var "z1")) ($#k26_quaterni :::"+"::: ) (Set (Var "z2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k20_quaterni :::"Im3"::: ) (Set (Var "z1")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k20_quaterni :::"Im3"::: ) (Set (Var "z2")) ")" ))) ")" )) ; definitionlet "z1", "z2" be ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) ; :: original: :::"*"::: redefine func "z1" :::"*"::: "z2" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_quaterni :::"QUATERNION"::: ) ); end; theorem :: QUATERNI:37 (Bool "for" (Set (Var "z")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" ($#k17_quaterni :::"Rea"::: ) (Set (Var "z")) ")" ) ($#k23_quaterni :::"+"::: ) (Set "(" (Set "(" ($#k18_quaterni :::"Im1"::: ) (Set (Var "z")) ")" ) ($#k25_quaterni :::"*"::: ) (Set ($#k1_xcmplx_0 :::""::: ) ) ")" ) ")" ) ($#k26_quaterni :::"+"::: ) (Set "(" (Set "(" ($#k19_quaterni :::"Im2"::: ) (Set (Var "z")) ")" ) ($#k25_quaterni :::"*"::: ) (Set ($#k11_quaterni :::""::: ) ) ")" ) ")" ) ($#k26_quaterni :::"+"::: ) (Set "(" (Set "(" ($#k20_quaterni :::"Im3"::: ) (Set (Var "z")) ")" ) ($#k25_quaterni :::"*"::: ) (Set ($#k12_quaterni :::""::: ) ) ")" )))) ; theorem :: QUATERNI:38 (Bool "for" (Set (Var "z1")) "," (Set (Var "z2")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set ($#k18_quaterni :::"Im1"::: ) (Set (Var "z1"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k18_quaterni :::"Im1"::: ) (Set (Var "z2"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k19_quaterni :::"Im2"::: ) (Set (Var "z1"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k19_quaterni :::"Im2"::: ) (Set (Var "z2"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k20_quaterni :::"Im3"::: ) (Set (Var "z1"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k20_quaterni :::"Im3"::: ) (Set (Var "z2"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "(" (Bool (Set ($#k17_quaterni :::"Rea"::: ) (Set "(" (Set (Var "z1")) ($#k27_quaterni :::"*"::: ) (Set (Var "z2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k17_quaterni :::"Rea"::: ) (Set (Var "z1")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k17_quaterni :::"Rea"::: ) (Set (Var "z2")) ")" ))) & (Bool (Set ($#k18_quaterni :::"Im1"::: ) (Set "(" (Set (Var "z1")) ($#k27_quaterni :::"*"::: ) (Set (Var "z2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k19_quaterni :::"Im2"::: ) (Set (Var "z1")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k20_quaterni :::"Im3"::: ) (Set (Var "z2")) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" ($#k20_quaterni :::"Im3"::: ) (Set (Var "z1")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k19_quaterni :::"Im2"::: ) (Set (Var "z2")) ")" ) ")" ))) & (Bool (Set ($#k19_quaterni :::"Im2"::: ) (Set "(" (Set (Var "z1")) ($#k27_quaterni :::"*"::: ) (Set (Var "z2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k20_quaterni :::"Im3"::: ) (Set (Var "z1")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k18_quaterni :::"Im1"::: ) (Set (Var "z2")) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" ($#k18_quaterni :::"Im1"::: ) (Set (Var "z1")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k20_quaterni :::"Im3"::: ) (Set (Var "z2")) ")" ) ")" ))) & (Bool (Set ($#k20_quaterni :::"Im3"::: ) (Set "(" (Set (Var "z1")) ($#k27_quaterni :::"*"::: ) (Set (Var "z2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k18_quaterni :::"Im1"::: ) (Set (Var "z1")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k19_quaterni :::"Im2"::: ) (Set (Var "z2")) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" ($#k19_quaterni :::"Im2"::: ) (Set (Var "z1")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k18_quaterni :::"Im1"::: ) (Set (Var "z2")) ")" ) ")" ))) ")" )) ; theorem :: QUATERNI:39 (Bool "for" (Set (Var "z1")) "," (Set (Var "z2")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set ($#k17_quaterni :::"Rea"::: ) (Set (Var "z1"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k17_quaterni :::"Rea"::: ) (Set (Var "z2"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "(" (Bool (Set ($#k17_quaterni :::"Rea"::: ) (Set "(" (Set (Var "z1")) ($#k27_quaterni :::"*"::: ) (Set (Var "z2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" (Set "(" ($#k18_quaterni :::"Im1"::: ) (Set (Var "z1")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k18_quaterni :::"Im1"::: ) (Set (Var "z2")) ")" ) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" ($#k19_quaterni :::"Im2"::: ) (Set (Var "z1")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k19_quaterni :::"Im2"::: ) (Set (Var "z2")) ")" ) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" ($#k20_quaterni :::"Im3"::: ) (Set (Var "z1")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k20_quaterni :::"Im3"::: ) (Set (Var "z2")) ")" ) ")" ))) & (Bool (Set ($#k18_quaterni :::"Im1"::: ) (Set "(" (Set (Var "z1")) ($#k27_quaterni :::"*"::: ) (Set (Var "z2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k19_quaterni :::"Im2"::: ) (Set (Var "z1")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k20_quaterni :::"Im3"::: ) (Set (Var "z2")) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" ($#k20_quaterni :::"Im3"::: ) (Set (Var "z1")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k19_quaterni :::"Im2"::: ) (Set (Var "z2")) ")" ) ")" ))) & (Bool (Set ($#k19_quaterni :::"Im2"::: ) (Set "(" (Set (Var "z1")) ($#k27_quaterni :::"*"::: ) (Set (Var "z2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k20_quaterni :::"Im3"::: ) (Set (Var "z1")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k18_quaterni :::"Im1"::: ) (Set (Var "z2")) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" ($#k18_quaterni :::"Im1"::: ) (Set (Var "z1")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k20_quaterni :::"Im3"::: ) (Set (Var "z2")) ")" ) ")" ))) & (Bool (Set ($#k20_quaterni :::"Im3"::: ) (Set "(" (Set (Var "z1")) ($#k27_quaterni :::"*"::: ) (Set (Var "z2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k18_quaterni :::"Im1"::: ) (Set (Var "z1")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k19_quaterni :::"Im2"::: ) (Set (Var "z2")) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" ($#k19_quaterni :::"Im2"::: ) (Set (Var "z1")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k18_quaterni :::"Im1"::: ) (Set (Var "z2")) ")" ) ")" ))) ")" )) ; theorem :: QUATERNI:40 (Bool "for" (Set (Var "z")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set ($#k17_quaterni :::"Rea"::: ) (Set "(" (Set (Var "z")) ($#k27_quaterni :::"*"::: ) (Set (Var "z")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set "(" ($#k17_quaterni :::"Rea"::: ) (Set (Var "z")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" ($#k18_quaterni :::"Im1"::: ) (Set (Var "z")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" ($#k19_quaterni :::"Im2"::: ) (Set (Var "z")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" ($#k20_quaterni :::"Im3"::: ) (Set (Var "z")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ))) & (Bool (Set ($#k18_quaterni :::"Im1"::: ) (Set "(" (Set (Var "z")) ($#k27_quaterni :::"*"::: ) (Set (Var "z")) ")" )) ($#r1_hidden :::"="::: ) (Set (Num 2) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" ($#k17_quaterni :::"Rea"::: ) (Set (Var "z")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k18_quaterni :::"Im1"::: ) (Set (Var "z")) ")" ) ")" ))) & (Bool (Set ($#k19_quaterni :::"Im2"::: ) (Set "(" (Set (Var "z")) ($#k27_quaterni :::"*"::: ) (Set (Var "z")) ")" )) ($#r1_hidden :::"="::: ) (Set (Num 2) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" ($#k17_quaterni :::"Rea"::: ) (Set (Var "z")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k19_quaterni :::"Im2"::: ) (Set (Var "z")) ")" ) ")" ))) & (Bool (Set ($#k20_quaterni :::"Im3"::: ) (Set "(" (Set (Var "z")) ($#k27_quaterni :::"*"::: ) (Set (Var "z")) ")" )) ($#r1_hidden :::"="::: ) (Set (Num 2) ($#k8_real_1 :::"*"::: ) (Set "(" (Set "(" ($#k17_quaterni :::"Rea"::: ) (Set (Var "z")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k20_quaterni :::"Im3"::: ) (Set (Var "z")) ")" ) ")" ))) ")" )) ; definitionlet "z" be ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) ; :: original: :::"-"::: redefine func :::"-"::: "z" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_quaterni :::"QUATERNION"::: ) ); end; theorem :: QUATERNI:41 (Bool "for" (Set (Var "z")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set ($#k17_quaterni :::"Rea"::: ) (Set "(" ($#k28_quaterni :::"-"::: ) (Set (Var "z")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Set "(" ($#k17_quaterni :::"Rea"::: ) (Set (Var "z")) ")" ))) & (Bool (Set ($#k18_quaterni :::"Im1"::: ) (Set "(" ($#k28_quaterni :::"-"::: ) (Set (Var "z")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Set "(" ($#k18_quaterni :::"Im1"::: ) (Set (Var "z")) ")" ))) & (Bool (Set ($#k19_quaterni :::"Im2"::: ) (Set "(" ($#k28_quaterni :::"-"::: ) (Set (Var "z")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Set "(" ($#k19_quaterni :::"Im2"::: ) (Set (Var "z")) ")" ))) & (Bool (Set ($#k20_quaterni :::"Im3"::: ) (Set "(" ($#k28_quaterni :::"-"::: ) (Set (Var "z")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Set "(" ($#k20_quaterni :::"Im3"::: ) (Set (Var "z")) ")" ))) ")" )) ; definitionlet "z1", "z2" be ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) ; :: original: :::"-"::: redefine func "z1" :::"-"::: "z2" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_quaterni :::"QUATERNION"::: ) ); end; theorem :: QUATERNI:42 (Bool "for" (Set (Var "z1")) "," (Set (Var "z2")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set ($#k17_quaterni :::"Rea"::: ) (Set "(" (Set (Var "z1")) ($#k29_quaterni :::"-"::: ) (Set (Var "z2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k17_quaterni :::"Rea"::: ) (Set (Var "z1")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" ($#k17_quaterni :::"Rea"::: ) (Set (Var "z2")) ")" ))) & (Bool (Set ($#k18_quaterni :::"Im1"::: ) (Set "(" (Set (Var "z1")) ($#k29_quaterni :::"-"::: ) (Set (Var "z2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k18_quaterni :::"Im1"::: ) (Set (Var "z1")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" ($#k18_quaterni :::"Im1"::: ) (Set (Var "z2")) ")" ))) & (Bool (Set ($#k19_quaterni :::"Im2"::: ) (Set "(" (Set (Var "z1")) ($#k29_quaterni :::"-"::: ) (Set (Var "z2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k19_quaterni :::"Im2"::: ) (Set (Var "z1")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" ($#k19_quaterni :::"Im2"::: ) (Set (Var "z2")) ")" ))) & (Bool (Set ($#k20_quaterni :::"Im3"::: ) (Set "(" (Set (Var "z1")) ($#k29_quaterni :::"-"::: ) (Set (Var "z2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k20_quaterni :::"Im3"::: ) (Set (Var "z1")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" ($#k20_quaterni :::"Im3"::: ) (Set (Var "z2")) ")" ))) ")" )) ; definitionlet "z" be ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) ; func "z" :::"*'"::: -> ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) equals :: QUATERNI:def 22 (Set (Set "(" (Set "(" (Set "(" ($#k17_quaterni :::"Rea"::: ) "z" ")" ) ($#k23_quaterni :::"+"::: ) (Set "(" (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" ($#k18_quaterni :::"Im1"::: ) "z" ")" ) ")" ) ($#k25_quaterni :::"*"::: ) (Set ($#k1_xcmplx_0 :::""::: ) ) ")" ) ")" ) ($#k26_quaterni :::"+"::: ) (Set "(" (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" ($#k19_quaterni :::"Im2"::: ) "z" ")" ) ")" ) ($#k25_quaterni :::"*"::: ) (Set ($#k11_quaterni :::""::: ) ) ")" ) ")" ) ($#k26_quaterni :::"+"::: ) (Set "(" (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" ($#k20_quaterni :::"Im3"::: ) "z" ")" ) ")" ) ($#k25_quaterni :::"*"::: ) (Set ($#k12_quaterni :::""::: ) ) ")" )); end; :: deftheorem defines :::"*'"::: QUATERNI:def 22 : (Bool "for" (Set (Var "z")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "z")) ($#k30_quaterni :::"*'"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" ($#k17_quaterni :::"Rea"::: ) (Set (Var "z")) ")" ) ($#k23_quaterni :::"+"::: ) (Set "(" (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" ($#k18_quaterni :::"Im1"::: ) (Set (Var "z")) ")" ) ")" ) ($#k25_quaterni :::"*"::: ) (Set ($#k1_xcmplx_0 :::""::: ) ) ")" ) ")" ) ($#k26_quaterni :::"+"::: ) (Set "(" (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" ($#k19_quaterni :::"Im2"::: ) (Set (Var "z")) ")" ) ")" ) ($#k25_quaterni :::"*"::: ) (Set ($#k11_quaterni :::""::: ) ) ")" ) ")" ) ($#k26_quaterni :::"+"::: ) (Set "(" (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" ($#k20_quaterni :::"Im3"::: ) (Set (Var "z")) ")" ) ")" ) ($#k25_quaterni :::"*"::: ) (Set ($#k12_quaterni :::""::: ) ) ")" )))); definitionlet "z" be ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) ; :: original: :::"*'"::: redefine func "z" :::"*'"::: -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_quaterni :::"QUATERNION"::: ) ); end; theorem :: QUATERNI:43 (Bool "for" (Set (Var "z")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "z")) ($#k31_quaterni :::"*'"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_quaterni :::"[*"::: ) (Set "(" ($#k17_quaterni :::"Rea"::: ) (Set (Var "z")) ")" ) "," (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" ($#k18_quaterni :::"Im1"::: ) (Set (Var "z")) ")" ) ")" ) "," (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" ($#k19_quaterni :::"Im2"::: ) (Set (Var "z")) ")" ) ")" ) "," (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" ($#k20_quaterni :::"Im3"::: ) (Set (Var "z")) ")" ) ")" ) ($#k6_quaterni :::"*]"::: ) ))) ; theorem :: QUATERNI:44 (Bool "for" (Set (Var "z")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set ($#k17_quaterni :::"Rea"::: ) (Set "(" (Set (Var "z")) ($#k31_quaterni :::"*'"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k17_quaterni :::"Rea"::: ) (Set (Var "z")))) & (Bool (Set ($#k18_quaterni :::"Im1"::: ) (Set "(" (Set (Var "z")) ($#k31_quaterni :::"*'"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Set "(" ($#k18_quaterni :::"Im1"::: ) (Set (Var "z")) ")" ))) & (Bool (Set ($#k19_quaterni :::"Im2"::: ) (Set "(" (Set (Var "z")) ($#k31_quaterni :::"*'"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Set "(" ($#k19_quaterni :::"Im2"::: ) (Set (Var "z")) ")" ))) & (Bool (Set ($#k20_quaterni :::"Im3"::: ) (Set "(" (Set (Var "z")) ($#k31_quaterni :::"*'"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Set "(" ($#k20_quaterni :::"Im3"::: ) (Set (Var "z")) ")" ))) ")" )) ; theorem :: QUATERNI:45 (Bool "for" (Set (Var "z")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set (Var "z")) ($#k31_quaterni :::"*'"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) ; theorem :: QUATERNI:46 (Bool "for" (Set (Var "z")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Set (Var "z")) ($#k31_quaterni :::"*'"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) ; theorem :: QUATERNI:47 (Bool (Set (Set ($#k22_quaterni :::"1q"::: ) ) ($#k31_quaterni :::"*'"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k22_quaterni :::"1q"::: ) )) ; theorem :: QUATERNI:48 (Bool "(" (Bool (Set ($#k17_quaterni :::"Rea"::: ) (Set "(" (Set ($#k1_xcmplx_0 :::""::: ) ) ($#k31_quaterni :::"*'"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k18_quaterni :::"Im1"::: ) (Set "(" (Set ($#k1_xcmplx_0 :::""::: ) ) ($#k31_quaterni :::"*'"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Num 1))) & (Bool (Set ($#k19_quaterni :::"Im2"::: ) (Set "(" (Set ($#k1_xcmplx_0 :::""::: ) ) ($#k31_quaterni :::"*'"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k20_quaterni :::"Im3"::: ) (Set "(" (Set ($#k1_xcmplx_0 :::""::: ) ) ($#k31_quaterni :::"*'"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) ; theorem :: QUATERNI:49 (Bool "(" (Bool (Set ($#k17_quaterni :::"Rea"::: ) (Set "(" (Set ($#k11_quaterni :::""::: ) ) ($#k31_quaterni :::"*'"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k18_quaterni :::"Im1"::: ) (Set "(" (Set ($#k11_quaterni :::""::: ) ) ($#k31_quaterni :::"*'"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k19_quaterni :::"Im2"::: ) (Set "(" (Set ($#k11_quaterni :::""::: ) ) ($#k31_quaterni :::"*'"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Num 1))) & (Bool (Set ($#k20_quaterni :::"Im3"::: ) (Set "(" (Set ($#k11_quaterni :::""::: ) ) ($#k31_quaterni :::"*'"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) ; theorem :: QUATERNI:50 (Bool "(" (Bool (Set ($#k17_quaterni :::"Rea"::: ) (Set "(" (Set ($#k12_quaterni :::""::: ) ) ($#k31_quaterni :::"*'"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k18_quaterni :::"Im1"::: ) (Set "(" (Set ($#k12_quaterni :::""::: ) ) ($#k31_quaterni :::"*'"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k19_quaterni :::"Im2"::: ) (Set "(" (Set ($#k12_quaterni :::""::: ) ) ($#k31_quaterni :::"*'"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k20_quaterni :::"Im3"::: ) (Set "(" (Set ($#k12_quaterni :::""::: ) ) ($#k31_quaterni :::"*'"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Num 1))) ")" ) ; theorem :: QUATERNI:51 (Bool (Set (Set ($#k1_xcmplx_0 :::""::: ) ) ($#k31_quaterni :::"*'"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k28_quaterni :::"-"::: ) (Set ($#k1_xcmplx_0 :::""::: ) ))) ; theorem :: QUATERNI:52 (Bool (Set (Set ($#k11_quaterni :::""::: ) ) ($#k31_quaterni :::"*'"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k28_quaterni :::"-"::: ) (Set ($#k11_quaterni :::""::: ) ))) ; theorem :: QUATERNI:53 (Bool (Set (Set ($#k12_quaterni :::""::: ) ) ($#k31_quaterni :::"*'"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k28_quaterni :::"-"::: ) (Set ($#k12_quaterni :::""::: ) ))) ; theorem :: QUATERNI:54 (Bool "for" (Set (Var "z1")) "," (Set (Var "z2")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set "(" (Set (Var "z1")) ($#k26_quaterni :::"+"::: ) (Set (Var "z2")) ")" ) ($#k31_quaterni :::"*'"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "z1")) ($#k31_quaterni :::"*'"::: ) ")" ) ($#k26_quaterni :::"+"::: ) (Set "(" (Set (Var "z2")) ($#k31_quaterni :::"*'"::: ) ")" )))) ; theorem :: QUATERNI:55 (Bool "for" (Set (Var "z")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set "(" ($#k28_quaterni :::"-"::: ) (Set (Var "z")) ")" ) ($#k31_quaterni :::"*'"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k28_quaterni :::"-"::: ) (Set "(" (Set (Var "z")) ($#k31_quaterni :::"*'"::: ) ")" )))) ; theorem :: QUATERNI:56 (Bool "for" (Set (Var "z1")) "," (Set (Var "z2")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set "(" (Set (Var "z1")) ($#k29_quaterni :::"-"::: ) (Set (Var "z2")) ")" ) ($#k31_quaterni :::"*'"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "z1")) ($#k31_quaterni :::"*'"::: ) ")" ) ($#k29_quaterni :::"-"::: ) (Set "(" (Set (Var "z2")) ($#k31_quaterni :::"*'"::: ) ")" )))) ; theorem :: QUATERNI:57 (Bool "for" (Set (Var "z1")) "," (Set (Var "z2")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Set "(" (Set (Var "z1")) ($#k27_quaterni :::"*"::: ) (Set (Var "z2")) ")" ) ($#k31_quaterni :::"*'"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "z1")) ($#k31_quaterni :::"*'"::: ) ")" ) ($#k27_quaterni :::"*"::: ) (Set "(" (Set (Var "z2")) ($#k31_quaterni :::"*'"::: ) ")" )))) "holds" (Bool (Set (Set "(" ($#k19_quaterni :::"Im2"::: ) (Set (Var "z1")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k20_quaterni :::"Im3"::: ) (Set (Var "z2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k20_quaterni :::"Im3"::: ) (Set (Var "z1")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k19_quaterni :::"Im2"::: ) (Set (Var "z2")) ")" )))) ; theorem :: QUATERNI:58 (Bool "for" (Set (Var "z")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set ($#k18_quaterni :::"Im1"::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k19_quaterni :::"Im2"::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k20_quaterni :::"Im3"::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set (Var "z")) ($#k31_quaterni :::"*'"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "z")))) ; theorem :: QUATERNI:59 (Bool "for" (Set (Var "z")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set ($#k17_quaterni :::"Rea"::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set (Var "z")) ($#k31_quaterni :::"*'"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k28_quaterni :::"-"::: ) (Set (Var "z"))))) ; theorem :: QUATERNI:60 (Bool "for" (Set (Var "z")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set ($#k17_quaterni :::"Rea"::: ) (Set "(" (Set (Var "z")) ($#k27_quaterni :::"*"::: ) (Set "(" (Set (Var "z")) ($#k31_quaterni :::"*'"::: ) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set "(" ($#k17_quaterni :::"Rea"::: ) (Set (Var "z")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" ($#k18_quaterni :::"Im1"::: ) (Set (Var "z")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" ($#k19_quaterni :::"Im2"::: ) (Set (Var "z")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" ($#k20_quaterni :::"Im3"::: ) (Set (Var "z")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ))) & (Bool (Set ($#k18_quaterni :::"Im1"::: ) (Set "(" (Set (Var "z")) ($#k27_quaterni :::"*"::: ) (Set "(" (Set (Var "z")) ($#k31_quaterni :::"*'"::: ) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k19_quaterni :::"Im2"::: ) (Set "(" (Set (Var "z")) ($#k27_quaterni :::"*"::: ) (Set "(" (Set (Var "z")) ($#k31_quaterni :::"*'"::: ) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k20_quaterni :::"Im3"::: ) (Set "(" (Set (Var "z")) ($#k27_quaterni :::"*"::: ) (Set "(" (Set (Var "z")) ($#k31_quaterni :::"*'"::: ) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )) ; theorem :: QUATERNI:61 (Bool "for" (Set (Var "z")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set ($#k17_quaterni :::"Rea"::: ) (Set "(" (Set (Var "z")) ($#k26_quaterni :::"+"::: ) (Set "(" (Set (Var "z")) ($#k31_quaterni :::"*'"::: ) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Num 2) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k17_quaterni :::"Rea"::: ) (Set (Var "z")) ")" ))) & (Bool (Set ($#k18_quaterni :::"Im1"::: ) (Set "(" (Set (Var "z")) ($#k26_quaterni :::"+"::: ) (Set "(" (Set (Var "z")) ($#k31_quaterni :::"*'"::: ) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k19_quaterni :::"Im2"::: ) (Set "(" (Set (Var "z")) ($#k26_quaterni :::"+"::: ) (Set "(" (Set (Var "z")) ($#k31_quaterni :::"*'"::: ) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k20_quaterni :::"Im3"::: ) (Set "(" (Set (Var "z")) ($#k26_quaterni :::"+"::: ) (Set "(" (Set (Var "z")) ($#k31_quaterni :::"*'"::: ) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )) ; theorem :: QUATERNI:62 (Bool "for" (Set (Var "z")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k28_quaterni :::"-"::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set ($#k6_quaterni :::"[*"::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" ($#k17_quaterni :::"Rea"::: ) (Set (Var "z")) ")" ) ")" ) "," (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" ($#k18_quaterni :::"Im1"::: ) (Set (Var "z")) ")" ) ")" ) "," (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" ($#k19_quaterni :::"Im2"::: ) (Set (Var "z")) ")" ) ")" ) "," (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" ($#k20_quaterni :::"Im3"::: ) (Set (Var "z")) ")" ) ")" ) ($#k6_quaterni :::"*]"::: ) ))) ; theorem :: QUATERNI:63 (Bool "for" (Set (Var "z1")) "," (Set (Var "z2")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "z1")) ($#k29_quaterni :::"-"::: ) (Set (Var "z2"))) ($#r1_hidden :::"="::: ) (Set ($#k6_quaterni :::"[*"::: ) (Set "(" (Set "(" ($#k17_quaterni :::"Rea"::: ) (Set (Var "z1")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" ($#k17_quaterni :::"Rea"::: ) (Set (Var "z2")) ")" ) ")" ) "," (Set "(" (Set "(" ($#k18_quaterni :::"Im1"::: ) (Set (Var "z1")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" ($#k18_quaterni :::"Im1"::: ) (Set (Var "z2")) ")" ) ")" ) "," (Set "(" (Set "(" ($#k19_quaterni :::"Im2"::: ) (Set (Var "z1")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" ($#k19_quaterni :::"Im2"::: ) (Set (Var "z2")) ")" ) ")" ) "," (Set "(" (Set "(" ($#k20_quaterni :::"Im3"::: ) (Set (Var "z1")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" ($#k20_quaterni :::"Im3"::: ) (Set (Var "z2")) ")" ) ")" ) ($#k6_quaterni :::"*]"::: ) ))) ; theorem :: QUATERNI:64 (Bool "for" (Set (Var "z")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set ($#k17_quaterni :::"Rea"::: ) (Set "(" (Set (Var "z")) ($#k29_quaterni :::"-"::: ) (Set "(" (Set (Var "z")) ($#k31_quaterni :::"*'"::: ) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k18_quaterni :::"Im1"::: ) (Set "(" (Set (Var "z")) ($#k29_quaterni :::"-"::: ) (Set "(" (Set (Var "z")) ($#k31_quaterni :::"*'"::: ) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Num 2) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k18_quaterni :::"Im1"::: ) (Set (Var "z")) ")" ))) & (Bool (Set ($#k19_quaterni :::"Im2"::: ) (Set "(" (Set (Var "z")) ($#k29_quaterni :::"-"::: ) (Set "(" (Set (Var "z")) ($#k31_quaterni :::"*'"::: ) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Num 2) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k19_quaterni :::"Im2"::: ) (Set (Var "z")) ")" ))) & (Bool (Set ($#k20_quaterni :::"Im3"::: ) (Set "(" (Set (Var "z")) ($#k29_quaterni :::"-"::: ) (Set "(" (Set (Var "z")) ($#k31_quaterni :::"*'"::: ) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Num 2) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k20_quaterni :::"Im3"::: ) (Set (Var "z")) ")" ))) ")" )) ; definitionlet "z" be ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) ; func :::"|.":::"z":::".|"::: -> ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) equals :: QUATERNI:def 23 (Set ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" ($#k17_quaterni :::"Rea"::: ) "z" ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" ($#k18_quaterni :::"Im1"::: ) "z" ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" ($#k19_quaterni :::"Im2"::: ) "z" ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" ($#k20_quaterni :::"Im3"::: ) "z" ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" )); end; :: deftheorem defines :::"|."::: QUATERNI:def 23 : (Bool "for" (Set (Var "z")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k32_quaterni :::"|."::: ) (Set (Var "z")) ($#k32_quaterni :::".|"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" ($#k17_quaterni :::"Rea"::: ) (Set (Var "z")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" ($#k18_quaterni :::"Im1"::: ) (Set (Var "z")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" ($#k19_quaterni :::"Im2"::: ) (Set (Var "z")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" ($#k20_quaterni :::"Im3"::: ) (Set (Var "z")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" )))); theorem :: QUATERNI:65 (Bool (Set ($#k32_quaterni :::"|."::: ) (Set ($#k21_quaterni :::"0q"::: ) ) ($#k32_quaterni :::".|"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ; theorem :: QUATERNI:66 (Bool "for" (Set (Var "z")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set ($#k32_quaterni :::"|."::: ) (Set (Var "z")) ($#k32_quaterni :::".|"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) ; theorem :: QUATERNI:67 (Bool "for" (Set (Var "z")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k32_quaterni :::"|."::: ) (Set (Var "z")) ($#k32_quaterni :::".|"::: ) ))) ; theorem :: QUATERNI:68 (Bool (Set ($#k32_quaterni :::"|."::: ) (Set ($#k22_quaterni :::"1q"::: ) ) ($#k32_quaterni :::".|"::: ) ) ($#r1_hidden :::"="::: ) (Num 1)) ; theorem :: QUATERNI:69 (Bool (Set ($#k32_quaterni :::"|."::: ) (Set ($#k1_xcmplx_0 :::""::: ) ) ($#k32_quaterni :::".|"::: ) ) ($#r1_hidden :::"="::: ) (Num 1)) ; theorem :: QUATERNI:70 (Bool (Set ($#k32_quaterni :::"|."::: ) (Set ($#k11_quaterni :::""::: ) ) ($#k32_quaterni :::".|"::: ) ) ($#r1_hidden :::"="::: ) (Num 1)) ; theorem :: QUATERNI:71 (Bool (Set ($#k32_quaterni :::"|."::: ) (Set ($#k12_quaterni :::""::: ) ) ($#k32_quaterni :::".|"::: ) ) ($#r1_hidden :::"="::: ) (Num 1)) ; theorem :: QUATERNI:72 (Bool "for" (Set (Var "z")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k32_quaterni :::"|."::: ) (Set "(" ($#k28_quaterni :::"-"::: ) (Set (Var "z")) ")" ) ($#k32_quaterni :::".|"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k32_quaterni :::"|."::: ) (Set (Var "z")) ($#k32_quaterni :::".|"::: ) ))) ; theorem :: QUATERNI:73 (Bool "for" (Set (Var "z")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k32_quaterni :::"|."::: ) (Set "(" (Set (Var "z")) ($#k31_quaterni :::"*'"::: ) ")" ) ($#k32_quaterni :::".|"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k32_quaterni :::"|."::: ) (Set (Var "z")) ($#k32_quaterni :::".|"::: ) ))) ; theorem :: QUATERNI:74 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set "(" (Set "(" (Set "(" (Set (Var "a")) ($#k3_square_1 :::"^2"::: ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k3_square_1 :::"^2"::: ) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "c")) ($#k3_square_1 :::"^2"::: ) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "d")) ($#k3_square_1 :::"^2"::: ) ")" )) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) ))) ; theorem :: QUATERNI:75 (Bool "for" (Set (Var "z")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k17_quaterni :::"Rea"::: ) (Set (Var "z"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k32_quaterni :::"|."::: ) (Set (Var "z")) ($#k32_quaterni :::".|"::: ) ))) ; theorem :: QUATERNI:76 (Bool "for" (Set (Var "z")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k18_quaterni :::"Im1"::: ) (Set (Var "z"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k32_quaterni :::"|."::: ) (Set (Var "z")) ($#k32_quaterni :::".|"::: ) ))) ; theorem :: QUATERNI:77 (Bool "for" (Set (Var "z")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k19_quaterni :::"Im2"::: ) (Set (Var "z"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k32_quaterni :::"|."::: ) (Set (Var "z")) ($#k32_quaterni :::".|"::: ) ))) ; theorem :: QUATERNI:78 (Bool "for" (Set (Var "z")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k20_quaterni :::"Im3"::: ) (Set (Var "z"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k32_quaterni :::"|."::: ) (Set (Var "z")) ($#k32_quaterni :::".|"::: ) ))) ; theorem :: QUATERNI:79 (Bool "for" (Set (Var "z1")) "," (Set (Var "z2")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k32_quaterni :::"|."::: ) (Set "(" (Set (Var "z1")) ($#k26_quaterni :::"+"::: ) (Set (Var "z2")) ")" ) ($#k32_quaterni :::".|"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set ($#k32_quaterni :::"|."::: ) (Set (Var "z1")) ($#k32_quaterni :::".|"::: ) ) ($#k2_xcmplx_0 :::"+"::: ) (Set ($#k32_quaterni :::"|."::: ) (Set (Var "z2")) ($#k32_quaterni :::".|"::: ) )))) ; theorem :: QUATERNI:80 (Bool "for" (Set (Var "z1")) "," (Set (Var "z2")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k32_quaterni :::"|."::: ) (Set "(" (Set (Var "z1")) ($#k29_quaterni :::"-"::: ) (Set (Var "z2")) ")" ) ($#k32_quaterni :::".|"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set ($#k32_quaterni :::"|."::: ) (Set (Var "z1")) ($#k32_quaterni :::".|"::: ) ) ($#k2_xcmplx_0 :::"+"::: ) (Set ($#k32_quaterni :::"|."::: ) (Set (Var "z2")) ($#k32_quaterni :::".|"::: ) )))) ; theorem :: QUATERNI:81 (Bool "for" (Set (Var "z1")) "," (Set (Var "z2")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set ($#k32_quaterni :::"|."::: ) (Set (Var "z1")) ($#k32_quaterni :::".|"::: ) ) ($#k6_xcmplx_0 :::"-"::: ) (Set ($#k32_quaterni :::"|."::: ) (Set (Var "z2")) ($#k32_quaterni :::".|"::: ) )) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k32_quaterni :::"|."::: ) (Set "(" (Set (Var "z1")) ($#k26_quaterni :::"+"::: ) (Set (Var "z2")) ")" ) ($#k32_quaterni :::".|"::: ) ))) ; theorem :: QUATERNI:82 (Bool "for" (Set (Var "z1")) "," (Set (Var "z2")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set ($#k32_quaterni :::"|."::: ) (Set (Var "z1")) ($#k32_quaterni :::".|"::: ) ) ($#k6_xcmplx_0 :::"-"::: ) (Set ($#k32_quaterni :::"|."::: ) (Set (Var "z2")) ($#k32_quaterni :::".|"::: ) )) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k32_quaterni :::"|."::: ) (Set "(" (Set (Var "z1")) ($#k29_quaterni :::"-"::: ) (Set (Var "z2")) ")" ) ($#k32_quaterni :::".|"::: ) ))) ; theorem :: QUATERNI:83 (Bool "for" (Set (Var "z1")) "," (Set (Var "z2")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k32_quaterni :::"|."::: ) (Set "(" (Set (Var "z1")) ($#k29_quaterni :::"-"::: ) (Set (Var "z2")) ")" ) ($#k32_quaterni :::".|"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k32_quaterni :::"|."::: ) (Set "(" (Set (Var "z2")) ($#k29_quaterni :::"-"::: ) (Set (Var "z1")) ")" ) ($#k32_quaterni :::".|"::: ) ))) ; theorem :: QUATERNI:84 (Bool "for" (Set (Var "z1")) "," (Set (Var "z2")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set ($#k32_quaterni :::"|."::: ) (Set "(" (Set (Var "z1")) ($#k29_quaterni :::"-"::: ) (Set (Var "z2")) ")" ) ($#k32_quaterni :::".|"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) "iff" (Bool (Set (Var "z1")) ($#r1_hidden :::"="::: ) (Set (Var "z2"))) ")" )) ; theorem :: QUATERNI:85 (Bool "for" (Set (Var "z1")) "," (Set (Var "z2")) "," (Set (Var "z")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k32_quaterni :::"|."::: ) (Set "(" (Set (Var "z1")) ($#k29_quaterni :::"-"::: ) (Set (Var "z2")) ")" ) ($#k32_quaterni :::".|"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set ($#k32_quaterni :::"|."::: ) (Set "(" (Set (Var "z1")) ($#k29_quaterni :::"-"::: ) (Set (Var "z")) ")" ) ($#k32_quaterni :::".|"::: ) ) ($#k2_xcmplx_0 :::"+"::: ) (Set ($#k32_quaterni :::"|."::: ) (Set "(" (Set (Var "z")) ($#k29_quaterni :::"-"::: ) (Set (Var "z2")) ")" ) ($#k32_quaterni :::".|"::: ) )))) ; theorem :: QUATERNI:86 (Bool "for" (Set (Var "z1")) "," (Set (Var "z2")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k17_complex1 :::"|."::: ) (Set "(" (Set ($#k32_quaterni :::"|."::: ) (Set (Var "z1")) ($#k32_quaterni :::".|"::: ) ) ($#k6_xcmplx_0 :::"-"::: ) (Set ($#k32_quaterni :::"|."::: ) (Set (Var "z2")) ($#k32_quaterni :::".|"::: ) ) ")" ) ($#k17_complex1 :::".|"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k32_quaterni :::"|."::: ) (Set "(" (Set (Var "z1")) ($#k29_quaterni :::"-"::: ) (Set (Var "z2")) ")" ) ($#k32_quaterni :::".|"::: ) ))) ; theorem :: QUATERNI:87 (Bool "for" (Set (Var "z1")) "," (Set (Var "z2")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k32_quaterni :::"|."::: ) (Set "(" (Set (Var "z1")) ($#k27_quaterni :::"*"::: ) (Set (Var "z2")) ")" ) ($#k32_quaterni :::".|"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set ($#k32_quaterni :::"|."::: ) (Set (Var "z1")) ($#k32_quaterni :::".|"::: ) ) ($#k3_xcmplx_0 :::"*"::: ) (Set ($#k32_quaterni :::"|."::: ) (Set (Var "z2")) ($#k32_quaterni :::".|"::: ) )))) ; theorem :: QUATERNI:88 (Bool "for" (Set (Var "z")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k32_quaterni :::"|."::: ) (Set "(" (Set (Var "z")) ($#k27_quaterni :::"*"::: ) (Set (Var "z")) ")" ) ($#k32_quaterni :::".|"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set "(" ($#k17_quaterni :::"Rea"::: ) (Set (Var "z")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" ($#k18_quaterni :::"Im1"::: ) (Set (Var "z")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" ($#k19_quaterni :::"Im2"::: ) (Set (Var "z")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" ($#k20_quaterni :::"Im3"::: ) (Set (Var "z")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" )))) ; theorem :: QUATERNI:89 (Bool "for" (Set (Var "z")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k32_quaterni :::"|."::: ) (Set "(" (Set (Var "z")) ($#k27_quaterni :::"*"::: ) (Set (Var "z")) ")" ) ($#k32_quaterni :::".|"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k32_quaterni :::"|."::: ) (Set "(" (Set (Var "z")) ($#k27_quaterni :::"*"::: ) (Set "(" (Set (Var "z")) ($#k31_quaterni :::"*'"::: ) ")" ) ")" ) ($#k32_quaterni :::".|"::: ) ))) ; theorem :: QUATERNI:90 (Bool "for" (Set (Var "z")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "z")) "is" ($#v1_xreal_0 :::"real"::: ) )) "holds" (Bool "(" (Bool (Set ($#k17_quaterni :::"Rea"::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set (Var "z"))) & (Bool (Set ($#k18_quaterni :::"Im1"::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k19_quaterni :::"Im2"::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k20_quaterni :::"Im3"::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )) ; theorem :: QUATERNI:91 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set ($#k6_quaterni :::"[*"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k6_quaterni :::"*]"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k5_arytm_0 :::"[*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k5_arytm_0 :::"*]"::: ) ))) ; theorem :: QUATERNI:92 (Bool "for" (Set (Var "z1")) "," (Set (Var "z2")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "z1")) ($#k26_quaterni :::"+"::: ) (Set (Var "z2"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set "(" ($#k17_quaterni :::"Rea"::: ) (Set (Var "z1")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k17_quaterni :::"Rea"::: ) (Set (Var "z2")) ")" ) ")" ) ($#k23_quaterni :::"+"::: ) (Set "(" (Set "(" (Set "(" ($#k18_quaterni :::"Im1"::: ) (Set (Var "z1")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k18_quaterni :::"Im1"::: ) (Set (Var "z2")) ")" ) ")" ) ($#k25_quaterni :::"*"::: ) (Set ($#k1_xcmplx_0 :::""::: ) ) ")" ) ")" ) ($#k26_quaterni :::"+"::: ) (Set "(" (Set "(" (Set "(" ($#k19_quaterni :::"Im2"::: ) (Set (Var "z1")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k19_quaterni :::"Im2"::: ) (Set (Var "z2")) ")" ) ")" ) ($#k25_quaterni :::"*"::: ) (Set ($#k11_quaterni :::""::: ) ) ")" ) ")" ) ($#k26_quaterni :::"+"::: ) (Set "(" (Set "(" (Set "(" ($#k20_quaterni :::"Im3"::: ) (Set (Var "z1")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k20_quaterni :::"Im3"::: ) (Set (Var "z2")) ")" ) ")" ) ($#k25_quaterni :::"*"::: ) (Set ($#k12_quaterni :::""::: ) ) ")" )))) ; theorem :: QUATERNI:93 (Bool "for" (Set (Var "z1")) "," (Set (Var "z2")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "z1")) ($#k27_quaterni :::"*"::: ) (Set (Var "z2"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" ($#k17_quaterni :::"Rea"::: ) (Set (Var "z1")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k17_quaterni :::"Rea"::: ) (Set (Var "z2")) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" ($#k18_quaterni :::"Im1"::: ) (Set (Var "z1")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k18_quaterni :::"Im1"::: ) (Set (Var "z2")) ")" ) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" ($#k19_quaterni :::"Im2"::: ) (Set (Var "z1")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k19_quaterni :::"Im2"::: ) (Set (Var "z2")) ")" ) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" ($#k20_quaterni :::"Im3"::: ) (Set (Var "z1")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k20_quaterni :::"Im3"::: ) (Set (Var "z2")) ")" ) ")" ) ")" ) ($#k23_quaterni :::"+"::: ) (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" ($#k17_quaterni :::"Rea"::: ) (Set (Var "z1")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k18_quaterni :::"Im1"::: ) (Set (Var "z2")) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" ($#k18_quaterni :::"Im1"::: ) (Set (Var "z1")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k17_quaterni :::"Rea"::: ) (Set (Var "z2")) ")" ) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" ($#k19_quaterni :::"Im2"::: ) (Set (Var "z1")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k20_quaterni :::"Im3"::: ) (Set (Var "z2")) ")" ) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" ($#k20_quaterni :::"Im3"::: ) (Set (Var "z1")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k19_quaterni :::"Im2"::: ) (Set (Var "z2")) ")" ) ")" ) ")" ) ($#k25_quaterni :::"*"::: ) (Set ($#k1_xcmplx_0 :::""::: ) ) ")" ) ")" ) ($#k26_quaterni :::"+"::: ) (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" ($#k17_quaterni :::"Rea"::: ) (Set (Var "z1")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k19_quaterni :::"Im2"::: ) (Set (Var "z2")) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" ($#k19_quaterni :::"Im2"::: ) (Set (Var "z1")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k17_quaterni :::"Rea"::: ) (Set (Var "z2")) ")" ) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" ($#k20_quaterni :::"Im3"::: ) (Set (Var "z1")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k18_quaterni :::"Im1"::: ) (Set (Var "z2")) ")" ) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" ($#k18_quaterni :::"Im1"::: ) (Set (Var "z1")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k20_quaterni :::"Im3"::: ) (Set (Var "z2")) ")" ) ")" ) ")" ) ($#k25_quaterni :::"*"::: ) (Set ($#k11_quaterni :::""::: ) ) ")" ) ")" ) ($#k26_quaterni :::"+"::: ) (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" ($#k17_quaterni :::"Rea"::: ) (Set (Var "z1")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k20_quaterni :::"Im3"::: ) (Set (Var "z2")) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" ($#k20_quaterni :::"Im3"::: ) (Set (Var "z1")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k17_quaterni :::"Rea"::: ) (Set (Var "z2")) ")" ) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" ($#k18_quaterni :::"Im1"::: ) (Set (Var "z1")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k19_quaterni :::"Im2"::: ) (Set (Var "z2")) ")" ) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" ($#k19_quaterni :::"Im2"::: ) (Set (Var "z1")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k18_quaterni :::"Im1"::: ) (Set (Var "z2")) ")" ) ")" ) ")" ) ($#k25_quaterni :::"*"::: ) (Set ($#k12_quaterni :::""::: ) ) ")" )))) ; theorem :: QUATERNI:94 (Bool "for" (Set (Var "z")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k28_quaterni :::"-"::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" ($#k17_quaterni :::"Rea"::: ) (Set (Var "z")) ")" ) ")" ) ($#k23_quaterni :::"+"::: ) (Set "(" (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" ($#k18_quaterni :::"Im1"::: ) (Set (Var "z")) ")" ) ")" ) ($#k25_quaterni :::"*"::: ) (Set ($#k1_xcmplx_0 :::""::: ) ) ")" ) ")" ) ($#k26_quaterni :::"+"::: ) (Set "(" (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" ($#k19_quaterni :::"Im2"::: ) (Set (Var "z")) ")" ) ")" ) ($#k25_quaterni :::"*"::: ) (Set ($#k11_quaterni :::""::: ) ) ")" ) ")" ) ($#k26_quaterni :::"+"::: ) (Set "(" (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" ($#k20_quaterni :::"Im3"::: ) (Set (Var "z")) ")" ) ")" ) ($#k25_quaterni :::"*"::: ) (Set ($#k12_quaterni :::""::: ) ) ")" )))) ; theorem :: QUATERNI:95 (Bool "for" (Set (Var "z1")) "," (Set (Var "z2")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "z1")) ($#k29_quaterni :::"-"::: ) (Set (Var "z2"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set "(" ($#k17_quaterni :::"Rea"::: ) (Set (Var "z1")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" ($#k17_quaterni :::"Rea"::: ) (Set (Var "z2")) ")" ) ")" ) ($#k23_quaterni :::"+"::: ) (Set "(" (Set "(" (Set "(" ($#k18_quaterni :::"Im1"::: ) (Set (Var "z1")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" ($#k18_quaterni :::"Im1"::: ) (Set (Var "z2")) ")" ) ")" ) ($#k25_quaterni :::"*"::: ) (Set ($#k1_xcmplx_0 :::""::: ) ) ")" ) ")" ) ($#k26_quaterni :::"+"::: ) (Set "(" (Set "(" (Set "(" ($#k19_quaterni :::"Im2"::: ) (Set (Var "z1")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" ($#k19_quaterni :::"Im2"::: ) (Set (Var "z2")) ")" ) ")" ) ($#k25_quaterni :::"*"::: ) (Set ($#k11_quaterni :::""::: ) ) ")" ) ")" ) ($#k26_quaterni :::"+"::: ) (Set "(" (Set "(" (Set "(" ($#k20_quaterni :::"Im3"::: ) (Set (Var "z1")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" ($#k20_quaterni :::"Im3"::: ) (Set (Var "z2")) ")" ) ")" ) ($#k25_quaterni :::"*"::: ) (Set ($#k12_quaterni :::""::: ) ) ")" )))) ; theorem :: QUATERNI:96 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Set "(" (Set "(" (Set "(" (Set (Var "a")) ($#k3_square_1 :::"^2"::: ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k3_square_1 :::"^2"::: ) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "c")) ($#k3_square_1 :::"^2"::: ) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "d")) ($#k3_square_1 :::"^2"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "c")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "d")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )) ; theorem :: QUATERNI:97 (Bool "for" (Set (Var "z1")) "," (Set (Var "z2")) "being" ($#v1_quaterni :::"quaternion"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set ($#k17_quaterni :::"Rea"::: ) (Set "(" (Set (Var "z1")) ($#k27_quaterni :::"*"::: ) (Set (Var "z2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set "(" ($#k17_quaterni :::"Rea"::: ) (Set (Var "z1")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k17_quaterni :::"Rea"::: ) (Set (Var "z2")) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" ($#k18_quaterni :::"Im1"::: ) (Set (Var "z1")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k18_quaterni :::"Im1"::: ) (Set (Var "z2")) ")" ) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" ($#k19_quaterni :::"Im2"::: ) (Set (Var "z1")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k19_quaterni :::"Im2"::: ) (Set (Var "z2")) ")" ) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" ($#k20_quaterni :::"Im3"::: ) (Set (Var "z1")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k20_quaterni :::"Im3"::: ) (Set (Var "z2")) ")" ) ")" ))) & (Bool (Set ($#k18_quaterni :::"Im1"::: ) (Set "(" (Set (Var "z1")) ($#k27_quaterni :::"*"::: ) (Set (Var "z2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set "(" ($#k17_quaterni :::"Rea"::: ) (Set (Var "z1")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k18_quaterni :::"Im1"::: ) (Set (Var "z2")) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" ($#k18_quaterni :::"Im1"::: ) (Set (Var "z1")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k17_quaterni :::"Rea"::: ) (Set (Var "z2")) ")" ) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" ($#k19_quaterni :::"Im2"::: ) (Set (Var "z1")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k20_quaterni :::"Im3"::: ) (Set (Var "z2")) ")" ) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" ($#k20_quaterni :::"Im3"::: ) (Set (Var "z1")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k19_quaterni :::"Im2"::: ) (Set (Var "z2")) ")" ) ")" ))) & (Bool (Set ($#k19_quaterni :::"Im2"::: ) (Set "(" (Set (Var "z1")) ($#k27_quaterni :::"*"::: ) (Set (Var "z2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set "(" ($#k17_quaterni :::"Rea"::: ) (Set (Var "z1")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k19_quaterni :::"Im2"::: ) (Set (Var "z2")) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" ($#k19_quaterni :::"Im2"::: ) (Set (Var "z1")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k17_quaterni :::"Rea"::: ) (Set (Var "z2")) ")" ) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" ($#k20_quaterni :::"Im3"::: ) (Set (Var "z1")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k18_quaterni :::"Im1"::: ) (Set (Var "z2")) ")" ) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" ($#k18_quaterni :::"Im1"::: ) (Set (Var "z1")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k20_quaterni :::"Im3"::: ) (Set (Var "z2")) ")" ) ")" ))) & (Bool (Set ($#k20_quaterni :::"Im3"::: ) (Set "(" (Set (Var "z1")) ($#k27_quaterni :::"*"::: ) (Set (Var "z2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set "(" ($#k17_quaterni :::"Rea"::: ) (Set (Var "z1")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k20_quaterni :::"Im3"::: ) (Set (Var "z2")) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" ($#k20_quaterni :::"Im3"::: ) (Set (Var "z1")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k17_quaterni :::"Rea"::: ) (Set (Var "z2")) ")" ) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" ($#k18_quaterni :::"Im1"::: ) (Set (Var "z1")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k19_quaterni :::"Im2"::: ) (Set (Var "z2")) ")" ) ")" ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set "(" ($#k19_quaterni :::"Im2"::: ) (Set (Var "z1")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k18_quaterni :::"Im1"::: ) (Set (Var "z2")) ")" ) ")" ))) ")" )) ;