:: RLVECT_1 semantic presentation begin definitionattr "c1" is :::"strict"::: ; struct :::"RLSStruct"::: -> ($#l2_algstr_0 :::"addLoopStr"::: ) ; aggr :::"RLSStruct":::(# :::"carrier":::, :::"ZeroF":::, :::"addF":::, :::"Mult"::: #) -> ($#l1_rlvect_1 :::"RLSStruct"::: ) ; sel :::"Mult"::: "c1" -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "c1") ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "c1"); end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) for ($#l1_rlvect_1 :::"RLSStruct"::: ) ; end; definitionlet "V" be ($#l1_rlvect_1 :::"RLSStruct"::: ) ; mode VECTOR of "V" is ($#m1_subset_1 :::"Element":::) "of" "V"; end; theorem :: RLVECT_1:1 (Bool "for" (Set (Var "V")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_struct_0 :::"1-sorted"::: ) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "holds" (Bool (Set (Var "v")) ($#r1_struct_0 :::"in"::: ) (Set (Var "V"))))) ; definitionlet "V" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rlvect_1 :::"RLSStruct"::: ) ; let "v" be ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Const "V")); let "a" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; func "a" :::"*"::: "v" -> ($#m1_subset_1 :::"Element":::) "of" "V" equals :: RLVECT_1:def 1 (Set (Set "the" ($#u1_rlvect_1 :::"Mult"::: ) "of" "V") ($#k1_binop_1 :::"."::: ) "(" "a" "," "v" ")" ); end; :: deftheorem defines :::"*"::: RLVECT_1:def 1 : (Bool "for" (Set (Var "V")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rlvect_1 :::"RLSStruct"::: ) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "a")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_rlvect_1 :::"Mult"::: ) "of" (Set (Var "V"))) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "v")) ")" ))))); theorem :: RLVECT_1:2 (Bool "for" (Set (Var "V")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_algstr_0 :::"addMagma"::: ) (Bool "for" (Set (Var "v")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "holds" (Bool (Set (Set (Var "v")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "w"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_algstr_0 :::"addF"::: ) "of" (Set (Var "V"))) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "v")) "," (Set (Var "w")) ")" )))) ; registrationlet "ZS" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "O" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "ZS")); let "F" be ($#m1_subset_1 :::"BinOp":::) "of" (Set (Const "ZS")); let "G" be ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set (Const "ZS")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Const "ZS")); cluster (Set ($#g1_rlvect_1 :::"RLSStruct"::: ) "(#" "ZS" "," "O" "," "F" "," "G" "#)" ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ; end; definitionlet "IT" be ($#l1_algstr_0 :::"addMagma"::: ) ; attr "IT" is :::"Abelian"::: means :: RLVECT_1:def 2 (Bool "for" (Set (Var "v")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" "holds" (Bool (Set (Set (Var "v")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "w"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "w")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "v"))))); attr "IT" is :::"add-associative"::: means :: RLVECT_1:def 3 (Bool "for" (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" "holds" (Bool (Set (Set "(" (Set (Var "u")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "v")) ")" ) ($#k1_algstr_0 :::"+"::: ) (Set (Var "w"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "u")) ($#k1_algstr_0 :::"+"::: ) (Set "(" (Set (Var "v")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "w")) ")" )))); end; :: deftheorem defines :::"Abelian"::: RLVECT_1:def 2 : (Bool "for" (Set (Var "IT")) "being" ($#l1_algstr_0 :::"addMagma"::: ) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v2_rlvect_1 :::"Abelian"::: ) ) "iff" (Bool "for" (Set (Var "v")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "holds" (Bool (Set (Set (Var "v")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "w"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "w")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "v"))))) ")" )); :: deftheorem defines :::"add-associative"::: RLVECT_1:def 3 : (Bool "for" (Set (Var "IT")) "being" ($#l1_algstr_0 :::"addMagma"::: ) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v3_rlvect_1 :::"add-associative"::: ) ) "iff" (Bool "for" (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "holds" (Bool (Set (Set "(" (Set (Var "u")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "v")) ")" ) ($#k1_algstr_0 :::"+"::: ) (Set (Var "w"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "u")) ($#k1_algstr_0 :::"+"::: ) (Set "(" (Set (Var "v")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "w")) ")" )))) ")" )); definitionlet "IT" be ($#l2_algstr_0 :::"addLoopStr"::: ) ; attr "IT" is :::"right_zeroed"::: means :: RLVECT_1:def 4 (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" "holds" (Bool (Set (Set (Var "v")) ($#k1_algstr_0 :::"+"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) "IT" ")" )) ($#r1_hidden :::"="::: ) (Set (Var "v")))); end; :: deftheorem defines :::"right_zeroed"::: RLVECT_1:def 4 : (Bool "for" (Set (Var "IT")) "being" ($#l2_algstr_0 :::"addLoopStr"::: ) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v4_rlvect_1 :::"right_zeroed"::: ) ) "iff" (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "holds" (Bool (Set (Set (Var "v")) ($#k1_algstr_0 :::"+"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "IT")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "v")))) ")" )); definitionlet "IT" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rlvect_1 :::"RLSStruct"::: ) ; attr "IT" is :::"vector-distributive"::: means :: RLVECT_1:def 5 (Bool "for" (Set (Var "a")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "v")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" "IT" "holds" (Bool (Set (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set (Var "v")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "w")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "v")) ")" ) ($#k1_algstr_0 :::"+"::: ) (Set "(" (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "w")) ")" ))))); attr "IT" is :::"scalar-distributive"::: means :: RLVECT_1:def 6 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" "IT" "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "b")) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "v")) ")" ) ($#k1_algstr_0 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "v")) ")" ))))); attr "IT" is :::"scalar-associative"::: means :: RLVECT_1:def 7 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" "IT" "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "b")) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set (Var "b")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "v")) ")" ))))); attr "IT" is :::"scalar-unital"::: means :: RLVECT_1:def 8 (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" "IT" "holds" (Bool (Set (Num 1) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set (Var "v")))); end; :: deftheorem defines :::"vector-distributive"::: RLVECT_1:def 5 : (Bool "for" (Set (Var "IT")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rlvect_1 :::"RLSStruct"::: ) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v5_rlvect_1 :::"vector-distributive"::: ) ) "iff" (Bool "for" (Set (Var "a")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "v")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "IT")) "holds" (Bool (Set (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set (Var "v")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "w")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "v")) ")" ) ($#k1_algstr_0 :::"+"::: ) (Set "(" (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "w")) ")" ))))) ")" )); :: deftheorem defines :::"scalar-distributive"::: RLVECT_1:def 6 : (Bool "for" (Set (Var "IT")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rlvect_1 :::"RLSStruct"::: ) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v6_rlvect_1 :::"scalar-distributive"::: ) ) "iff" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "IT")) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "b")) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "v")) ")" ) ($#k1_algstr_0 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "v")) ")" ))))) ")" )); :: deftheorem defines :::"scalar-associative"::: RLVECT_1:def 7 : (Bool "for" (Set (Var "IT")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rlvect_1 :::"RLSStruct"::: ) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v7_rlvect_1 :::"scalar-associative"::: ) ) "iff" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "IT")) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "b")) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set (Var "b")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "v")) ")" ))))) ")" )); :: deftheorem defines :::"scalar-unital"::: RLVECT_1:def 8 : (Bool "for" (Set (Var "IT")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rlvect_1 :::"RLSStruct"::: ) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v8_rlvect_1 :::"scalar-unital"::: ) ) "iff" (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "IT")) "holds" (Bool (Set (Num 1) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set (Var "v")))) ")" )); definitionfunc :::"Trivial-RLSStruct"::: -> ($#v1_rlvect_1 :::"strict"::: ) ($#l1_rlvect_1 :::"RLSStruct"::: ) equals :: RLVECT_1:def 9 (Set ($#g1_rlvect_1 :::"RLSStruct"::: ) "(#" (Num 1) "," (Set ($#k5_funct_5 :::"op0"::: ) ) "," (Set ($#k9_funct_5 :::"op2"::: ) ) "," (Set "(" ($#k10_funct_3 :::"pr2"::: ) "(" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Num 1) ")" ")" ) "#)" ); end; :: deftheorem defines :::"Trivial-RLSStruct"::: RLVECT_1:def 9 : (Bool (Set ($#k2_rlvect_1 :::"Trivial-RLSStruct"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#g1_rlvect_1 :::"RLSStruct"::: ) "(#" (Num 1) "," (Set ($#k5_funct_5 :::"op0"::: ) ) "," (Set ($#k9_funct_5 :::"op2"::: ) ) "," (Set "(" ($#k10_funct_3 :::"pr2"::: ) "(" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Num 1) ")" ")" ) "#)" )); registration cluster (Set ($#k2_rlvect_1 :::"Trivial-RLSStruct"::: ) ) -> (Num 1) ($#v13_struct_0 :::"-element"::: ) ($#v1_rlvect_1 :::"strict"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_algstr_0 :::"strict"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) for ($#l1_algstr_0 :::"addMagma"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v8_algstr_0 :::"strict"::: ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) for ($#l2_algstr_0 :::"addLoopStr"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v1_rlvect_1 :::"strict"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v5_rlvect_1 :::"vector-distributive"::: ) ($#v6_rlvect_1 :::"scalar-distributive"::: ) ($#v7_rlvect_1 :::"scalar-associative"::: ) ($#v8_rlvect_1 :::"scalar-unital"::: ) for ($#l1_rlvect_1 :::"RLSStruct"::: ) ; end; definitionmode RealLinearSpace is ($#~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_rlvect_1 :::"vector-distributive"::: ) ($#v6_rlvect_1 :::"scalar-distributive"::: ) ($#v7_rlvect_1 :::"scalar-associative"::: ) ($#v8_rlvect_1 :::"scalar-unital"::: ) ($#l1_rlvect_1 :::"RLSStruct"::: ) ; end; definitionlet "V" be ($#v2_rlvect_1 :::"Abelian"::: ) ($#l1_algstr_0 :::"addMagma"::: ) ; let "v", "w" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "V")); :: original: :::"+"::: redefine func "v" :::"+"::: "w" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "V"); commutativity (Bool "for" (Set (Var "v")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Const "V")) "holds" (Bool (Set (Set (Var "v")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "w"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "w")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "v"))))) ; end; theorem :: RLVECT_1:3 (Bool "for" (Set (Var "V")) "being" ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) "holds" (Bool (Set (Var "V")) "is" ($#v6_algstr_0 :::"right_add-cancelable"::: ) )) ; theorem :: RLVECT_1:4 (Bool "for" (Set (Var "V")) "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 "v")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Set (Var "v")) ($#k1_algstr_0 :::"+"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "V")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "v"))) & (Bool (Set (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "V")) ")" ) ($#k1_algstr_0 :::"+"::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set (Var "v"))) ")" ))) ; definitionlet "V" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) ; let "v" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "V")); assume (Bool "(" (Bool (Set (Const "V")) "is" ($#v3_rlvect_1 :::"add-associative"::: ) ) & (Bool (Set (Const "V")) "is" ($#v4_rlvect_1 :::"right_zeroed"::: ) ) & (Bool (Set (Const "V")) "is" ($#v13_algstr_0 :::"right_complementable"::: ) ) ")" ) ; redefine func :::"-"::: "v" means :: RLVECT_1:def 10 (Bool (Set "v" ($#k1_algstr_0 :::"+"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) "V")); end; :: deftheorem defines :::"-"::: RLVECT_1:def 10 : (Bool "for" (Set (Var "V")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "V")) "is" ($#v3_rlvect_1 :::"add-associative"::: ) ) & (Bool (Set (Var "V")) "is" ($#v4_rlvect_1 :::"right_zeroed"::: ) ) & (Bool (Set (Var "V")) "is" ($#v13_algstr_0 :::"right_complementable"::: ) )) "holds" (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "V"))) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k4_algstr_0 :::"-"::: ) (Set (Var "v")))) "iff" (Bool (Set (Set (Var "v")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "V")))) ")" )))); definitionlet "V" be ($#l2_algstr_0 :::"addLoopStr"::: ) ; let "v", "w" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "V")); redefine func "v" :::"-"::: "w" equals :: RLVECT_1:def 11 (Set "v" ($#k1_algstr_0 :::"+"::: ) (Set "(" ($#k4_algstr_0 :::"-"::: ) "w" ")" )); end; :: deftheorem defines :::"-"::: RLVECT_1:def 11 : (Bool "for" (Set (Var "V")) "being" ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "v")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "holds" (Bool (Set (Set (Var "v")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "w"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "v")) ($#k1_algstr_0 :::"+"::: ) (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "w")) ")" ))))); theorem :: RLVECT_1:5 (Bool "for" (Set (Var "V")) "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 "v")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Set (Var "v")) ($#k1_algstr_0 :::"+"::: ) (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "v")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "V")))) & (Bool (Set (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "v")) ")" ) ($#k1_algstr_0 :::"+"::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "V")))) ")" ))) ; theorem :: RLVECT_1:6 (Bool "for" (Set (Var "V")) "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 "v")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Set (Var "v")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "w"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "V"))))) "holds" (Bool (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set ($#k4_algstr_0 :::"-"::: ) (Set (Var "w")))))) ; theorem :: RLVECT_1:7 (Bool "for" (Set (Var "V")) "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 "v")) "," (Set (Var "u")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) (Bool "ex" (Set (Var "w")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "st" (Bool (Set (Set (Var "v")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "w"))) ($#r1_hidden :::"="::: ) (Set (Var "u")))))) ; theorem :: RLVECT_1:8 (Bool "for" (Set (Var "V")) "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 "w")) "," (Set (Var "u")) "," (Set (Var "v1")) "," (Set (Var "v2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "st" (Bool (Bool "(" (Bool (Set (Set (Var "w")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "v1"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "w")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "v2")))) "or" (Bool (Set (Set (Var "v1")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "w"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "v2")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "w")))) ")" )) "holds" (Bool (Set (Var "v1")) ($#r1_hidden :::"="::: ) (Set (Var "v2"))))) ; theorem :: RLVECT_1:9 (Bool "for" (Set (Var "V")) "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 "v")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "st" (Bool (Bool "(" (Bool (Set (Set (Var "v")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "w"))) ($#r1_hidden :::"="::: ) (Set (Var "v"))) "or" (Bool (Set (Set (Var "w")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set (Var "v"))) ")" )) "holds" (Bool (Set (Var "w")) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "V")))))) ; theorem :: RLVECT_1:10 (Bool "for" (Set (Var "a")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) "or" (Bool (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "V")))) ")" )) "holds" (Bool (Set (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "V"))))))) ; theorem :: RLVECT_1:11 (Bool "for" (Set (Var "a")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "holds" (Bool "(" "not" (Bool (Set (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "V")))) "or" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) "or" (Bool (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "V")))) ")" )))) ; theorem :: RLVECT_1:12 (Bool "for" (Set (Var "V")) "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"::: ) "holds" (Bool (Set ($#k4_algstr_0 :::"-"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "V")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "V"))))) ; theorem :: RLVECT_1:13 (Bool "for" (Set (Var "V")) "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 "v")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "holds" (Bool (Set (Set (Var "v")) ($#k5_algstr_0 :::"-"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "V")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "v"))))) ; theorem :: RLVECT_1:14 (Bool "for" (Set (Var "V")) "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 "v")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "holds" (Bool (Set (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "V")) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set ($#k4_algstr_0 :::"-"::: ) (Set (Var "v")))))) ; theorem :: RLVECT_1:15 (Bool "for" (Set (Var "V")) "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 "v")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "holds" (Bool (Set (Set (Var "v")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "V")))))) ; theorem :: RLVECT_1:16 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "holds" (Bool (Set ($#k4_algstr_0 :::"-"::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "v")))))) ; theorem :: RLVECT_1:17 (Bool "for" (Set (Var "V")) "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 "v")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "holds" (Bool (Set ($#k4_algstr_0 :::"-"::: ) (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "v")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "v"))))) ; theorem :: RLVECT_1:18 (Bool "for" (Set (Var "V")) "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 "v")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set ($#k4_algstr_0 :::"-"::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set ($#k4_algstr_0 :::"-"::: ) (Set (Var "w"))))) "holds" (Bool (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set (Var "w"))))) ; theorem :: RLVECT_1:19 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set ($#k4_algstr_0 :::"-"::: ) (Set (Var "v"))))) "holds" (Bool (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "V")))))) ; theorem :: RLVECT_1:20 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Set (Var "v")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "V"))))) "holds" (Bool (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "V")))))) ; theorem :: RLVECT_1:21 (Bool "for" (Set (Var "V")) "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 "v")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Set (Var "v")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "w"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "V"))))) "holds" (Bool (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set (Var "w"))))) ; theorem :: RLVECT_1:22 (Bool "for" (Set (Var "V")) "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 "u")) "," (Set (Var "v")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) (Bool "ex" (Set (Var "w")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "st" (Bool (Set (Set (Var "v")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "w"))) ($#r1_hidden :::"="::: ) (Set (Var "u")))))) ; theorem :: RLVECT_1:23 (Bool "for" (Set (Var "V")) "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 "w")) "," (Set (Var "v1")) "," (Set (Var "v2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Set (Var "w")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "v1"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "w")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "v2"))))) "holds" (Bool (Set (Var "v1")) ($#r1_hidden :::"="::: ) (Set (Var "v2"))))) ; theorem :: RLVECT_1:24 (Bool "for" (Set (Var "a")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "holds" (Bool (Set (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "v")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Set (Var "a")) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "v"))))))) ; theorem :: RLVECT_1:25 (Bool "for" (Set (Var "a")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "holds" (Bool (Set (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "v")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_algstr_0 :::"-"::: ) (Set "(" (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "v")) ")" )))))) ; theorem :: RLVECT_1:26 (Bool "for" (Set (Var "a")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "holds" (Bool (Set (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Set (Var "a")) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "v")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "v"))))))) ; theorem :: RLVECT_1:27 (Bool "for" (Set (Var "V")) "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 "v")) "," (Set (Var "u")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "holds" (Bool (Set (Set (Var "v")) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "u")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "w")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "v")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "w")) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set (Var "u")))))) ; theorem :: RLVECT_1:28 (Bool "for" (Set (Var "V")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "v")) "," (Set (Var "u")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "holds" (Bool (Set (Set "(" (Set (Var "v")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "u")) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set (Var "w"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "v")) ($#k1_algstr_0 :::"+"::: ) (Set "(" (Set (Var "u")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "w")) ")" ))))) ; theorem :: RLVECT_1:29 (Bool "for" (Set (Var "V")) "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 "v")) "," (Set (Var "u")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "holds" (Bool (Set (Set (Var "v")) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "u")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "w")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "v")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "u")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "w")))))) ; theorem :: RLVECT_1:30 (Bool "for" (Set (Var "V")) "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 "v")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "holds" (Bool (Set ($#k4_algstr_0 :::"-"::: ) (Set "(" (Set (Var "v")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "w")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "w")) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set (Var "v")))))) ; theorem :: RLVECT_1:31 (Bool "for" (Set (Var "V")) "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 "v")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "holds" (Bool (Set ($#k4_algstr_0 :::"-"::: ) (Set "(" (Set (Var "v")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "w")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "w")) ")" ) ($#k1_algstr_0 :::"+"::: ) (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "v")) ")" ))))) ; theorem :: RLVECT_1:32 (Bool "for" (Set (Var "V")) "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 "v")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "holds" (Bool (Set (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "v")) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set (Var "w"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "w")) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set (Var "v")))))) ; theorem :: RLVECT_1:33 (Bool "for" (Set (Var "V")) "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 "v")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "holds" (Bool (Set ($#k4_algstr_0 :::"-"::: ) (Set "(" (Set (Var "v")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "w")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "w")) ($#k1_algstr_0 :::"+"::: ) (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "v")) ")" ))))) ; theorem :: RLVECT_1:34 (Bool "for" (Set (Var "a")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "v")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "holds" (Bool (Set (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set (Var "v")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "w")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "v")) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "w")) ")" )))))) ; theorem :: RLVECT_1:35 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "b")) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "v")) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "b")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "v")) ")" )))))) ; theorem :: RLVECT_1:36 (Bool "for" (Set (Var "a")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "v")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "w"))))) "holds" (Bool (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set (Var "w")))))) ; theorem :: RLVECT_1:37 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "v")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "V")))) & (Bool (Set (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "b")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "v"))))) "holds" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "b")))))) ; definitionlet "V" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) ; let "F" be (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "V"))) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"FinSequence":::); func :::"Sum"::: "F" -> ($#m1_subset_1 :::"Element":::) "of" "V" means :: RLVECT_1:def 12 (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," "V" "st" (Bool "(" (Bool it ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k8_nat_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) "F" ")" ))) & (Bool (Set (Set (Var "f")) ($#k8_nat_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) "V")) & (Bool "(" "for" (Set (Var "j")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element":::) "of" "V" "st" (Bool (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) "F")) & (Bool (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set "F" ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "j")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )))) "holds" (Bool (Set (Set (Var "f")) ($#k8_nat_1 :::"."::: ) (Set "(" (Set (Var "j")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k8_nat_1 :::"."::: ) (Set (Var "j")) ")" ) ($#k1_algstr_0 :::"+"::: ) (Set (Var "v"))))) ")" ) ")" )); end; :: deftheorem defines :::"Sum"::: RLVECT_1:def 12 : (Bool "for" (Set (Var "V")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "F")) "being" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "b1"))) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set (Var "F")))) "iff" (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set (Var "V")) "st" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k8_nat_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "F")) ")" ))) & (Bool (Set (Set (Var "f")) ($#k8_nat_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "V")))) & (Bool "(" "for" (Set (Var "j")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "F")))) & (Bool (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "j")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )))) "holds" (Bool (Set (Set (Var "f")) ($#k8_nat_1 :::"."::: ) (Set "(" (Set (Var "j")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k8_nat_1 :::"."::: ) (Set (Var "j")) ")" ) ($#k1_algstr_0 :::"+"::: ) (Set (Var "v"))))) ")" ) ")" )) ")" )))); theorem :: RLVECT_1:38 (Bool "for" (Set (Var "V")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "G")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1))) & (Bool (Set (Var "G")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k5_relat_1 :::"|"::: ) (Set "(" ($#k4_finseq_1 :::"dom"::: ) (Set (Var "G")) ")" ))) & (Bool (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "F")) ")" )))) "holds" (Bool (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_rlvect_1 :::"Sum"::: ) (Set (Var "G")) ")" ) ($#k1_algstr_0 :::"+"::: ) (Set (Var "v"))))))) ; theorem :: RLVECT_1:39 (Bool "for" (Set (Var "a")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "G")))) & (Bool "(" "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "F")))) & (Bool (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))))) "holds" (Bool (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "v"))))) ")" )) "holds" (Bool (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set "(" ($#k4_rlvect_1 :::"Sum"::: ) (Set (Var "G")) ")" )))))) ; theorem :: RLVECT_1:40 (Bool "for" (Set (Var "V")) "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 "F")) "," (Set (Var "G")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "G")))) & (Bool "(" "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "F")))) & (Bool (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))))) "holds" (Bool (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set ($#k4_algstr_0 :::"-"::: ) (Set (Var "v"))))) ")" )) "holds" (Bool (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#k4_algstr_0 :::"-"::: ) (Set "(" ($#k4_rlvect_1 :::"Sum"::: ) (Set (Var "G")) ")" ))))) ; theorem :: RLVECT_1:41 (Bool "for" (Set (Var "V")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "V")) "holds" (Bool (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set "(" (Set (Var "F")) ($#k8_finseq_1 :::"^"::: ) (Set (Var "G")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_rlvect_1 :::"Sum"::: ) (Set (Var "F")) ")" ) ($#k1_algstr_0 :::"+"::: ) (Set "(" ($#k4_rlvect_1 :::"Sum"::: ) (Set (Var "G")) ")" ))))) ; theorem :: RLVECT_1:42 (Bool "for" (Set (Var "V")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "G")))) & (Bool (Set (Var "F")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool (Set (Var "G")) "is" ($#v2_funct_1 :::"one-to-one"::: ) )) "holds" (Bool (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set (Var "G")))))) ; theorem :: RLVECT_1:43 (Bool "for" (Set (Var "V")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) "holds" (Bool (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set "(" ($#k6_finseq_1 :::"<*>"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "V"))) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "V"))))) ; theorem :: RLVECT_1:44 (Bool "for" (Set (Var "V")) "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 "v")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "holds" (Bool (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "v")) ($#k12_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "v"))))) ; theorem :: RLVECT_1:45 (Bool "for" (Set (Var "V")) "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 "v")) "," (Set (Var "u")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "holds" (Bool (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set ($#k2_finseq_4 :::"<*"::: ) (Set (Var "v")) "," (Set (Var "u")) ($#k2_finseq_4 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set (Var "v")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "u")))))) ; theorem :: RLVECT_1:46 (Bool "for" (Set (Var "V")) "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 "v")) "," (Set (Var "u")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "holds" (Bool (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set ($#k3_finseq_4 :::"<*"::: ) (Set (Var "v")) "," (Set (Var "u")) "," (Set (Var "w")) ($#k3_finseq_4 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "v")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "u")) ")" ) ($#k1_algstr_0 :::"+"::: ) (Set (Var "w")))))) ; theorem :: RLVECT_1:47 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool (Set (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set "(" ($#k4_rlvect_1 :::"Sum"::: ) (Set "(" ($#k6_finseq_1 :::"<*>"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "V"))) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "V")))))) ; theorem :: RLVECT_1:48 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "v")) "," (Set (Var "u")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "holds" (Bool (Set (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set "(" ($#k4_rlvect_1 :::"Sum"::: ) (Set ($#k2_finseq_4 :::"<*"::: ) (Set (Var "v")) "," (Set (Var "u")) ($#k2_finseq_4 :::"*>"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "v")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "u")) ")" )))))) ; theorem :: RLVECT_1:49 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "v")) "," (Set (Var "u")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "holds" (Bool (Set (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set "(" ($#k4_rlvect_1 :::"Sum"::: ) (Set ($#k3_finseq_4 :::"<*"::: ) (Set (Var "v")) "," (Set (Var "u")) "," (Set (Var "w")) ($#k3_finseq_4 :::"*>"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "v")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "u")) ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "w")) ")" )))))) ; theorem :: RLVECT_1:50 (Bool "for" (Set (Var "V")) "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"::: ) "holds" (Bool (Set ($#k4_algstr_0 :::"-"::: ) (Set "(" ($#k4_rlvect_1 :::"Sum"::: ) (Set "(" ($#k6_finseq_1 :::"<*>"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "V"))) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "V"))))) ; theorem :: RLVECT_1:51 (Bool "for" (Set (Var "V")) "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 "v")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "holds" (Bool (Set ($#k4_algstr_0 :::"-"::: ) (Set "(" ($#k4_rlvect_1 :::"Sum"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "v")) ($#k12_finseq_1 :::"*>"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_algstr_0 :::"-"::: ) (Set (Var "v")))))) ; theorem :: RLVECT_1:52 (Bool "for" (Set (Var "V")) "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 "v")) "," (Set (Var "u")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "holds" (Bool (Set ($#k4_algstr_0 :::"-"::: ) (Set "(" ($#k4_rlvect_1 :::"Sum"::: ) (Set ($#k2_finseq_4 :::"<*"::: ) (Set (Var "v")) "," (Set (Var "u")) ($#k2_finseq_4 :::"*>"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "v")) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set (Var "u")))))) ; theorem :: RLVECT_1:53 (Bool "for" (Set (Var "V")) "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 "v")) "," (Set (Var "u")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "holds" (Bool (Set ($#k4_algstr_0 :::"-"::: ) (Set "(" ($#k4_rlvect_1 :::"Sum"::: ) (Set ($#k3_finseq_4 :::"<*"::: ) (Set (Var "v")) "," (Set (Var "u")) "," (Set (Var "w")) ($#k3_finseq_4 :::"*>"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "v")) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set (Var "u")) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set (Var "w")))))) ; theorem :: RLVECT_1:54 (Bool "for" (Set (Var "V")) "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 "v")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "holds" (Bool (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set ($#k2_finseq_4 :::"<*"::: ) (Set (Var "v")) "," (Set (Var "w")) ($#k2_finseq_4 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set ($#k2_finseq_4 :::"<*"::: ) (Set (Var "w")) "," (Set (Var "v")) ($#k2_finseq_4 :::"*>"::: ) ))))) ; theorem :: RLVECT_1:55 (Bool "for" (Set (Var "V")) "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 "v")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "holds" (Bool (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set ($#k2_finseq_4 :::"<*"::: ) (Set (Var "v")) "," (Set (Var "w")) ($#k2_finseq_4 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_rlvect_1 :::"Sum"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "v")) ($#k12_finseq_1 :::"*>"::: ) ) ")" ) ($#k1_algstr_0 :::"+"::: ) (Set "(" ($#k4_rlvect_1 :::"Sum"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "w")) ($#k12_finseq_1 :::"*>"::: ) ) ")" ))))) ; theorem :: RLVECT_1:56 canceled; theorem :: RLVECT_1:57 (Bool "for" (Set (Var "V")) "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 "v")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set ($#k2_finseq_4 :::"<*"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "V")) ")" ) "," (Set (Var "v")) ($#k2_finseq_4 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "v"))) & (Bool (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set ($#k2_finseq_4 :::"<*"::: ) (Set (Var "v")) "," (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "V")) ")" ) ($#k2_finseq_4 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "v"))) ")" ))) ; theorem :: RLVECT_1:58 (Bool "for" (Set (Var "V")) "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 "v")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set ($#k2_finseq_4 :::"<*"::: ) (Set (Var "v")) "," (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "v")) ")" ) ($#k2_finseq_4 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "V")))) & (Bool (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set ($#k2_finseq_4 :::"<*"::: ) (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "v")) ")" ) "," (Set (Var "v")) ($#k2_finseq_4 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "V")))) ")" ))) ; theorem :: RLVECT_1:59 (Bool "for" (Set (Var "V")) "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 "v")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "holds" (Bool (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set ($#k2_finseq_4 :::"<*"::: ) (Set (Var "v")) "," (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "w")) ")" ) ($#k2_finseq_4 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set (Var "v")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "w")))))) ; theorem :: RLVECT_1:60 (Bool "for" (Set (Var "V")) "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 "v")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "holds" (Bool (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set ($#k2_finseq_4 :::"<*"::: ) (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "v")) ")" ) "," (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "w")) ")" ) ($#k2_finseq_4 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k4_algstr_0 :::"-"::: ) (Set "(" (Set (Var "w")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "v")) ")" ))))) ; theorem :: RLVECT_1:61 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "holds" (Bool (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set ($#k2_finseq_4 :::"<*"::: ) (Set (Var "v")) "," (Set (Var "v")) ($#k2_finseq_4 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Num 2) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "v")))))) ; theorem :: RLVECT_1:62 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "holds" (Bool (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set ($#k2_finseq_4 :::"<*"::: ) (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "v")) ")" ) "," (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "v")) ")" ) ($#k2_finseq_4 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_real_1 :::"-"::: ) (Num 2) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "v")))))) ; theorem :: RLVECT_1:63 (Bool "for" (Set (Var "V")) "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 "u")) "," (Set (Var "v")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "holds" (Bool (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set ($#k3_finseq_4 :::"<*"::: ) (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "w")) ($#k3_finseq_4 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k4_rlvect_1 :::"Sum"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "u")) ($#k12_finseq_1 :::"*>"::: ) ) ")" ) ($#k1_algstr_0 :::"+"::: ) (Set "(" ($#k4_rlvect_1 :::"Sum"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "v")) ($#k12_finseq_1 :::"*>"::: ) ) ")" ) ")" ) ($#k1_algstr_0 :::"+"::: ) (Set "(" ($#k4_rlvect_1 :::"Sum"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "w")) ($#k12_finseq_1 :::"*>"::: ) ) ")" ))))) ; theorem :: RLVECT_1:64 (Bool "for" (Set (Var "V")) "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 "u")) "," (Set (Var "v")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "holds" (Bool (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set ($#k3_finseq_4 :::"<*"::: ) (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "w")) ($#k3_finseq_4 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_rlvect_1 :::"Sum"::: ) (Set ($#k2_finseq_4 :::"<*"::: ) (Set (Var "u")) "," (Set (Var "v")) ($#k2_finseq_4 :::"*>"::: ) ) ")" ) ($#k1_algstr_0 :::"+"::: ) (Set (Var "w")))))) ; theorem :: RLVECT_1:65 (Bool "for" (Set (Var "V")) "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 "v")) "," (Set (Var "u")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "holds" (Bool (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set ($#k3_finseq_4 :::"<*"::: ) (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "w")) ($#k3_finseq_4 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_rlvect_1 :::"Sum"::: ) (Set ($#k2_finseq_4 :::"<*"::: ) (Set (Var "v")) "," (Set (Var "w")) ($#k2_finseq_4 :::"*>"::: ) ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "u")))))) ; theorem :: RLVECT_1:66 (Bool "for" (Set (Var "V")) "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 "v")) "," (Set (Var "u")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "holds" (Bool (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set ($#k3_finseq_4 :::"<*"::: ) (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "w")) ($#k3_finseq_4 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_rlvect_1 :::"Sum"::: ) (Set ($#k2_finseq_4 :::"<*"::: ) (Set (Var "u")) "," (Set (Var "w")) ($#k2_finseq_4 :::"*>"::: ) ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "v")))))) ; theorem :: RLVECT_1:67 (Bool "for" (Set (Var "V")) "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 "v")) "," (Set (Var "u")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "holds" (Bool (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set ($#k3_finseq_4 :::"<*"::: ) (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "w")) ($#k3_finseq_4 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set ($#k3_finseq_4 :::"<*"::: ) (Set (Var "u")) "," (Set (Var "w")) "," (Set (Var "v")) ($#k3_finseq_4 :::"*>"::: ) ))))) ; theorem :: RLVECT_1:68 (Bool "for" (Set (Var "V")) "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 "v")) "," (Set (Var "u")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "holds" (Bool (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set ($#k3_finseq_4 :::"<*"::: ) (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "w")) ($#k3_finseq_4 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set ($#k3_finseq_4 :::"<*"::: ) (Set (Var "v")) "," (Set (Var "u")) "," (Set (Var "w")) ($#k3_finseq_4 :::"*>"::: ) ))))) ; theorem :: RLVECT_1:69 (Bool "for" (Set (Var "V")) "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 "v")) "," (Set (Var "u")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "holds" (Bool (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set ($#k3_finseq_4 :::"<*"::: ) (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "w")) ($#k3_finseq_4 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set ($#k3_finseq_4 :::"<*"::: ) (Set (Var "v")) "," (Set (Var "w")) "," (Set (Var "u")) ($#k3_finseq_4 :::"*>"::: ) ))))) ; theorem :: RLVECT_1:70 (Bool "for" (Set (Var "V")) "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 "v")) "," (Set (Var "u")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "holds" (Bool (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set ($#k3_finseq_4 :::"<*"::: ) (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "w")) ($#k3_finseq_4 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set ($#k3_finseq_4 :::"<*"::: ) (Set (Var "w")) "," (Set (Var "v")) "," (Set (Var "u")) ($#k3_finseq_4 :::"*>"::: ) ))))) ; theorem :: RLVECT_1:71 canceled; theorem :: RLVECT_1:72 (Bool "for" (Set (Var "V")) "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 "v")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set ($#k3_finseq_4 :::"<*"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "V")) ")" ) "," (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "V")) ")" ) "," (Set (Var "v")) ($#k3_finseq_4 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "v"))) & (Bool (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set ($#k3_finseq_4 :::"<*"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "V")) ")" ) "," (Set (Var "v")) "," (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "V")) ")" ) ($#k3_finseq_4 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "v"))) & (Bool (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set ($#k3_finseq_4 :::"<*"::: ) (Set (Var "v")) "," (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "V")) ")" ) "," (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "V")) ")" ) ($#k3_finseq_4 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "v"))) ")" ))) ; theorem :: RLVECT_1:73 (Bool "for" (Set (Var "V")) "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 "u")) "," (Set (Var "v")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set ($#k3_finseq_4 :::"<*"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "V")) ")" ) "," (Set (Var "u")) "," (Set (Var "v")) ($#k3_finseq_4 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set (Var "u")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "v")))) & (Bool (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set ($#k3_finseq_4 :::"<*"::: ) (Set (Var "u")) "," (Set (Var "v")) "," (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "V")) ")" ) ($#k3_finseq_4 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set (Var "u")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "v")))) & (Bool (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set ($#k3_finseq_4 :::"<*"::: ) (Set (Var "u")) "," (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "V")) ")" ) "," (Set (Var "v")) ($#k3_finseq_4 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set (Var "u")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "v")))) ")" ))) ; theorem :: RLVECT_1:74 (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "holds" (Bool (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set ($#k3_finseq_4 :::"<*"::: ) (Set (Var "v")) "," (Set (Var "v")) "," (Set (Var "v")) ($#k3_finseq_4 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Num 3) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "v")))))) ; theorem :: RLVECT_1:75 (Bool "for" (Set (Var "V")) "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 "F")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "V")))))) ; theorem :: RLVECT_1:76 (Bool "for" (Set (Var "V")) "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 "F")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Num 1))) "holds" (Bool (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Num 1))))) ; theorem :: RLVECT_1:77 (Bool "for" (Set (Var "V")) "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 "F")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "v1")) "," (Set (Var "v2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Num 2)) & (Bool (Set (Var "v1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Num 1))) & (Bool (Set (Var "v2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Num 2)))) "holds" (Bool (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "v1")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "v2"))))))) ; theorem :: RLVECT_1:78 (Bool "for" (Set (Var "V")) "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 "F")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "V")) (Bool "for" (Set (Var "v1")) "," (Set (Var "v2")) "," (Set (Var "v")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Num 3)) & (Bool (Set (Var "v1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Num 1))) & (Bool (Set (Var "v2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Num 2))) & (Bool (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Num 3)))) "holds" (Bool (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "v1")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "v2")) ")" ) ($#k1_algstr_0 :::"+"::: ) (Set (Var "v"))))))) ; begin definitionlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) ; attr "L" is :::"zeroed"::: means :: RLVECT_1:def 13 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" "L" "holds" (Bool "(" (Bool (Set (Set (Var "a")) ($#k1_algstr_0 :::"+"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) "L" ")" )) ($#r1_hidden :::"="::: ) (Set (Var "a"))) & (Bool (Set (Set "(" ($#k4_struct_0 :::"0."::: ) "L" ")" ) ($#k1_algstr_0 :::"+"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Var "a"))) ")" )); end; :: deftheorem defines :::"zeroed"::: RLVECT_1:def 13 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) "holds" (Bool "(" (Bool (Set (Var "L")) "is" ($#v9_rlvect_1 :::"zeroed"::: ) ) "iff" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Set (Var "a")) ($#k1_algstr_0 :::"+"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "L")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "a"))) & (Bool (Set (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "L")) ")" ) ($#k1_algstr_0 :::"+"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Var "a"))) ")" )) ")" )); registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v9_rlvect_1 :::"zeroed"::: ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_rlvect_1 :::"right_zeroed"::: ) for ($#l2_algstr_0 :::"addLoopStr"::: ) ; end; 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"::: ) ) ($#v9_rlvect_1 :::"zeroed"::: ) for ($#l2_algstr_0 :::"addLoopStr"::: ) ; cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v12_algstr_0 :::"left_complementable"::: ) for ($#l2_algstr_0 :::"addLoopStr"::: ) ; end; theorem :: RLVECT_1:79 (Bool "for" (Set (Var "a")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "V")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"VECTOR":::) "of" (Set (Var "V")) "holds" (Bool (Set (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Set (Var "a")) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set ($#k4_algstr_0 :::"-"::: ) (Set "(" (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "v")) ")" )))))) ; begin theorem :: RLVECT_1:80 (Bool "for" (Set (Var "V")) "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 ($#k4_algstr_0 :::"-"::: ) (Set "(" ($#k4_rlvect_1 :::"Sum"::: ) (Set "(" ($#k6_finseq_1 :::"<*>"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "V"))) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "V"))))) ; theorem :: RLVECT_1:81 (Bool "for" (Set (Var "V")) "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 "v")) "," (Set (Var "u")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "holds" (Bool (Set ($#k4_algstr_0 :::"-"::: ) (Set "(" ($#k4_rlvect_1 :::"Sum"::: ) (Set ($#k2_finseq_4 :::"<*"::: ) (Set (Var "v")) "," (Set (Var "u")) ($#k2_finseq_4 :::"*>"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "v")) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set (Var "u")))))) ; theorem :: RLVECT_1:82 (Bool "for" (Set (Var "V")) "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 "v")) "," (Set (Var "u")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "holds" (Bool (Set ($#k4_algstr_0 :::"-"::: ) (Set "(" ($#k4_rlvect_1 :::"Sum"::: ) (Set ($#k3_finseq_4 :::"<*"::: ) (Set (Var "v")) "," (Set (Var "u")) "," (Set (Var "w")) ($#k3_finseq_4 :::"*>"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "v")) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set (Var "u")) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set (Var "w")))))) ; theorem :: RLVECT_1:83 (Bool "for" (Set (Var "V")) "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 "v")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set ($#k2_finseq_4 :::"<*"::: ) (Set (Var "v")) "," (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "v")) ")" ) ($#k2_finseq_4 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "V")))) & (Bool (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set ($#k2_finseq_4 :::"<*"::: ) (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "v")) ")" ) "," (Set (Var "v")) ($#k2_finseq_4 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "V")))) ")" ))) ; theorem :: RLVECT_1:84 (Bool "for" (Set (Var "V")) "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 "v")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set ($#k2_finseq_4 :::"<*"::: ) (Set (Var "v")) "," (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "w")) ")" ) ($#k2_finseq_4 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set (Var "v")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "w")))) & (Bool (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set ($#k2_finseq_4 :::"<*"::: ) (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "w")) ")" ) "," (Set (Var "v")) ($#k2_finseq_4 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set (Var "v")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "w")))) ")" ))) ; theorem :: RLVECT_1:85 (Bool "for" (Set (Var "V")) "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 "v")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "V")) "holds" (Bool "(" (Bool (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set ($#k2_finseq_4 :::"<*"::: ) (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "v")) ")" ) "," (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "w")) ")" ) ($#k2_finseq_4 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k4_algstr_0 :::"-"::: ) (Set "(" (Set (Var "v")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "w")) ")" ))) & (Bool (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set ($#k2_finseq_4 :::"<*"::: ) (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "w")) ")" ) "," (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "v")) ")" ) ($#k2_finseq_4 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k4_algstr_0 :::"-"::: ) (Set "(" (Set (Var "v")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "w")) ")" ))) ")" ))) ;