:: COMPLFLD semantic presentation begin definitionfunc :::"F_Complex"::: -> ($#v36_algstr_0 :::"strict"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) means :: COMPLFLD:def 1 (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set ($#k2_numbers :::"COMPLEX"::: ) )) & (Bool (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set ($#k27_binop_2 :::"addcomplex"::: ) )) & (Bool (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set ($#k29_binop_2 :::"multcomplex"::: ) )) & (Bool (Set ($#k5_struct_0 :::"1."::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k6_complex1 :::"1r"::: ) )) & (Bool (Set ($#k4_struct_0 :::"0."::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k5_complex1 :::"0c"::: ) )) ")" ); end; :: deftheorem defines :::"F_Complex"::: COMPLFLD:def 1 : (Bool "for" (Set (Var "b1")) "being" ($#v36_algstr_0 :::"strict"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k1_complfld :::"F_Complex"::: ) )) "iff" (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b1"))) ($#r1_hidden :::"="::: ) (Set ($#k2_numbers :::"COMPLEX"::: ) )) & (Bool (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" (Set (Var "b1"))) ($#r1_hidden :::"="::: ) (Set ($#k27_binop_2 :::"addcomplex"::: ) )) & (Bool (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "b1"))) ($#r1_hidden :::"="::: ) (Set ($#k29_binop_2 :::"multcomplex"::: ) )) & (Bool (Set ($#k5_struct_0 :::"1."::: ) (Set (Var "b1"))) ($#r1_hidden :::"="::: ) (Set ($#k6_complex1 :::"1r"::: ) )) & (Bool (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "b1"))) ($#r1_hidden :::"="::: ) (Set ($#k5_complex1 :::"0c"::: ) )) ")" ) ")" )); registration cluster (Set ($#k1_complfld :::"F_Complex"::: ) ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v36_algstr_0 :::"strict"::: ) ; end; registration cluster -> ($#v1_xcmplx_0 :::"complex"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set ($#k1_complfld :::"F_Complex"::: ) )); end; registrationlet "a", "b" be ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) ; let "x", "y" be ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ); identify ; identify ; end; registration cluster (Set ($#k1_complfld :::"F_Complex"::: ) ) -> ($#v36_algstr_0 :::"strict"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ; end; registration cluster (Set ($#k1_complfld :::"F_Complex"::: ) ) -> ($#~v6_struct_0 "non" ($#v6_struct_0 :::"degenerated"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v33_algstr_0 :::"almost_left_invertible"::: ) ($#v36_algstr_0 :::"strict"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v3_vectsp_1 :::"right_unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v6_vectsp_1 :::"left_unital"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ; end; theorem :: COMPLFLD:1 (Bool "for" (Set (Var "x1")) "," (Set (Var "y1")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) (Bool "for" (Set (Var "x2")) "," (Set (Var "y2")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "x1")) ($#r1_hidden :::"="::: ) (Set (Var "x2"))) & (Bool (Set (Var "y1")) ($#r1_hidden :::"="::: ) (Set (Var "y2")))) "holds" (Bool (Set (Set (Var "x1")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "y1"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "x2")) ($#k3_binop_2 :::"+"::: ) (Set (Var "y2")))))) ; theorem :: COMPLFLD:2 (Bool "for" (Set (Var "x1")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) (Bool "for" (Set (Var "x2")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "x1")) ($#r1_hidden :::"="::: ) (Set (Var "x2")))) "holds" (Bool (Set ($#k4_algstr_0 :::"-"::: ) (Set (Var "x1"))) ($#r1_hidden :::"="::: ) (Set ($#k1_binop_2 :::"-"::: ) (Set (Var "x2")))))) ; theorem :: COMPLFLD:3 (Bool "for" (Set (Var "x1")) "," (Set (Var "y1")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) (Bool "for" (Set (Var "x2")) "," (Set (Var "y2")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "x1")) ($#r1_hidden :::"="::: ) (Set (Var "x2"))) & (Bool (Set (Var "y1")) ($#r1_hidden :::"="::: ) (Set (Var "y2")))) "holds" (Bool (Set (Set (Var "x1")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "y1"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "x2")) ($#k4_binop_2 :::"-"::: ) (Set (Var "y2")))))) ; theorem :: COMPLFLD:4 (Bool "for" (Set (Var "x1")) "," (Set (Var "y1")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) (Bool "for" (Set (Var "x2")) "," (Set (Var "y2")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "x1")) ($#r1_hidden :::"="::: ) (Set (Var "x2"))) & (Bool (Set (Var "y1")) ($#r1_hidden :::"="::: ) (Set (Var "y2")))) "holds" (Bool (Set (Set (Var "x1")) ($#k8_group_1 :::"*"::: ) (Set (Var "y1"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "x2")) ($#k5_binop_2 :::"*"::: ) (Set (Var "y2")))))) ; theorem :: COMPLFLD:5 (Bool "for" (Set (Var "x1")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) (Bool "for" (Set (Var "x2")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "x1")) ($#r1_hidden :::"="::: ) (Set (Var "x2"))) & (Bool (Set (Var "x1")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set ($#k1_complfld :::"F_Complex"::: ) )))) "holds" (Bool (Set (Set (Var "x1")) ($#k11_algstr_0 :::"""::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "x2")) ($#k2_binop_2 :::"""::: ) )))) ; theorem :: COMPLFLD:6 (Bool "for" (Set (Var "x1")) "," (Set (Var "y1")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) (Bool "for" (Set (Var "x2")) "," (Set (Var "y2")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "x1")) ($#r1_hidden :::"="::: ) (Set (Var "x2"))) & (Bool (Set (Var "y1")) ($#r1_hidden :::"="::: ) (Set (Var "y2"))) & (Bool (Set (Var "y1")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set ($#k1_complfld :::"F_Complex"::: ) )))) "holds" (Bool (Set (Set (Var "x1")) ($#k3_vectsp_1 :::"/"::: ) (Set (Var "y1"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "x2")) ($#k6_binop_2 :::"/"::: ) (Set (Var "y2")))))) ; theorem :: COMPLFLD:7 (Bool (Set ($#k4_struct_0 :::"0."::: ) (Set ($#k1_complfld :::"F_Complex"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k5_complex1 :::"0c"::: ) )) ; theorem :: COMPLFLD:8 (Bool (Set ($#k1_group_1 :::"1_"::: ) (Set ($#k1_complfld :::"F_Complex"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_complex1 :::"1r"::: ) )) ; theorem :: COMPLFLD:9 (Bool (Set (Set "(" ($#k1_group_1 :::"1_"::: ) (Set ($#k1_complfld :::"F_Complex"::: ) ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" ($#k1_group_1 :::"1_"::: ) (Set ($#k1_complfld :::"F_Complex"::: ) ) ")" )) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set ($#k1_complfld :::"F_Complex"::: ) ))) ; definitionlet "z" be ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ); :: original: :::"*'"::: redefine func "z" :::"*'"::: -> ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ); end; theorem :: COMPLFLD:10 (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) "holds" (Bool (Set ($#k4_algstr_0 :::"-"::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set "(" ($#k1_group_1 :::"1_"::: ) (Set ($#k1_complfld :::"F_Complex"::: ) ) ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set (Var "z"))))) ; theorem :: COMPLFLD:11 (Bool "for" (Set (Var "z1")) "," (Set (Var "z2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) "holds" (Bool (Set (Set (Var "z1")) ($#k5_algstr_0 :::"-"::: ) (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "z2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "z1")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "z2"))))) ; theorem :: COMPLFLD:12 (Bool "for" (Set (Var "z1")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) "holds" (Bool (Set (Var "z1")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "z1")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "z")) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set (Var "z"))))) ; theorem :: COMPLFLD:13 (Bool "for" (Set (Var "z1")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) "holds" (Bool (Set (Var "z1")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "z1")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "z")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "z"))))) ; theorem :: COMPLFLD:14 (Bool "for" (Set (Var "z1")) "," (Set (Var "z2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) "st" (Bool (Bool (Set (Var "z1")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set ($#k1_complfld :::"F_Complex"::: ) ))) & (Bool (Set (Var "z2")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set ($#k1_complfld :::"F_Complex"::: ) ))) & (Bool (Set (Set (Var "z1")) ($#k11_algstr_0 :::"""::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "z2")) ($#k11_algstr_0 :::"""::: ) ))) "holds" (Bool (Set (Var "z1")) ($#r1_hidden :::"="::: ) (Set (Var "z2")))) ; theorem :: COMPLFLD:15 (Bool "for" (Set (Var "z2")) "," (Set (Var "z1")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) "st" (Bool (Bool (Set (Var "z2")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set ($#k1_complfld :::"F_Complex"::: ) ))) & (Bool "(" (Bool (Set (Set (Var "z1")) ($#k8_group_1 :::"*"::: ) (Set (Var "z2"))) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) (Set ($#k1_complfld :::"F_Complex"::: ) ))) "or" (Bool (Set (Set (Var "z2")) ($#k8_group_1 :::"*"::: ) (Set (Var "z1"))) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) (Set ($#k1_complfld :::"F_Complex"::: ) ))) ")" )) "holds" (Bool (Set (Var "z1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "z2")) ($#k11_algstr_0 :::"""::: ) ))) ; theorem :: COMPLFLD:16 (Bool "for" (Set (Var "z2")) "," (Set (Var "z1")) "," (Set (Var "z3")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) "st" (Bool (Bool (Set (Var "z2")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set ($#k1_complfld :::"F_Complex"::: ) ))) & (Bool "(" (Bool (Set (Set (Var "z1")) ($#k8_group_1 :::"*"::: ) (Set (Var "z2"))) ($#r1_hidden :::"="::: ) (Set (Var "z3"))) "or" (Bool (Set (Set (Var "z2")) ($#k8_group_1 :::"*"::: ) (Set (Var "z1"))) ($#r1_hidden :::"="::: ) (Set (Var "z3"))) ")" )) "holds" (Bool "(" (Bool (Set (Var "z1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "z3")) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "z2")) ($#k11_algstr_0 :::"""::: ) ")" ))) & (Bool (Set (Var "z1")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "z2")) ($#k11_algstr_0 :::"""::: ) ")" ) ($#k8_group_1 :::"*"::: ) (Set (Var "z3")))) ")" )) ; theorem :: COMPLFLD:17 (Bool (Set (Set "(" ($#k5_struct_0 :::"1."::: ) (Set ($#k1_complfld :::"F_Complex"::: ) ) ")" ) ($#k11_algstr_0 :::"""::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) (Set ($#k1_complfld :::"F_Complex"::: ) ))) ; theorem :: COMPLFLD:18 (Bool "for" (Set (Var "z1")) "," (Set (Var "z2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) "st" (Bool (Bool (Set (Var "z1")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set ($#k1_complfld :::"F_Complex"::: ) ))) & (Bool (Set (Var "z2")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set ($#k1_complfld :::"F_Complex"::: ) )))) "holds" (Bool (Set (Set "(" (Set (Var "z1")) ($#k8_group_1 :::"*"::: ) (Set (Var "z2")) ")" ) ($#k11_algstr_0 :::"""::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "z1")) ($#k11_algstr_0 :::"""::: ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "z2")) ($#k11_algstr_0 :::"""::: ) ")" )))) ; theorem :: COMPLFLD:19 (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) "st" (Bool (Bool (Set (Var "z")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set ($#k1_complfld :::"F_Complex"::: ) )))) "holds" (Bool (Set (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "z")) ")" ) ($#k11_algstr_0 :::"""::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k4_algstr_0 :::"-"::: ) (Set "(" (Set (Var "z")) ($#k11_algstr_0 :::"""::: ) ")" )))) ; theorem :: COMPLFLD:20 (Bool "for" (Set (Var "z1")) "," (Set (Var "z2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) "st" (Bool (Bool (Set (Var "z1")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set ($#k1_complfld :::"F_Complex"::: ) ))) & (Bool (Set (Var "z2")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set ($#k1_complfld :::"F_Complex"::: ) )))) "holds" (Bool (Set (Set "(" (Set (Var "z1")) ($#k11_algstr_0 :::"""::: ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "z2")) ($#k11_algstr_0 :::"""::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "z1")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "z2")) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "z1")) ($#k8_group_1 :::"*"::: ) (Set (Var "z2")) ")" ) ($#k11_algstr_0 :::"""::: ) ")" )))) ; theorem :: COMPLFLD:21 (Bool "for" (Set (Var "z1")) "," (Set (Var "z2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) "st" (Bool (Bool (Set (Var "z1")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set ($#k1_complfld :::"F_Complex"::: ) ))) & (Bool (Set (Var "z2")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set ($#k1_complfld :::"F_Complex"::: ) )))) "holds" (Bool (Set (Set "(" (Set (Var "z1")) ($#k11_algstr_0 :::"""::: ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "z2")) ($#k11_algstr_0 :::"""::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "z2")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "z1")) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "z1")) ($#k8_group_1 :::"*"::: ) (Set (Var "z2")) ")" ) ($#k11_algstr_0 :::"""::: ) ")" )))) ; theorem :: COMPLFLD:22 (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) "st" (Bool (Bool (Set (Var "z")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set ($#k1_complfld :::"F_Complex"::: ) )))) "holds" (Bool (Set (Set (Var "z")) ($#k11_algstr_0 :::"""::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_struct_0 :::"1."::: ) (Set ($#k1_complfld :::"F_Complex"::: ) ) ")" ) ($#k3_vectsp_1 :::"/"::: ) (Set (Var "z"))))) ; theorem :: COMPLFLD:23 (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) "holds" (Bool (Set (Set (Var "z")) ($#k3_vectsp_1 :::"/"::: ) (Set "(" ($#k5_struct_0 :::"1."::: ) (Set ($#k1_complfld :::"F_Complex"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "z")))) ; theorem :: COMPLFLD:24 (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) "st" (Bool (Bool (Set (Var "z")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set ($#k1_complfld :::"F_Complex"::: ) )))) "holds" (Bool (Set (Set (Var "z")) ($#k3_vectsp_1 :::"/"::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) (Set ($#k1_complfld :::"F_Complex"::: ) )))) ; theorem :: COMPLFLD:25 (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) "st" (Bool (Bool (Set (Var "z")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set ($#k1_complfld :::"F_Complex"::: ) )))) "holds" (Bool (Set (Set "(" ($#k4_struct_0 :::"0."::: ) (Set ($#k1_complfld :::"F_Complex"::: ) ) ")" ) ($#k3_vectsp_1 :::"/"::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set ($#k1_complfld :::"F_Complex"::: ) )))) ; theorem :: COMPLFLD:26 (Bool "for" (Set (Var "z2")) "," (Set (Var "z1")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) "st" (Bool (Bool (Set (Var "z2")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set ($#k1_complfld :::"F_Complex"::: ) ))) & (Bool (Set (Set (Var "z1")) ($#k3_vectsp_1 :::"/"::: ) (Set (Var "z2"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set ($#k1_complfld :::"F_Complex"::: ) )))) "holds" (Bool (Set (Var "z1")) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set ($#k1_complfld :::"F_Complex"::: ) )))) ; theorem :: COMPLFLD:27 (Bool "for" (Set (Var "z2")) "," (Set (Var "z4")) "," (Set (Var "z1")) "," (Set (Var "z3")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) "st" (Bool (Bool (Set (Var "z2")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set ($#k1_complfld :::"F_Complex"::: ) ))) & (Bool (Set (Var "z4")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set ($#k1_complfld :::"F_Complex"::: ) )))) "holds" (Bool (Set (Set "(" (Set (Var "z1")) ($#k3_vectsp_1 :::"/"::: ) (Set (Var "z2")) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "z3")) ($#k3_vectsp_1 :::"/"::: ) (Set (Var "z4")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "z1")) ($#k8_group_1 :::"*"::: ) (Set (Var "z3")) ")" ) ($#k3_vectsp_1 :::"/"::: ) (Set "(" (Set (Var "z2")) ($#k8_group_1 :::"*"::: ) (Set (Var "z4")) ")" )))) ; theorem :: COMPLFLD:28 (Bool "for" (Set (Var "z2")) "," (Set (Var "z")) "," (Set (Var "z1")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) "st" (Bool (Bool (Set (Var "z2")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set ($#k1_complfld :::"F_Complex"::: ) )))) "holds" (Bool (Set (Set (Var "z")) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "z1")) ($#k3_vectsp_1 :::"/"::: ) (Set (Var "z2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "z")) ($#k8_group_1 :::"*"::: ) (Set (Var "z1")) ")" ) ($#k3_vectsp_1 :::"/"::: ) (Set (Var "z2"))))) ; theorem :: COMPLFLD:29 (Bool "for" (Set (Var "z2")) "," (Set (Var "z1")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) "st" (Bool (Bool (Set (Var "z2")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set ($#k1_complfld :::"F_Complex"::: ) ))) & (Bool (Set (Set (Var "z1")) ($#k3_vectsp_1 :::"/"::: ) (Set (Var "z2"))) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) (Set ($#k1_complfld :::"F_Complex"::: ) )))) "holds" (Bool (Set (Var "z1")) ($#r1_hidden :::"="::: ) (Set (Var "z2")))) ; theorem :: COMPLFLD:30 (Bool "for" (Set (Var "z")) "," (Set (Var "z1")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) "st" (Bool (Bool (Set (Var "z")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set ($#k1_complfld :::"F_Complex"::: ) )))) "holds" (Bool (Set (Var "z1")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "z1")) ($#k8_group_1 :::"*"::: ) (Set (Var "z")) ")" ) ($#k3_vectsp_1 :::"/"::: ) (Set (Var "z"))))) ; theorem :: COMPLFLD:31 (Bool "for" (Set (Var "z1")) "," (Set (Var "z2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) "st" (Bool (Bool (Set (Var "z1")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set ($#k1_complfld :::"F_Complex"::: ) ))) & (Bool (Set (Var "z2")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set ($#k1_complfld :::"F_Complex"::: ) )))) "holds" (Bool (Set (Set "(" (Set (Var "z1")) ($#k3_vectsp_1 :::"/"::: ) (Set (Var "z2")) ")" ) ($#k11_algstr_0 :::"""::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "z2")) ($#k3_vectsp_1 :::"/"::: ) (Set (Var "z1"))))) ; theorem :: COMPLFLD:32 (Bool "for" (Set (Var "z1")) "," (Set (Var "z2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) "st" (Bool (Bool (Set (Var "z1")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set ($#k1_complfld :::"F_Complex"::: ) ))) & (Bool (Set (Var "z2")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set ($#k1_complfld :::"F_Complex"::: ) )))) "holds" (Bool (Set (Set "(" (Set (Var "z1")) ($#k11_algstr_0 :::"""::: ) ")" ) ($#k3_vectsp_1 :::"/"::: ) (Set "(" (Set (Var "z2")) ($#k11_algstr_0 :::"""::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "z2")) ($#k3_vectsp_1 :::"/"::: ) (Set (Var "z1"))))) ; theorem :: COMPLFLD:33 (Bool "for" (Set (Var "z2")) "," (Set (Var "z1")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) "st" (Bool (Bool (Set (Var "z2")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set ($#k1_complfld :::"F_Complex"::: ) )))) "holds" (Bool (Set (Set (Var "z1")) ($#k3_vectsp_1 :::"/"::: ) (Set "(" (Set (Var "z2")) ($#k11_algstr_0 :::"""::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "z1")) ($#k8_group_1 :::"*"::: ) (Set (Var "z2"))))) ; theorem :: COMPLFLD:34 (Bool "for" (Set (Var "z1")) "," (Set (Var "z2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) "st" (Bool (Bool (Set (Var "z1")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set ($#k1_complfld :::"F_Complex"::: ) ))) & (Bool (Set (Var "z2")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set ($#k1_complfld :::"F_Complex"::: ) )))) "holds" (Bool (Set (Set "(" (Set (Var "z1")) ($#k11_algstr_0 :::"""::: ) ")" ) ($#k3_vectsp_1 :::"/"::: ) (Set (Var "z2"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "z1")) ($#k8_group_1 :::"*"::: ) (Set (Var "z2")) ")" ) ($#k11_algstr_0 :::"""::: ) ))) ; theorem :: COMPLFLD:35 (Bool "for" (Set (Var "z1")) "," (Set (Var "z2")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) "st" (Bool (Bool (Set (Var "z1")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set ($#k1_complfld :::"F_Complex"::: ) ))) & (Bool (Set (Var "z2")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set ($#k1_complfld :::"F_Complex"::: ) )))) "holds" (Bool (Set (Set "(" (Set (Var "z1")) ($#k11_algstr_0 :::"""::: ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "z")) ($#k3_vectsp_1 :::"/"::: ) (Set (Var "z2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "z")) ($#k3_vectsp_1 :::"/"::: ) (Set "(" (Set (Var "z1")) ($#k8_group_1 :::"*"::: ) (Set (Var "z2")) ")" )))) ; theorem :: COMPLFLD:36 (Bool "for" (Set (Var "z")) "," (Set (Var "z2")) "," (Set (Var "z1")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) "st" (Bool (Bool (Set (Var "z")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set ($#k1_complfld :::"F_Complex"::: ) ))) & (Bool (Set (Var "z2")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set ($#k1_complfld :::"F_Complex"::: ) )))) "holds" (Bool "(" (Bool (Set (Set (Var "z1")) ($#k3_vectsp_1 :::"/"::: ) (Set (Var "z2"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "z1")) ($#k8_group_1 :::"*"::: ) (Set (Var "z")) ")" ) ($#k3_vectsp_1 :::"/"::: ) (Set "(" (Set (Var "z2")) ($#k8_group_1 :::"*"::: ) (Set (Var "z")) ")" ))) & (Bool (Set (Set (Var "z1")) ($#k3_vectsp_1 :::"/"::: ) (Set (Var "z2"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "z")) ($#k8_group_1 :::"*"::: ) (Set (Var "z1")) ")" ) ($#k3_vectsp_1 :::"/"::: ) (Set "(" (Set (Var "z")) ($#k8_group_1 :::"*"::: ) (Set (Var "z2")) ")" ))) ")" )) ; theorem :: COMPLFLD:37 (Bool "for" (Set (Var "z2")) "," (Set (Var "z3")) "," (Set (Var "z1")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) "st" (Bool (Bool (Set (Var "z2")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set ($#k1_complfld :::"F_Complex"::: ) ))) & (Bool (Set (Var "z3")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set ($#k1_complfld :::"F_Complex"::: ) )))) "holds" (Bool (Set (Set (Var "z1")) ($#k3_vectsp_1 :::"/"::: ) (Set "(" (Set (Var "z2")) ($#k8_group_1 :::"*"::: ) (Set (Var "z3")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "z1")) ($#k3_vectsp_1 :::"/"::: ) (Set (Var "z2")) ")" ) ($#k3_vectsp_1 :::"/"::: ) (Set (Var "z3"))))) ; theorem :: COMPLFLD:38 (Bool "for" (Set (Var "z2")) "," (Set (Var "z3")) "," (Set (Var "z1")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) "st" (Bool (Bool (Set (Var "z2")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set ($#k1_complfld :::"F_Complex"::: ) ))) & (Bool (Set (Var "z3")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set ($#k1_complfld :::"F_Complex"::: ) )))) "holds" (Bool (Set (Set "(" (Set (Var "z1")) ($#k8_group_1 :::"*"::: ) (Set (Var "z3")) ")" ) ($#k3_vectsp_1 :::"/"::: ) (Set (Var "z2"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "z1")) ($#k3_vectsp_1 :::"/"::: ) (Set "(" (Set (Var "z2")) ($#k3_vectsp_1 :::"/"::: ) (Set (Var "z3")) ")" )))) ; theorem :: COMPLFLD:39 (Bool "for" (Set (Var "z2")) "," (Set (Var "z3")) "," (Set (Var "z4")) "," (Set (Var "z1")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) "st" (Bool (Bool (Set (Var "z2")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set ($#k1_complfld :::"F_Complex"::: ) ))) & (Bool (Set (Var "z3")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set ($#k1_complfld :::"F_Complex"::: ) ))) & (Bool (Set (Var "z4")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set ($#k1_complfld :::"F_Complex"::: ) )))) "holds" (Bool (Set (Set "(" (Set (Var "z1")) ($#k3_vectsp_1 :::"/"::: ) (Set (Var "z2")) ")" ) ($#k3_vectsp_1 :::"/"::: ) (Set "(" (Set (Var "z3")) ($#k3_vectsp_1 :::"/"::: ) (Set (Var "z4")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "z1")) ($#k8_group_1 :::"*"::: ) (Set (Var "z4")) ")" ) ($#k3_vectsp_1 :::"/"::: ) (Set "(" (Set (Var "z2")) ($#k8_group_1 :::"*"::: ) (Set (Var "z3")) ")" )))) ; theorem :: COMPLFLD:40 (Bool "for" (Set (Var "z2")) "," (Set (Var "z4")) "," (Set (Var "z1")) "," (Set (Var "z3")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) "st" (Bool (Bool (Set (Var "z2")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set ($#k1_complfld :::"F_Complex"::: ) ))) & (Bool (Set (Var "z4")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set ($#k1_complfld :::"F_Complex"::: ) )))) "holds" (Bool (Set (Set "(" (Set (Var "z1")) ($#k3_vectsp_1 :::"/"::: ) (Set (Var "z2")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "z3")) ($#k3_vectsp_1 :::"/"::: ) (Set (Var "z4")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "z1")) ($#k8_group_1 :::"*"::: ) (Set (Var "z4")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "z3")) ($#k8_group_1 :::"*"::: ) (Set (Var "z2")) ")" ) ")" ) ($#k3_vectsp_1 :::"/"::: ) (Set "(" (Set (Var "z2")) ($#k8_group_1 :::"*"::: ) (Set (Var "z4")) ")" )))) ; theorem :: COMPLFLD:41 (Bool "for" (Set (Var "z")) "," (Set (Var "z1")) "," (Set (Var "z2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) "st" (Bool (Bool (Set (Var "z")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set ($#k1_complfld :::"F_Complex"::: ) )))) "holds" (Bool (Set (Set "(" (Set (Var "z1")) ($#k3_vectsp_1 :::"/"::: ) (Set (Var "z")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "z2")) ($#k3_vectsp_1 :::"/"::: ) (Set (Var "z")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "z1")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "z2")) ")" ) ($#k3_vectsp_1 :::"/"::: ) (Set (Var "z"))))) ; theorem :: COMPLFLD:42 (Bool "for" (Set (Var "z2")) "," (Set (Var "z1")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) "st" (Bool (Bool (Set (Var "z2")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set ($#k1_complfld :::"F_Complex"::: ) )))) "holds" (Bool "(" (Bool (Set ($#k4_algstr_0 :::"-"::: ) (Set "(" (Set (Var "z1")) ($#k3_vectsp_1 :::"/"::: ) (Set (Var "z2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "z1")) ")" ) ($#k3_vectsp_1 :::"/"::: ) (Set (Var "z2")))) & (Bool (Set ($#k4_algstr_0 :::"-"::: ) (Set "(" (Set (Var "z1")) ($#k3_vectsp_1 :::"/"::: ) (Set (Var "z2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "z1")) ($#k3_vectsp_1 :::"/"::: ) (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "z2")) ")" ))) ")" )) ; theorem :: COMPLFLD:43 (Bool "for" (Set (Var "z2")) "," (Set (Var "z1")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) "st" (Bool (Bool (Set (Var "z2")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set ($#k1_complfld :::"F_Complex"::: ) )))) "holds" (Bool (Set (Set (Var "z1")) ($#k3_vectsp_1 :::"/"::: ) (Set (Var "z2"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "z1")) ")" ) ($#k3_vectsp_1 :::"/"::: ) (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "z2")) ")" )))) ; theorem :: COMPLFLD:44 (Bool "for" (Set (Var "z2")) "," (Set (Var "z4")) "," (Set (Var "z1")) "," (Set (Var "z3")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) "st" (Bool (Bool (Set (Var "z2")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set ($#k1_complfld :::"F_Complex"::: ) ))) & (Bool (Set (Var "z4")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set ($#k1_complfld :::"F_Complex"::: ) )))) "holds" (Bool (Set (Set "(" (Set (Var "z1")) ($#k3_vectsp_1 :::"/"::: ) (Set (Var "z2")) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "z3")) ($#k3_vectsp_1 :::"/"::: ) (Set (Var "z4")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "z1")) ($#k8_group_1 :::"*"::: ) (Set (Var "z4")) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "z3")) ($#k8_group_1 :::"*"::: ) (Set (Var "z2")) ")" ) ")" ) ($#k3_vectsp_1 :::"/"::: ) (Set "(" (Set (Var "z2")) ($#k8_group_1 :::"*"::: ) (Set (Var "z4")) ")" )))) ; theorem :: COMPLFLD:45 (Bool "for" (Set (Var "z")) "," (Set (Var "z1")) "," (Set (Var "z2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) "st" (Bool (Bool (Set (Var "z")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set ($#k1_complfld :::"F_Complex"::: ) )))) "holds" (Bool (Set (Set "(" (Set (Var "z1")) ($#k3_vectsp_1 :::"/"::: ) (Set (Var "z")) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "z2")) ($#k3_vectsp_1 :::"/"::: ) (Set (Var "z")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "z1")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "z2")) ")" ) ($#k3_vectsp_1 :::"/"::: ) (Set (Var "z"))))) ; theorem :: COMPLFLD:46 (Bool "for" (Set (Var "z2")) "," (Set (Var "z1")) "," (Set (Var "z3")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) "st" (Bool (Bool (Set (Var "z2")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set ($#k1_complfld :::"F_Complex"::: ) ))) & (Bool "(" (Bool (Set (Set (Var "z1")) ($#k8_group_1 :::"*"::: ) (Set (Var "z2"))) ($#r1_hidden :::"="::: ) (Set (Var "z3"))) "or" (Bool (Set (Set (Var "z2")) ($#k8_group_1 :::"*"::: ) (Set (Var "z1"))) ($#r1_hidden :::"="::: ) (Set (Var "z3"))) ")" )) "holds" (Bool (Set (Var "z1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "z3")) ($#k3_vectsp_1 :::"/"::: ) (Set (Var "z2"))))) ; theorem :: COMPLFLD:47 (Bool (Set (Set "(" ($#k4_struct_0 :::"0."::: ) (Set ($#k1_complfld :::"F_Complex"::: ) ) ")" ) ($#k2_complfld :::"*'"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set ($#k1_complfld :::"F_Complex"::: ) ))) ; theorem :: COMPLFLD:48 (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) "st" (Bool (Bool (Set (Set (Var "z")) ($#k2_complfld :::"*'"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set ($#k1_complfld :::"F_Complex"::: ) )))) "holds" (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set ($#k1_complfld :::"F_Complex"::: ) )))) ; theorem :: COMPLFLD:49 (Bool (Set (Set "(" ($#k5_struct_0 :::"1."::: ) (Set ($#k1_complfld :::"F_Complex"::: ) ) ")" ) ($#k2_complfld :::"*'"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) (Set ($#k1_complfld :::"F_Complex"::: ) ))) ; theorem :: COMPLFLD:50 (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) "holds" (Bool (Set (Set "(" (Set (Var "z")) ($#k2_complfld :::"*'"::: ) ")" ) ($#k2_complfld :::"*'"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "z")))) ; theorem :: COMPLFLD:51 (Bool "for" (Set (Var "z1")) "," (Set (Var "z2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) "holds" (Bool (Set (Set "(" (Set (Var "z1")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "z2")) ")" ) ($#k2_complfld :::"*'"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "z1")) ($#k2_complfld :::"*'"::: ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "z2")) ($#k2_complfld :::"*'"::: ) ")" )))) ; theorem :: COMPLFLD:52 (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) "holds" (Bool (Set (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "z")) ")" ) ($#k2_complfld :::"*'"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k4_algstr_0 :::"-"::: ) (Set "(" (Set (Var "z")) ($#k2_complfld :::"*'"::: ) ")" )))) ; theorem :: COMPLFLD:53 (Bool "for" (Set (Var "z1")) "," (Set (Var "z2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) "holds" (Bool (Set (Set "(" (Set (Var "z1")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "z2")) ")" ) ($#k2_complfld :::"*'"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "z1")) ($#k2_complfld :::"*'"::: ) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "z2")) ($#k2_complfld :::"*'"::: ) ")" )))) ; theorem :: COMPLFLD:54 (Bool "for" (Set (Var "z1")) "," (Set (Var "z2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) "holds" (Bool (Set (Set "(" (Set (Var "z1")) ($#k8_group_1 :::"*"::: ) (Set (Var "z2")) ")" ) ($#k2_complfld :::"*'"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "z1")) ($#k2_complfld :::"*'"::: ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "z2")) ($#k2_complfld :::"*'"::: ) ")" )))) ; theorem :: COMPLFLD:55 (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) "st" (Bool (Bool (Set (Var "z")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set ($#k1_complfld :::"F_Complex"::: ) )))) "holds" (Bool (Set (Set "(" (Set (Var "z")) ($#k11_algstr_0 :::"""::: ) ")" ) ($#k2_complfld :::"*'"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "z")) ($#k2_complfld :::"*'"::: ) ")" ) ($#k11_algstr_0 :::"""::: ) ))) ; theorem :: COMPLFLD:56 (Bool "for" (Set (Var "z2")) "," (Set (Var "z1")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) "st" (Bool (Bool (Set (Var "z2")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set ($#k1_complfld :::"F_Complex"::: ) )))) "holds" (Bool (Set (Set "(" (Set (Var "z1")) ($#k3_vectsp_1 :::"/"::: ) (Set (Var "z2")) ")" ) ($#k2_complfld :::"*'"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "z1")) ($#k2_complfld :::"*'"::: ) ")" ) ($#k3_vectsp_1 :::"/"::: ) (Set "(" (Set (Var "z2")) ($#k2_complfld :::"*'"::: ) ")" )))) ; theorem :: COMPLFLD:57 (Bool (Set ($#k17_complex1 :::"|."::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set ($#k1_complfld :::"F_Complex"::: ) ) ")" ) ($#k17_complex1 :::".|"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ; theorem :: COMPLFLD:58 (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) "st" (Bool (Bool (Set ($#k17_complex1 :::"|."::: ) (Set (Var "z")) ($#k17_complex1 :::".|"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set ($#k1_complfld :::"F_Complex"::: ) )))) ; theorem :: COMPLFLD:59 (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) "holds" (Bool "(" (Bool (Set (Var "z")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set ($#k1_complfld :::"F_Complex"::: ) ))) "iff" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k17_complex1 :::"|."::: ) (Set (Var "z")) ($#k17_complex1 :::".|"::: ) )) ")" )) ; theorem :: COMPLFLD:60 (Bool (Set ($#k17_complex1 :::"|."::: ) (Set "(" ($#k5_struct_0 :::"1."::: ) (Set ($#k1_complfld :::"F_Complex"::: ) ) ")" ) ($#k17_complex1 :::".|"::: ) ) ($#r1_hidden :::"="::: ) (Num 1)) ; theorem :: COMPLFLD:61 (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) "holds" (Bool (Set ($#k17_complex1 :::"|."::: ) (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "z")) ")" ) ($#k17_complex1 :::".|"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k17_complex1 :::"|."::: ) (Set (Var "z")) ($#k17_complex1 :::".|"::: ) ))) ; theorem :: COMPLFLD:62 (Bool "for" (Set (Var "z1")) "," (Set (Var "z2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) "holds" (Bool (Set ($#k17_complex1 :::"|."::: ) (Set "(" (Set (Var "z1")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "z2")) ")" ) ($#k17_complex1 :::".|"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set ($#k17_complex1 :::"|."::: ) (Set (Var "z1")) ($#k17_complex1 :::".|"::: ) ) ($#k9_binop_2 :::"+"::: ) (Set ($#k17_complex1 :::"|."::: ) (Set (Var "z2")) ($#k17_complex1 :::".|"::: ) )))) ; theorem :: COMPLFLD:63 (Bool "for" (Set (Var "z1")) "," (Set (Var "z2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) "holds" (Bool (Set ($#k17_complex1 :::"|."::: ) (Set "(" (Set (Var "z1")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "z2")) ")" ) ($#k17_complex1 :::".|"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set ($#k17_complex1 :::"|."::: ) (Set (Var "z1")) ($#k17_complex1 :::".|"::: ) ) ($#k9_binop_2 :::"+"::: ) (Set ($#k17_complex1 :::"|."::: ) (Set (Var "z2")) ($#k17_complex1 :::".|"::: ) )))) ; theorem :: COMPLFLD:64 (Bool "for" (Set (Var "z1")) "," (Set (Var "z2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) "holds" (Bool (Set (Set ($#k17_complex1 :::"|."::: ) (Set (Var "z1")) ($#k17_complex1 :::".|"::: ) ) ($#k10_binop_2 :::"-"::: ) (Set ($#k17_complex1 :::"|."::: ) (Set (Var "z2")) ($#k17_complex1 :::".|"::: ) )) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k17_complex1 :::"|."::: ) (Set "(" (Set (Var "z1")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "z2")) ")" ) ($#k17_complex1 :::".|"::: ) ))) ; theorem :: COMPLFLD:65 (Bool "for" (Set (Var "z1")) "," (Set (Var "z2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) "holds" (Bool (Set (Set ($#k17_complex1 :::"|."::: ) (Set (Var "z1")) ($#k17_complex1 :::".|"::: ) ) ($#k10_binop_2 :::"-"::: ) (Set ($#k17_complex1 :::"|."::: ) (Set (Var "z2")) ($#k17_complex1 :::".|"::: ) )) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k17_complex1 :::"|."::: ) (Set "(" (Set (Var "z1")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "z2")) ")" ) ($#k17_complex1 :::".|"::: ) ))) ; theorem :: COMPLFLD:66 (Bool "for" (Set (Var "z1")) "," (Set (Var "z2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) "holds" (Bool (Set ($#k17_complex1 :::"|."::: ) (Set "(" (Set (Var "z1")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "z2")) ")" ) ($#k17_complex1 :::".|"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k17_complex1 :::"|."::: ) (Set "(" (Set (Var "z2")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "z1")) ")" ) ($#k17_complex1 :::".|"::: ) ))) ; theorem :: COMPLFLD:67 (Bool "for" (Set (Var "z1")) "," (Set (Var "z2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) "holds" (Bool "(" (Bool (Set ($#k17_complex1 :::"|."::: ) (Set "(" (Set (Var "z1")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "z2")) ")" ) ($#k17_complex1 :::".|"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) "iff" (Bool (Set (Var "z1")) ($#r1_hidden :::"="::: ) (Set (Var "z2"))) ")" )) ; theorem :: COMPLFLD:68 (Bool "for" (Set (Var "z1")) "," (Set (Var "z2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) "holds" (Bool "(" (Bool (Set (Var "z1")) ($#r1_hidden :::"<>"::: ) (Set (Var "z2"))) "iff" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k17_complex1 :::"|."::: ) (Set "(" (Set (Var "z1")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "z2")) ")" ) ($#k17_complex1 :::".|"::: ) )) ")" )) ; theorem :: COMPLFLD:69 (Bool "for" (Set (Var "z1")) "," (Set (Var "z2")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) "holds" (Bool (Set ($#k17_complex1 :::"|."::: ) (Set "(" (Set (Var "z1")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "z2")) ")" ) ($#k17_complex1 :::".|"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set ($#k17_complex1 :::"|."::: ) (Set "(" (Set (Var "z1")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "z")) ")" ) ($#k17_complex1 :::".|"::: ) ) ($#k9_binop_2 :::"+"::: ) (Set ($#k17_complex1 :::"|."::: ) (Set "(" (Set (Var "z")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "z2")) ")" ) ($#k17_complex1 :::".|"::: ) )))) ; theorem :: COMPLFLD:70 (Bool "for" (Set (Var "z1")) "," (Set (Var "z2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) "holds" (Bool (Set ($#k18_complex1 :::"abs"::: ) (Set "(" (Set ($#k17_complex1 :::"|."::: ) (Set (Var "z1")) ($#k17_complex1 :::".|"::: ) ) ($#k10_binop_2 :::"-"::: ) (Set ($#k17_complex1 :::"|."::: ) (Set (Var "z2")) ($#k17_complex1 :::".|"::: ) ) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k17_complex1 :::"|."::: ) (Set "(" (Set (Var "z1")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "z2")) ")" ) ($#k17_complex1 :::".|"::: ) ))) ; theorem :: COMPLFLD:71 (Bool "for" (Set (Var "z1")) "," (Set (Var "z2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) "holds" (Bool (Set ($#k17_complex1 :::"|."::: ) (Set "(" (Set (Var "z1")) ($#k8_group_1 :::"*"::: ) (Set (Var "z2")) ")" ) ($#k17_complex1 :::".|"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set ($#k17_complex1 :::"|."::: ) (Set (Var "z1")) ($#k17_complex1 :::".|"::: ) ) ($#k11_binop_2 :::"*"::: ) (Set ($#k17_complex1 :::"|."::: ) (Set (Var "z2")) ($#k17_complex1 :::".|"::: ) )))) ; theorem :: COMPLFLD:72 (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) "st" (Bool (Bool (Set (Var "z")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set ($#k1_complfld :::"F_Complex"::: ) )))) "holds" (Bool (Set ($#k17_complex1 :::"|."::: ) (Set "(" (Set (Var "z")) ($#k11_algstr_0 :::"""::: ) ")" ) ($#k17_complex1 :::".|"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set ($#k17_complex1 :::"|."::: ) (Set (Var "z")) ($#k17_complex1 :::".|"::: ) ) ($#k8_binop_2 :::"""::: ) ))) ; theorem :: COMPLFLD:73 (Bool "for" (Set (Var "z2")) "," (Set (Var "z1")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) "st" (Bool (Bool (Set (Var "z2")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set ($#k1_complfld :::"F_Complex"::: ) )))) "holds" (Bool (Set (Set ($#k17_complex1 :::"|."::: ) (Set (Var "z1")) ($#k17_complex1 :::".|"::: ) ) ($#k12_binop_2 :::"/"::: ) (Set ($#k17_complex1 :::"|."::: ) (Set (Var "z2")) ($#k17_complex1 :::".|"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k17_complex1 :::"|."::: ) (Set "(" (Set (Var "z1")) ($#k3_vectsp_1 :::"/"::: ) (Set (Var "z2")) ")" ) ($#k17_complex1 :::".|"::: ) ))) ; begin scheme :: COMPLFLD:sch 1 Regrwithout0{ P1[ ($#m1_hidden :::"Nat":::)] } : (Bool P1[(Num 1)]) provided (Bool "ex" (Set (Var "k")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool P1[(Set (Var "k"))])) and (Bool "for" (Set (Var "k")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "k")) ($#r1_hidden :::"<>"::: ) (Num 1)) & (Bool P1[(Set (Var "k"))])) "holds" (Bool "ex" (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "k"))) & (Bool P1[(Set (Var "n"))]) ")" ))) proof end; theorem :: COMPLFLD:74 (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) (Bool "for" (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set "(" ($#k4_group_1 :::"power"::: ) (Set ($#k1_complfld :::"F_Complex"::: ) ) ")" ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "e")) "," (Set (Var "n")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "e")) ($#k1_newton :::"|^"::: ) (Set (Var "n")))))) ; definitionlet "x" be ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ); let "n" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); :: original: :::"CRoot"::: redefine mode :::"CRoot"::: "of" "n" "," "x" -> ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) means :: COMPLFLD:def 2 (Bool (Set (Set "(" ($#k4_group_1 :::"power"::: ) (Set ($#k1_complfld :::"F_Complex"::: ) ) ")" ) ($#k2_binop_1 :::"."::: ) "(" it "," "n" ")" ) ($#r1_hidden :::"="::: ) "x"); end; :: deftheorem defines :::"CRoot"::: COMPLFLD:def 2 : (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) (Bool "for" (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b3")) "is" ($#m1_complfld :::"CRoot"::: ) "of" (Set (Var "n")) "," (Set (Var "x"))) "iff" (Bool (Set (Set "(" ($#k4_group_1 :::"power"::: ) (Set ($#k1_complfld :::"F_Complex"::: ) ) ")" ) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "b3")) "," (Set (Var "n")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "x"))) ")" )))); theorem :: COMPLFLD:75 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) (Bool "for" (Set (Var "v")) "being" ($#m1_complfld :::"CRoot"::: ) "of" (Num 1) "," (Set (Var "x")) "holds" (Bool (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set (Var "x"))))) ; theorem :: COMPLFLD:76 (Bool "for" (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "v")) "being" ($#m1_complfld :::"CRoot"::: ) "of" (Set (Var "n")) "," (Set ($#k4_struct_0 :::"0."::: ) (Set ($#k1_complfld :::"F_Complex"::: ) )) "holds" (Bool (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set ($#k1_complfld :::"F_Complex"::: ) ))))) ; theorem :: COMPLFLD:77 (Bool "for" (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) (Bool "for" (Set (Var "v")) "being" ($#m1_complfld :::"CRoot"::: ) "of" (Set (Var "n")) "," (Set (Var "x")) "st" (Bool (Bool (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set ($#k1_complfld :::"F_Complex"::: ) )))) "holds" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set ($#k1_complfld :::"F_Complex"::: ) )))))) ;