:: FVSUM_1 semantic presentation begin theorem :: FVSUM_1:1 (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) "holds" (Bool (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" (Set (Var "K"))) "is" ($#v1_binop_1 :::"commutative"::: ) )) ; theorem :: FVSUM_1:2 (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) "holds" (Bool (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" (Set (Var "K"))) "is" ($#v2_binop_1 :::"associative"::: ) )) ; theorem :: FVSUM_1:3 (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v5_group_1 :::"commutative"::: ) ($#l3_algstr_0 :::"multMagma"::: ) "holds" (Bool (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "K"))) "is" ($#v1_binop_1 :::"commutative"::: ) )) ; registrationlet "K" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) ; cluster (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" "K") -> ($#v1_binop_1 :::"commutative"::: ) ; end; registrationlet "K" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) ; cluster (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" "K") -> ($#v2_binop_1 :::"associative"::: ) ; end; registrationlet "K" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v5_group_1 :::"commutative"::: ) ($#l3_algstr_0 :::"multMagma"::: ) ; cluster (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" "K") -> ($#v1_binop_1 :::"commutative"::: ) ; end; theorem :: FVSUM_1:4 (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v5_group_1 :::"commutative"::: ) ($#v6_vectsp_1 :::"left_unital"::: ) ($#l4_algstr_0 :::"multLoopStr"::: ) "holds" (Bool (Set ($#k5_struct_0 :::"1."::: ) (Set (Var "K"))) ($#r3_binop_1 :::"is_a_unity_wrt"::: ) (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "K"))))) ; theorem :: FVSUM_1:5 (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v5_group_1 :::"commutative"::: ) ($#v6_vectsp_1 :::"left_unital"::: ) ($#l4_algstr_0 :::"multLoopStr"::: ) "holds" (Bool (Set ($#k4_binop_1 :::"the_unity_wrt"::: ) (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "K")))) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) (Set (Var "K"))))) ; theorem :: FVSUM_1:6 (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_algstr_1 :::"left_zeroed"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) "holds" (Bool (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "K"))) ($#r3_binop_1 :::"is_a_unity_wrt"::: ) (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" (Set (Var "K"))))) ; theorem :: FVSUM_1:7 (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_algstr_1 :::"left_zeroed"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) "holds" (Bool (Set ($#k4_binop_1 :::"the_unity_wrt"::: ) (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" (Set (Var "K")))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "K"))))) ; theorem :: FVSUM_1:8 (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_algstr_1 :::"left_zeroed"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) "holds" (Bool (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" (Set (Var "K"))) "is" ($#v1_setwiseo :::"having_a_unity"::: ) )) ; theorem :: FVSUM_1:9 (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v5_group_1 :::"commutative"::: ) ($#v6_vectsp_1 :::"left_unital"::: ) ($#l4_algstr_0 :::"multLoopStr"::: ) "holds" (Bool (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "K"))) "is" ($#v1_setwiseo :::"having_a_unity"::: ) )) ; theorem :: FVSUM_1:10 (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v5_vectsp_1 :::"distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) "holds" (Bool (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "K"))) ($#r6_binop_1 :::"is_distributive_wrt"::: ) (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" (Set (Var "K"))))) ; definitionlet "K" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) ; let "a" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "K")); func "a" :::"multfield"::: -> ($#m1_subset_1 :::"UnOp":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "K") equals :: FVSUM_1:def 1 (Set (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" "K") ($#k10_funcop_1 :::"[;]"::: ) "(" "a" "," (Set "(" ($#k6_partfun1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "K") ")" ) ")" ); end; :: deftheorem defines :::"multfield"::: FVSUM_1:def 1 : (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) "holds" (Bool (Set (Set (Var "a")) ($#k1_fvsum_1 :::"multfield"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "K"))) ($#k10_funcop_1 :::"[;]"::: ) "(" (Set (Var "a")) "," (Set "(" ($#k6_partfun1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "K"))) ")" ) ")" )))); definitionlet "K" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) ; func :::"diffield"::: "K" -> ($#m1_subset_1 :::"BinOp":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "K") equals :: FVSUM_1:def 2 (Set (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" "K") ($#k7_finseqop :::"*"::: ) "(" (Set "(" ($#k6_partfun1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "K") ")" ) "," (Set "(" ($#k5_vectsp_1 :::"comp"::: ) "K" ")" ) ")" ); end; :: deftheorem defines :::"diffield"::: FVSUM_1:def 2 : (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) "holds" (Bool (Set ($#k2_fvsum_1 :::"diffield"::: ) (Set (Var "K"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" (Set (Var "K"))) ($#k7_finseqop :::"*"::: ) "(" (Set "(" ($#k6_partfun1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "K"))) ")" ) "," (Set "(" ($#k5_vectsp_1 :::"comp"::: ) (Set (Var "K")) ")" ) ")" ))); theorem :: FVSUM_1:11 (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) "holds" (Bool (Set (Set "(" ($#k2_fvsum_1 :::"diffield"::: ) (Set (Var "K")) ")" ) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "a1")) "," (Set (Var "a2")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "a1")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "a2")))))) ; theorem :: FVSUM_1:12 (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v5_vectsp_1 :::"distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) "holds" (Bool (Set (Set (Var "a")) ($#k1_fvsum_1 :::"multfield"::: ) ) ($#r7_binop_1 :::"is_distributive_wrt"::: ) (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" (Set (Var "K")))))) ; theorem :: FVSUM_1:13 (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v1_algstr_1 :::"left_zeroed"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) "holds" (Bool (Set ($#k5_vectsp_1 :::"comp"::: ) (Set (Var "K"))) ($#r1_finseqop :::"is_an_inverseOp_wrt"::: ) (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" (Set (Var "K"))))) ; theorem :: FVSUM_1:14 (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v1_algstr_1 :::"left_zeroed"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) "holds" (Bool (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" (Set (Var "K"))) "is" ($#v1_finseqop :::"having_an_inverseOp"::: ) )) ; theorem :: FVSUM_1:15 (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v1_algstr_1 :::"left_zeroed"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) "holds" (Bool (Set ($#k5_finseqop :::"the_inverseOp_wrt"::: ) (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" (Set (Var "K")))) ($#r2_funct_2 :::"="::: ) (Set ($#k5_vectsp_1 :::"comp"::: ) (Set (Var "K"))))) ; theorem :: FVSUM_1:16 (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) "holds" (Bool (Set ($#k5_vectsp_1 :::"comp"::: ) (Set (Var "K"))) ($#r7_binop_1 :::"is_distributive_wrt"::: ) (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" (Set (Var "K"))))) ; begin definitionlet "K" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) ; let "p1", "p2" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "K"))); func "p1" :::"+"::: "p2" -> ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "K") equals :: FVSUM_1:def 3 (Set (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" "K") ($#k1_finseqop :::".:"::: ) "(" "p1" "," "p2" ")" ); end; :: deftheorem defines :::"+"::: FVSUM_1:def 3 : (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "K"))) "holds" (Bool (Set (Set (Var "p1")) ($#k3_fvsum_1 :::"+"::: ) (Set (Var "p2"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" (Set (Var "K"))) ($#k1_finseqop :::".:"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) ")" )))); theorem :: FVSUM_1:17 (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "K"))) (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set "(" (Set (Var "p1")) ($#k3_fvsum_1 :::"+"::: ) (Set (Var "p2")) ")" ))) & (Bool (Set (Var "a1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "p1")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set (Var "a2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "p2")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))))) "holds" (Bool (Set (Set "(" (Set (Var "p1")) ($#k3_fvsum_1 :::"+"::: ) (Set (Var "p2")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a1")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "a2")))))))) ; definitionlet "i" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "K" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) ; let "R1", "R2" be ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Const "i")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "K")))); :: original: :::"+"::: redefine func "R1" :::"+"::: "R2" -> ($#m2_finseq_2 :::"Element"::: ) "of" (Set "i" ($#k4_finseq_2 :::"-tuples_on"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "K")); end; theorem :: FVSUM_1:18 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "R1")) "," (Set (Var "R2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Var "i")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "K")))) "st" (Bool (Bool (Set (Var "j")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "i")))) & (Bool (Set (Var "a1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "R1")) ($#k1_funct_1 :::"."::: ) (Set (Var "j")))) & (Bool (Set (Var "a2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "R2")) ($#k1_funct_1 :::"."::: ) (Set (Var "j"))))) "holds" (Bool (Set (Set "(" (Set (Var "R1")) ($#k4_fvsum_1 :::"+"::: ) (Set (Var "R2")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "j"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a1")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "a2")))))))) ; theorem :: FVSUM_1:19 (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) "holds" (Bool (Set (Set ($#k4_matrix_2 :::"<*"::: ) (Set (Var "a1")) ($#k4_matrix_2 :::"*>"::: ) ) ($#k4_fvsum_1 :::"+"::: ) (Set ($#k4_matrix_2 :::"<*"::: ) (Set (Var "a2")) ($#k4_matrix_2 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k4_matrix_2 :::"<*"::: ) (Set "(" (Set (Var "a1")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "a2")) ")" ) ($#k4_matrix_2 :::"*>"::: ) )))) ; theorem :: FVSUM_1:20 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) "holds" (Bool (Set (Set "(" (Set (Var "i")) ($#k5_finseq_2 :::"|->"::: ) (Set (Var "a1")) ")" ) ($#k4_fvsum_1 :::"+"::: ) (Set "(" (Set (Var "i")) ($#k5_finseq_2 :::"|->"::: ) (Set (Var "a2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "i")) ($#k5_finseq_2 :::"|->"::: ) (Set "(" (Set (Var "a1")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "a2")) ")" )))))) ; theorem :: FVSUM_1:21 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_algstr_1 :::"left_zeroed"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "R")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Var "i")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "K")))) "holds" (Bool "(" (Bool (Set (Set (Var "R")) ($#k4_fvsum_1 :::"+"::: ) (Set "(" (Set (Var "i")) ($#k5_finseq_2 :::"|->"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "K")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "R"))) & (Bool (Set (Var "R")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "i")) ($#k5_finseq_2 :::"|->"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "K")) ")" ) ")" ) ($#k4_fvsum_1 :::"+"::: ) (Set (Var "R")))) ")" )))) ; definitionlet "K" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) ; let "p" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "K"))); func :::"-"::: "p" -> ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "K") equals :: FVSUM_1:def 4 (Set (Set "(" ($#k5_vectsp_1 :::"comp"::: ) "K" ")" ) ($#k4_finseqop :::"*"::: ) "p"); end; :: deftheorem defines :::"-"::: FVSUM_1:def 4 : (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "K"))) "holds" (Bool (Set ($#k5_fvsum_1 :::"-"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_vectsp_1 :::"comp"::: ) (Set (Var "K")) ")" ) ($#k4_finseqop :::"*"::: ) (Set (Var "p")))))); theorem :: FVSUM_1:22 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "K"))) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set "(" ($#k5_fvsum_1 :::"-"::: ) (Set (Var "p")) ")" ))) & (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))))) "holds" (Bool (Set (Set "(" ($#k5_fvsum_1 :::"-"::: ) (Set (Var "p")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k4_algstr_0 :::"-"::: ) (Set (Var "a")))))))) ; definitionlet "i" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "K" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) ; let "R" be ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Const "i")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "K")))); :: original: :::"-"::: redefine func :::"-"::: "R" -> ($#m2_finseq_2 :::"Element"::: ) "of" (Set "i" ($#k4_finseq_2 :::"-tuples_on"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "K")); end; theorem :: FVSUM_1:23 (Bool "for" (Set (Var "j")) "," (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "R")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Var "i")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "K")))) "st" (Bool (Bool (Set (Var "j")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "i")))) & (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Set (Var "R")) ($#k1_funct_1 :::"."::: ) (Set (Var "j"))))) "holds" (Bool (Set (Set "(" ($#k6_fvsum_1 :::"-"::: ) (Set (Var "R")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "j"))) ($#r1_hidden :::"="::: ) (Set ($#k4_algstr_0 :::"-"::: ) (Set (Var "a")))))))) ; theorem :: FVSUM_1:24 (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) "holds" (Bool (Set ($#k6_fvsum_1 :::"-"::: ) (Set ($#k4_matrix_2 :::"<*"::: ) (Set (Var "a")) ($#k4_matrix_2 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k4_matrix_2 :::"<*"::: ) (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "a")) ")" ) ($#k4_matrix_2 :::"*>"::: ) )))) ; theorem :: FVSUM_1:25 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) "holds" (Bool (Set ($#k6_fvsum_1 :::"-"::: ) (Set "(" (Set (Var "i")) ($#k5_finseq_2 :::"|->"::: ) (Set (Var "a")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "i")) ($#k5_finseq_2 :::"|->"::: ) (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "a")) ")" )))))) ; theorem :: FVSUM_1:26 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "R")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Var "i")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "K")))) "holds" (Bool "(" (Bool (Set (Set (Var "R")) ($#k4_fvsum_1 :::"+"::: ) (Set "(" ($#k6_fvsum_1 :::"-"::: ) (Set (Var "R")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "i")) ($#k5_finseq_2 :::"|->"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "K")) ")" ))) & (Bool (Set (Set "(" ($#k6_fvsum_1 :::"-"::: ) (Set (Var "R")) ")" ) ($#k4_fvsum_1 :::"+"::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "i")) ($#k5_finseq_2 :::"|->"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "K")) ")" ))) ")" )))) ; theorem :: FVSUM_1:27 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v1_algstr_1 :::"left_zeroed"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "R1")) "," (Set (Var "R2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Var "i")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "K")))) "st" (Bool (Bool (Set (Set (Var "R1")) ($#k4_fvsum_1 :::"+"::: ) (Set (Var "R2"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "i")) ($#k5_finseq_2 :::"|->"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "K")) ")" )))) "holds" (Bool "(" (Bool (Set (Var "R1")) ($#r1_hidden :::"="::: ) (Set ($#k6_fvsum_1 :::"-"::: ) (Set (Var "R2")))) & (Bool (Set (Var "R2")) ($#r1_hidden :::"="::: ) (Set ($#k6_fvsum_1 :::"-"::: ) (Set (Var "R1")))) ")" )))) ; theorem :: FVSUM_1:28 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v1_algstr_1 :::"left_zeroed"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "R")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Var "i")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "K")))) "holds" (Bool (Set ($#k6_fvsum_1 :::"-"::: ) (Set "(" ($#k6_fvsum_1 :::"-"::: ) (Set (Var "R")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "R")))))) ; theorem :: FVSUM_1:29 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v1_algstr_1 :::"left_zeroed"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "R1")) "," (Set (Var "R2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Var "i")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "K")))) "st" (Bool (Bool (Set ($#k6_fvsum_1 :::"-"::: ) (Set (Var "R1"))) ($#r1_hidden :::"="::: ) (Set ($#k6_fvsum_1 :::"-"::: ) (Set (Var "R2"))))) "holds" (Bool (Set (Var "R1")) ($#r1_hidden :::"="::: ) (Set (Var "R2")))))) ; theorem :: FVSUM_1:30 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "R")) "," (Set (Var "R1")) "," (Set (Var "R2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Var "i")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "K")))) "st" (Bool (Bool "(" (Bool (Set (Set (Var "R1")) ($#k4_fvsum_1 :::"+"::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "R2")) ($#k4_fvsum_1 :::"+"::: ) (Set (Var "R")))) "or" (Bool (Set (Set (Var "R1")) ($#k4_fvsum_1 :::"+"::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "R")) ($#k4_fvsum_1 :::"+"::: ) (Set (Var "R2")))) ")" )) "holds" (Bool (Set (Var "R1")) ($#r1_hidden :::"="::: ) (Set (Var "R2")))))) ; theorem :: FVSUM_1:31 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "R1")) "," (Set (Var "R2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Var "i")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "K")))) "holds" (Bool (Set ($#k6_fvsum_1 :::"-"::: ) (Set "(" (Set (Var "R1")) ($#k4_fvsum_1 :::"+"::: ) (Set (Var "R2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k6_fvsum_1 :::"-"::: ) (Set (Var "R1")) ")" ) ($#k4_fvsum_1 :::"+"::: ) (Set "(" ($#k6_fvsum_1 :::"-"::: ) (Set (Var "R2")) ")" )))))) ; definitionlet "K" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) ; let "p1", "p2" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "K"))); func "p1" :::"-"::: "p2" -> ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "K") equals :: FVSUM_1:def 5 (Set (Set "(" ($#k2_fvsum_1 :::"diffield"::: ) "K" ")" ) ($#k1_finseqop :::".:"::: ) "(" "p1" "," "p2" ")" ); end; :: deftheorem defines :::"-"::: FVSUM_1:def 5 : (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "K"))) "holds" (Bool (Set (Set (Var "p1")) ($#k7_fvsum_1 :::"-"::: ) (Set (Var "p2"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_fvsum_1 :::"diffield"::: ) (Set (Var "K")) ")" ) ($#k1_finseqop :::".:"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) ")" )))); theorem :: FVSUM_1:32 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "K"))) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set "(" (Set (Var "p1")) ($#k7_fvsum_1 :::"-"::: ) (Set (Var "p2")) ")" ))) & (Bool (Set (Var "a1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "p1")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set (Var "a2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "p2")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))))) "holds" (Bool (Set (Set "(" (Set (Var "p1")) ($#k7_fvsum_1 :::"-"::: ) (Set (Var "p2")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a1")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "a2")))))))) ; definitionlet "i" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "K" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) ; let "R1", "R2" be ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Const "i")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "K")))); :: original: :::"-"::: redefine func "R1" :::"-"::: "R2" -> ($#m2_finseq_2 :::"Element"::: ) "of" (Set "i" ($#k4_finseq_2 :::"-tuples_on"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "K")); end; theorem :: FVSUM_1:33 (Bool "for" (Set (Var "j")) "," (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "R1")) "," (Set (Var "R2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Var "i")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "K")))) "st" (Bool (Bool (Set (Var "j")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "i")))) & (Bool (Set (Var "a1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "R1")) ($#k1_funct_1 :::"."::: ) (Set (Var "j")))) & (Bool (Set (Var "a2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "R2")) ($#k1_funct_1 :::"."::: ) (Set (Var "j"))))) "holds" (Bool (Set (Set "(" (Set (Var "R1")) ($#k8_fvsum_1 :::"-"::: ) (Set (Var "R2")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "j"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a1")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "a2")))))))) ; theorem :: FVSUM_1:34 (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) "holds" (Bool (Set (Set ($#k4_matrix_2 :::"<*"::: ) (Set (Var "a1")) ($#k4_matrix_2 :::"*>"::: ) ) ($#k8_fvsum_1 :::"-"::: ) (Set ($#k4_matrix_2 :::"<*"::: ) (Set (Var "a2")) ($#k4_matrix_2 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k4_matrix_2 :::"<*"::: ) (Set "(" (Set (Var "a1")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "a2")) ")" ) ($#k4_matrix_2 :::"*>"::: ) )))) ; theorem :: FVSUM_1:35 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) "holds" (Bool (Set (Set "(" (Set (Var "i")) ($#k5_finseq_2 :::"|->"::: ) (Set (Var "a1")) ")" ) ($#k8_fvsum_1 :::"-"::: ) (Set "(" (Set (Var "i")) ($#k5_finseq_2 :::"|->"::: ) (Set (Var "a2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "i")) ($#k5_finseq_2 :::"|->"::: ) (Set "(" (Set (Var "a1")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "a2")) ")" )))))) ; theorem :: FVSUM_1:36 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v1_algstr_1 :::"left_zeroed"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "R")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Var "i")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "K")))) "holds" (Bool (Set (Set (Var "R")) ($#k8_fvsum_1 :::"-"::: ) (Set "(" (Set (Var "i")) ($#k5_finseq_2 :::"|->"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "K")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "R")))))) ; theorem :: FVSUM_1:37 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_algstr_1 :::"left_zeroed"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "R")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Var "i")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "K")))) "holds" (Bool (Set (Set "(" (Set (Var "i")) ($#k5_finseq_2 :::"|->"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "K")) ")" ) ")" ) ($#k8_fvsum_1 :::"-"::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Set ($#k6_fvsum_1 :::"-"::: ) (Set (Var "R"))))))) ; theorem :: FVSUM_1:38 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v1_algstr_1 :::"left_zeroed"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "R1")) "," (Set (Var "R2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Var "i")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "K")))) "holds" (Bool (Set (Set (Var "R1")) ($#k8_fvsum_1 :::"-"::: ) (Set "(" ($#k6_fvsum_1 :::"-"::: ) (Set (Var "R2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "R1")) ($#k4_fvsum_1 :::"+"::: ) (Set (Var "R2"))))))) ; theorem :: FVSUM_1:39 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "R1")) "," (Set (Var "R2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Var "i")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "K")))) "holds" (Bool (Set ($#k6_fvsum_1 :::"-"::: ) (Set "(" (Set (Var "R1")) ($#k8_fvsum_1 :::"-"::: ) (Set (Var "R2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "R2")) ($#k8_fvsum_1 :::"-"::: ) (Set (Var "R1"))))))) ; theorem :: FVSUM_1:40 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "R1")) "," (Set (Var "R2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Var "i")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "K")))) "holds" (Bool (Set ($#k6_fvsum_1 :::"-"::: ) (Set "(" (Set (Var "R1")) ($#k8_fvsum_1 :::"-"::: ) (Set (Var "R2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k6_fvsum_1 :::"-"::: ) (Set (Var "R1")) ")" ) ($#k4_fvsum_1 :::"+"::: ) (Set (Var "R2"))))))) ; theorem :: FVSUM_1:41 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "R")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Var "i")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "K")))) "holds" (Bool (Set (Set (Var "R")) ($#k8_fvsum_1 :::"-"::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "i")) ($#k5_finseq_2 :::"|->"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "K")) ")" )))))) ; theorem :: FVSUM_1:42 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "R1")) "," (Set (Var "R2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Var "i")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "K")))) "st" (Bool (Bool (Set (Set (Var "R1")) ($#k8_fvsum_1 :::"-"::: ) (Set (Var "R2"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "i")) ($#k5_finseq_2 :::"|->"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "K")) ")" )))) "holds" (Bool (Set (Var "R1")) ($#r1_hidden :::"="::: ) (Set (Var "R2")))))) ; theorem :: FVSUM_1:43 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "R1")) "," (Set (Var "R2")) "," (Set (Var "R3")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Var "i")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "K")))) "holds" (Bool (Set (Set "(" (Set (Var "R1")) ($#k8_fvsum_1 :::"-"::: ) (Set (Var "R2")) ")" ) ($#k8_fvsum_1 :::"-"::: ) (Set (Var "R3"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "R1")) ($#k8_fvsum_1 :::"-"::: ) (Set "(" (Set (Var "R2")) ($#k4_fvsum_1 :::"+"::: ) (Set (Var "R3")) ")" )))))) ; theorem :: FVSUM_1:44 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "R1")) "," (Set (Var "R2")) "," (Set (Var "R3")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Var "i")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "K")))) "holds" (Bool (Set (Set (Var "R1")) ($#k4_fvsum_1 :::"+"::: ) (Set "(" (Set (Var "R2")) ($#k8_fvsum_1 :::"-"::: ) (Set (Var "R3")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "R1")) ($#k4_fvsum_1 :::"+"::: ) (Set (Var "R2")) ")" ) ($#k8_fvsum_1 :::"-"::: ) (Set (Var "R3"))))))) ; theorem :: FVSUM_1:45 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "R1")) "," (Set (Var "R2")) "," (Set (Var "R3")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Var "i")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "K")))) "holds" (Bool (Set (Set (Var "R1")) ($#k8_fvsum_1 :::"-"::: ) (Set "(" (Set (Var "R2")) ($#k8_fvsum_1 :::"-"::: ) (Set (Var "R3")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "R1")) ($#k8_fvsum_1 :::"-"::: ) (Set (Var "R2")) ")" ) ($#k4_fvsum_1 :::"+"::: ) (Set (Var "R3"))))))) ; theorem :: FVSUM_1:46 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "R1")) "," (Set (Var "R")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Var "i")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "K")))) "holds" (Bool (Set (Var "R1")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "R1")) ($#k4_fvsum_1 :::"+"::: ) (Set (Var "R")) ")" ) ($#k8_fvsum_1 :::"-"::: ) (Set (Var "R"))))))) ; theorem :: FVSUM_1:47 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "R1")) "," (Set (Var "R")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Var "i")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "K")))) "holds" (Bool (Set (Var "R1")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "R1")) ($#k8_fvsum_1 :::"-"::: ) (Set (Var "R")) ")" ) ($#k4_fvsum_1 :::"+"::: ) (Set (Var "R"))))))) ; theorem :: FVSUM_1:48 (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) "holds" (Bool (Set (Set "(" (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "K"))) ($#k10_funcop_1 :::"[;]"::: ) "(" (Set (Var "a")) "," (Set "(" ($#k6_partfun1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "K"))) ")" ) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "b")))))) ; theorem :: FVSUM_1:49 (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k1_fvsum_1 :::"multfield"::: ) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "b")))))) ; definitionlet "K" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) ; let "p" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "K"))); let "a" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "K")); func "a" :::"*"::: "p" -> ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "K") equals :: FVSUM_1:def 6 (Set (Set "(" "a" ($#k1_fvsum_1 :::"multfield"::: ) ")" ) ($#k4_finseqop :::"*"::: ) "p"); end; :: deftheorem defines :::"*"::: FVSUM_1:def 6 : (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "K"))) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) "holds" (Bool (Set (Set (Var "a")) ($#k9_fvsum_1 :::"*"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k1_fvsum_1 :::"multfield"::: ) ")" ) ($#k4_finseqop :::"*"::: ) (Set (Var "p"))))))); theorem :: FVSUM_1:50 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "a9")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "K"))) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set "(" (Set (Var "a")) ($#k9_fvsum_1 :::"*"::: ) (Set (Var "p")) ")" ))) & (Bool (Set (Var "a9")) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))))) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k9_fvsum_1 :::"*"::: ) (Set (Var "p")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "a9")))))))) ; definitionlet "i" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "K" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) ; let "R" be ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Const "i")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "K")))); let "a" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "K")); :: original: :::"*"::: redefine func "a" :::"*"::: "R" -> ($#m2_finseq_2 :::"Element"::: ) "of" (Set "i" ($#k4_finseq_2 :::"-tuples_on"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "K")); end; theorem :: FVSUM_1:51 (Bool "for" (Set (Var "j")) "," (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "a9")) "," (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "R")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Var "i")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "K")))) "st" (Bool (Bool (Set (Var "j")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "i")))) & (Bool (Set (Var "a9")) ($#r1_hidden :::"="::: ) (Set (Set (Var "R")) ($#k1_funct_1 :::"."::: ) (Set (Var "j"))))) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k10_fvsum_1 :::"*"::: ) (Set (Var "R")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "j"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "a9")))))))) ; theorem :: FVSUM_1:52 (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "a1")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) "holds" (Bool (Set (Set (Var "a")) ($#k10_fvsum_1 :::"*"::: ) (Set ($#k4_matrix_2 :::"<*"::: ) (Set (Var "a1")) ($#k4_matrix_2 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k4_matrix_2 :::"<*"::: ) (Set "(" (Set (Var "a")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "a1")) ")" ) ($#k4_matrix_2 :::"*>"::: ) )))) ; theorem :: FVSUM_1:53 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) "holds" (Bool (Set (Set (Var "a1")) ($#k10_fvsum_1 :::"*"::: ) (Set "(" (Set (Var "i")) ($#k5_finseq_2 :::"|->"::: ) (Set (Var "a2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "i")) ($#k5_finseq_2 :::"|->"::: ) (Set "(" (Set (Var "a1")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "a2")) ")" )))))) ; theorem :: FVSUM_1:54 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_group_1 :::"associative"::: ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "R")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Var "i")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "K")))) "holds" (Bool (Set (Set "(" (Set (Var "a1")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "a2")) ")" ) ($#k10_fvsum_1 :::"*"::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a1")) ($#k10_fvsum_1 :::"*"::: ) (Set "(" (Set (Var "a2")) ($#k10_fvsum_1 :::"*"::: ) (Set (Var "R")) ")" ))))))) ; theorem :: FVSUM_1:55 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v5_vectsp_1 :::"distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "R")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Var "i")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "K")))) "holds" (Bool (Set (Set "(" (Set (Var "a1")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "a2")) ")" ) ($#k10_fvsum_1 :::"*"::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a1")) ($#k10_fvsum_1 :::"*"::: ) (Set (Var "R")) ")" ) ($#k4_fvsum_1 :::"+"::: ) (Set "(" (Set (Var "a2")) ($#k10_fvsum_1 :::"*"::: ) (Set (Var "R")) ")" ))))))) ; theorem :: FVSUM_1:56 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v5_vectsp_1 :::"distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "R1")) "," (Set (Var "R2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Var "i")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "K")))) "holds" (Bool (Set (Set (Var "a")) ($#k10_fvsum_1 :::"*"::: ) (Set "(" (Set (Var "R1")) ($#k4_fvsum_1 :::"+"::: ) (Set (Var "R2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k10_fvsum_1 :::"*"::: ) (Set (Var "R1")) ")" ) ($#k4_fvsum_1 :::"+"::: ) (Set "(" (Set (Var "a")) ($#k10_fvsum_1 :::"*"::: ) (Set (Var "R2")) ")" ))))))) ; theorem :: FVSUM_1:57 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v5_group_1 :::"commutative"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v6_vectsp_1 :::"left_unital"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "R")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Var "i")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "K")))) "holds" (Bool (Set (Set "(" ($#k5_struct_0 :::"1."::: ) (Set (Var "K")) ")" ) ($#k10_fvsum_1 :::"*"::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Set (Var "R")))))) ; theorem :: FVSUM_1:58 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "R")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Var "i")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "K")))) "holds" (Bool (Set (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "K")) ")" ) ($#k10_fvsum_1 :::"*"::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "i")) ($#k5_finseq_2 :::"|->"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "K")) ")" )))))) ; theorem :: FVSUM_1:59 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v6_vectsp_1 :::"left_unital"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "R")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Var "i")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "K")))) "holds" (Bool (Set (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set "(" ($#k5_struct_0 :::"1."::: ) (Set (Var "K")) ")" ) ")" ) ($#k10_fvsum_1 :::"*"::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Set ($#k6_fvsum_1 :::"-"::: ) (Set (Var "R"))))))) ; definitionlet "M" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) ; let "p1", "p2" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "M"))); func :::"mlt"::: "(" "p1" "," "p2" ")" -> ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "M") equals :: FVSUM_1:def 7 (Set (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" "M") ($#k1_finseqop :::".:"::: ) "(" "p1" "," "p2" ")" ); end; :: deftheorem defines :::"mlt"::: FVSUM_1:def 7 : (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) "holds" (Bool (Set ($#k11_fvsum_1 :::"mlt"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u2_algstr_0 :::"multF"::: ) "of" (Set (Var "M"))) ($#k1_finseqop :::".:"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) ")" )))); theorem :: FVSUM_1:60 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "K"))) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set "(" ($#k11_fvsum_1 :::"mlt"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) ")" ")" ))) & (Bool (Set (Var "a1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "p1")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set (Var "a2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "p2")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))))) "holds" (Bool (Set (Set "(" ($#k11_fvsum_1 :::"mlt"::: ) "(" (Set (Var "p1")) "," (Set (Var "p2")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a1")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "a2")))))))) ; definitionlet "i" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "K" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) ; let "R1", "R2" be ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Const "i")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "K")))); :: original: :::"mlt"::: redefine func :::"mlt"::: "(" "R1" "," "R2" ")" -> ($#m2_finseq_2 :::"Element"::: ) "of" (Set "i" ($#k4_finseq_2 :::"-tuples_on"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "K")); end; theorem :: FVSUM_1:61 (Bool "for" (Set (Var "j")) "," (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "R1")) "," (Set (Var "R2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Var "i")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "K")))) "st" (Bool (Bool (Set (Var "j")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "i")))) & (Bool (Set (Var "a1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "R1")) ($#k1_funct_1 :::"."::: ) (Set (Var "j")))) & (Bool (Set (Var "a2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "R2")) ($#k1_funct_1 :::"."::: ) (Set (Var "j"))))) "holds" (Bool (Set (Set "(" ($#k12_fvsum_1 :::"mlt"::: ) "(" (Set (Var "R1")) "," (Set (Var "R2")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "j"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a1")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "a2")))))))) ; theorem :: FVSUM_1:62 (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) "holds" (Bool (Set ($#k12_fvsum_1 :::"mlt"::: ) "(" (Set ($#k4_matrix_2 :::"<*"::: ) (Set (Var "a1")) ($#k4_matrix_2 :::"*>"::: ) ) "," (Set ($#k4_matrix_2 :::"<*"::: ) (Set (Var "a2")) ($#k4_matrix_2 :::"*>"::: ) ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_matrix_2 :::"<*"::: ) (Set "(" (Set (Var "a1")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "a2")) ")" ) ($#k4_matrix_2 :::"*>"::: ) )))) ; theorem :: FVSUM_1:63 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v5_group_1 :::"commutative"::: ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "R1")) "," (Set (Var "R2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Var "i")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "K")))) "holds" (Bool (Set ($#k12_fvsum_1 :::"mlt"::: ) "(" (Set (Var "R1")) "," (Set (Var "R2")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k12_fvsum_1 :::"mlt"::: ) "(" (Set (Var "R2")) "," (Set (Var "R1")) ")" ))))) ; theorem :: FVSUM_1:64 (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v5_group_1 :::"commutative"::: ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "K"))) "holds" (Bool (Set ($#k11_fvsum_1 :::"mlt"::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k11_fvsum_1 :::"mlt"::: ) "(" (Set (Var "q")) "," (Set (Var "p")) ")" )))) ; theorem :: FVSUM_1:65 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_group_1 :::"associative"::: ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "R1")) "," (Set (Var "R2")) "," (Set (Var "R3")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Var "i")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "K")))) "holds" (Bool (Set ($#k12_fvsum_1 :::"mlt"::: ) "(" (Set (Var "R1")) "," (Set "(" ($#k12_fvsum_1 :::"mlt"::: ) "(" (Set (Var "R2")) "," (Set (Var "R3")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k12_fvsum_1 :::"mlt"::: ) "(" (Set "(" ($#k12_fvsum_1 :::"mlt"::: ) "(" (Set (Var "R1")) "," (Set (Var "R2")) ")" ")" ) "," (Set (Var "R3")) ")" ))))) ; theorem :: FVSUM_1:66 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "R")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Var "i")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "K")))) "holds" (Bool "(" (Bool (Set ($#k12_fvsum_1 :::"mlt"::: ) "(" (Set "(" (Set (Var "i")) ($#k5_finseq_2 :::"|->"::: ) (Set (Var "a")) ")" ) "," (Set (Var "R")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k10_fvsum_1 :::"*"::: ) (Set (Var "R")))) & (Bool (Set ($#k12_fvsum_1 :::"mlt"::: ) "(" (Set (Var "R")) "," (Set "(" (Set (Var "i")) ($#k5_finseq_2 :::"|->"::: ) (Set (Var "a")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k10_fvsum_1 :::"*"::: ) (Set (Var "R")))) ")" ))))) ; theorem :: FVSUM_1:67 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) "holds" (Bool (Set ($#k12_fvsum_1 :::"mlt"::: ) "(" (Set "(" (Set (Var "i")) ($#k5_finseq_2 :::"|->"::: ) (Set (Var "a1")) ")" ) "," (Set "(" (Set (Var "i")) ($#k5_finseq_2 :::"|->"::: ) (Set (Var "a2")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "i")) ($#k5_finseq_2 :::"|->"::: ) (Set "(" (Set (Var "a1")) ($#k8_group_1 :::"*"::: ) (Set (Var "a2")) ")" )))))) ; theorem :: FVSUM_1:68 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_group_1 :::"associative"::: ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "R1")) "," (Set (Var "R2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Var "i")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "K")))) "holds" (Bool (Set (Set (Var "a")) ($#k10_fvsum_1 :::"*"::: ) (Set "(" ($#k12_fvsum_1 :::"mlt"::: ) "(" (Set (Var "R1")) "," (Set (Var "R2")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k12_fvsum_1 :::"mlt"::: ) "(" (Set "(" (Set (Var "a")) ($#k10_fvsum_1 :::"*"::: ) (Set (Var "R1")) ")" ) "," (Set (Var "R2")) ")" )))))) ; theorem :: FVSUM_1:69 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "R1")) "," (Set (Var "R2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Var "i")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "K")))) "holds" (Bool "(" (Bool (Set (Set (Var "a")) ($#k10_fvsum_1 :::"*"::: ) (Set "(" ($#k12_fvsum_1 :::"mlt"::: ) "(" (Set (Var "R1")) "," (Set (Var "R2")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k12_fvsum_1 :::"mlt"::: ) "(" (Set "(" (Set (Var "a")) ($#k10_fvsum_1 :::"*"::: ) (Set (Var "R1")) ")" ) "," (Set (Var "R2")) ")" )) & (Bool (Set (Set (Var "a")) ($#k10_fvsum_1 :::"*"::: ) (Set "(" ($#k12_fvsum_1 :::"mlt"::: ) "(" (Set (Var "R1")) "," (Set (Var "R2")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k12_fvsum_1 :::"mlt"::: ) "(" (Set (Var "R1")) "," (Set "(" (Set (Var "a")) ($#k10_fvsum_1 :::"*"::: ) (Set (Var "R2")) ")" ) ")" )) ")" ))))) ; theorem :: FVSUM_1:70 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "R")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Var "i")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "K")))) "holds" (Bool (Set (Set (Var "a")) ($#k10_fvsum_1 :::"*"::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Set ($#k12_fvsum_1 :::"mlt"::: ) "(" (Set "(" (Set (Var "i")) ($#k5_finseq_2 :::"|->"::: ) (Set (Var "a")) ")" ) "," (Set (Var "R")) ")" )))))) ; begin registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_algstr_1 :::"left_zeroed"::: ) for ($#l2_algstr_0 :::"addLoopStr"::: ) ; end; definitionlet "K" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) ; let "p" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "K"))); redefine func :::"Sum"::: "p" equals :: FVSUM_1:def 8 (Set (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" "K") ($#k1_finsop_1 :::"$$"::: ) "p"); end; :: deftheorem defines :::"Sum"::: FVSUM_1:def 8 : (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "K"))) "holds" (Bool (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" (Set (Var "K"))) ($#k1_finsop_1 :::"$$"::: ) (Set (Var "p")))))); theorem :: FVSUM_1:71 (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "K"))) "holds" (Bool (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set "(" (Set (Var "p")) ($#k8_finseq_1 :::"^"::: ) (Set ($#k4_matrix_2 :::"<*"::: ) (Set (Var "a")) ($#k4_matrix_2 :::"*>"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_rlvect_1 :::"Sum"::: ) (Set (Var "p")) ")" ) ($#k1_algstr_0 :::"+"::: ) (Set (Var "a"))))))) ; theorem :: FVSUM_1:72 (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "K"))) "holds" (Bool (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set "(" (Set ($#k4_matrix_2 :::"<*"::: ) (Set (Var "a")) ($#k4_matrix_2 :::"*>"::: ) ) ($#k8_finseq_1 :::"^"::: ) (Set (Var "p")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k1_algstr_0 :::"+"::: ) (Set "(" ($#k4_rlvect_1 :::"Sum"::: ) (Set (Var "p")) ")" )))))) ; theorem :: FVSUM_1:73 (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "K"))) "holds" (Bool (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set "(" (Set (Var "a")) ($#k9_fvsum_1 :::"*"::: ) (Set (Var "p")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k6_algstr_0 :::"*"::: ) (Set "(" ($#k4_rlvect_1 :::"Sum"::: ) (Set (Var "p")) ")" )))))) ; theorem :: FVSUM_1:74 (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "R")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set ($#k6_numbers :::"0"::: ) ) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "K")))) "holds" (Bool (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "K")))))) ; theorem :: FVSUM_1:75 (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "K"))) "holds" (Bool (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set "(" ($#k5_fvsum_1 :::"-"::: ) (Set (Var "p")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_algstr_0 :::"-"::: ) (Set "(" ($#k4_rlvect_1 :::"Sum"::: ) (Set (Var "p")) ")" ))))) ; theorem :: FVSUM_1:76 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "R1")) "," (Set (Var "R2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Var "i")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "K")))) "holds" (Bool (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set "(" (Set (Var "R1")) ($#k4_fvsum_1 :::"+"::: ) (Set (Var "R2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_rlvect_1 :::"Sum"::: ) (Set (Var "R1")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" ($#k4_rlvect_1 :::"Sum"::: ) (Set (Var "R2")) ")" )))))) ; theorem :: FVSUM_1:77 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "R1")) "," (Set (Var "R2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Var "i")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "K")))) "holds" (Bool (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set "(" (Set (Var "R1")) ($#k8_fvsum_1 :::"-"::: ) (Set (Var "R2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_rlvect_1 :::"Sum"::: ) (Set (Var "R1")) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" ($#k4_rlvect_1 :::"Sum"::: ) (Set (Var "R2")) ")" )))))) ; begin theorem :: FVSUM_1:78 (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "p1")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "K"))) "holds" (Bool (Set ($#k3_group_4 :::"Product"::: ) (Set "(" (Set ($#k4_matrix_2 :::"<*"::: ) (Set (Var "a")) ($#k4_matrix_2 :::"*>"::: ) ) ($#k8_finseq_1 :::"^"::: ) (Set (Var "p1")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k8_group_1 :::"*"::: ) (Set "(" ($#k3_group_4 :::"Product"::: ) (Set (Var "p1")) ")" )))))) ; theorem :: FVSUM_1:79 (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) "holds" (Bool (Set ($#k3_group_4 :::"Product"::: ) (Set ($#k3_finseq_4 :::"<*"::: ) (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) ($#k3_finseq_4 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a1")) ($#k8_group_1 :::"*"::: ) (Set (Var "a2")) ")" ) ($#k8_group_1 :::"*"::: ) (Set (Var "a3")))))) ; theorem :: FVSUM_1:80 (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "R")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set ($#k6_numbers :::"0"::: ) ) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "K")))) "holds" (Bool (Set ($#k3_group_4 :::"Product"::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) (Set (Var "K")))))) ; theorem :: FVSUM_1:81 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) "holds" (Bool (Set ($#k3_group_4 :::"Product"::: ) (Set "(" (Set (Var "i")) ($#k5_finseq_2 :::"|->"::: ) (Set "(" ($#k1_group_1 :::"1_"::: ) (Set (Var "K")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_group_1 :::"1_"::: ) (Set (Var "K")))))) ; theorem :: FVSUM_1:82 (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v6_struct_0 "non" ($#v6_struct_0 :::"degenerated"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v33_algstr_0 :::"almost_left_invertible"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "K"))) "holds" (Bool "(" (Bool "ex" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p")))) & (Bool (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "K")))) ")" )) "iff" (Bool (Set ($#k3_group_4 :::"Product"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "K")))) ")" ))) ; theorem :: FVSUM_1:83 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) "holds" (Bool (Set ($#k3_group_4 :::"Product"::: ) (Set "(" (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Set (Var "j")) ")" ) ($#k5_finseq_2 :::"|->"::: ) (Set (Var "a")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_group_4 :::"Product"::: ) (Set "(" (Set (Var "i")) ($#k5_finseq_2 :::"|->"::: ) (Set (Var "a")) ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" ($#k3_group_4 :::"Product"::: ) (Set "(" (Set (Var "j")) ($#k5_finseq_2 :::"|->"::: ) (Set (Var "a")) ")" ) ")" )))))) ; theorem :: FVSUM_1:84 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) "holds" (Bool (Set ($#k3_group_4 :::"Product"::: ) (Set "(" (Set "(" (Set (Var "i")) ($#k4_nat_1 :::"*"::: ) (Set (Var "j")) ")" ) ($#k5_finseq_2 :::"|->"::: ) (Set (Var "a")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_group_4 :::"Product"::: ) (Set "(" (Set (Var "j")) ($#k5_finseq_2 :::"|->"::: ) (Set "(" ($#k3_group_4 :::"Product"::: ) (Set "(" (Set (Var "i")) ($#k5_finseq_2 :::"|->"::: ) (Set (Var "a")) ")" ) ")" ) ")" )))))) ; theorem :: FVSUM_1:85 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) "holds" (Bool (Set ($#k3_group_4 :::"Product"::: ) (Set "(" (Set (Var "i")) ($#k5_finseq_2 :::"|->"::: ) (Set "(" (Set (Var "a1")) ($#k8_group_1 :::"*"::: ) (Set (Var "a2")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_group_4 :::"Product"::: ) (Set "(" (Set (Var "i")) ($#k5_finseq_2 :::"|->"::: ) (Set (Var "a1")) ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" ($#k3_group_4 :::"Product"::: ) (Set "(" (Set (Var "i")) ($#k5_finseq_2 :::"|->"::: ) (Set (Var "a2")) ")" ) ")" )))))) ; theorem :: FVSUM_1:86 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "R1")) "," (Set (Var "R2")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Var "i")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "K")))) "holds" (Bool (Set ($#k3_group_4 :::"Product"::: ) (Set "(" ($#k12_fvsum_1 :::"mlt"::: ) "(" (Set (Var "R1")) "," (Set (Var "R2")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_group_4 :::"Product"::: ) (Set (Var "R1")) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" ($#k3_group_4 :::"Product"::: ) (Set (Var "R2")) ")" )))))) ; theorem :: FVSUM_1:87 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) (Bool "for" (Set (Var "R1")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Var "i")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "K")))) "holds" (Bool (Set ($#k3_group_4 :::"Product"::: ) (Set "(" (Set (Var "a")) ($#k10_fvsum_1 :::"*"::: ) (Set (Var "R1")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_group_4 :::"Product"::: ) (Set "(" (Set (Var "i")) ($#k5_finseq_2 :::"|->"::: ) (Set (Var "a")) ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" ($#k3_group_4 :::"Product"::: ) (Set (Var "R1")) ")" ))))))) ; begin definitionlet "K" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "p", "q" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "K"))); func "p" :::""*""::: "q" -> ($#m1_subset_1 :::"Element":::) "of" "K" equals :: FVSUM_1:def 9 (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set "(" ($#k11_fvsum_1 :::"mlt"::: ) "(" "p" "," "q" ")" ")" )); end; :: deftheorem defines :::""*""::: FVSUM_1:def 9 : (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "K"))) "holds" (Bool (Set (Set (Var "p")) ($#k13_fvsum_1 :::""*""::: ) (Set (Var "q"))) ($#r1_hidden :::"="::: ) (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set "(" ($#k11_fvsum_1 :::"mlt"::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" ")" ))))); theorem :: FVSUM_1:88 (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v6_vectsp_1 :::"left_unital"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) "holds" (Bool (Set (Set ($#k4_matrix_2 :::"<*"::: ) (Set (Var "a")) ($#k4_matrix_2 :::"*>"::: ) ) ($#k13_fvsum_1 :::""*""::: ) (Set ($#k4_matrix_2 :::"<*"::: ) (Set (Var "b")) ($#k4_matrix_2 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k8_group_1 :::"*"::: ) (Set (Var "b")))))) ; theorem :: FVSUM_1:89 (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v6_vectsp_1 :::"left_unital"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "b1")) "," (Set (Var "b2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "K")) "holds" (Bool (Set (Set ($#k2_finseq_4 :::"<*"::: ) (Set (Var "a1")) "," (Set (Var "a2")) ($#k2_finseq_4 :::"*>"::: ) ) ($#k13_fvsum_1 :::""*""::: ) (Set ($#k2_finseq_4 :::"<*"::: ) (Set (Var "b1")) "," (Set (Var "b2")) ($#k2_finseq_4 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a1")) ($#k8_group_1 :::"*"::: ) (Set (Var "b1")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "a2")) ($#k8_group_1 :::"*"::: ) (Set (Var "b2")) ")" ))))) ; theorem :: FVSUM_1:90 (Bool "for" (Set (Var "K")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "K"))) "holds" (Bool (Set (Set (Var "p")) ($#k13_fvsum_1 :::""*""::: ) (Set (Var "q"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "q")) ($#k13_fvsum_1 :::""*""::: ) (Set (Var "p")))))) ;