:: PRVECT_3 semantic presentation begin theorem :: PRVECT_3:1 (Bool "for" (Set (Var "D")) "," (Set (Var "E")) "," (Set (Var "F")) "," (Set (Var "G")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "ex" (Set (Var "I")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "D")) "," (Set (Var "E")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "F")) "," (Set (Var "G")) ($#k2_zfmisc_1 :::":]"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "D")) "," (Set (Var "F")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "E")) "," (Set (Var "G")) ($#k2_zfmisc_1 :::":]"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) "st" (Bool "(" (Bool (Set (Var "I")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool (Set (Var "I")) "is" ($#v2_funct_2 :::"onto"::: ) ) & (Bool "(" "for" (Set (Var "d")) "," (Set (Var "e")) "," (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "d")) ($#r2_hidden :::"in"::: ) (Set (Var "D"))) & (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set (Var "E"))) & (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set (Var "F"))) & (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set (Var "G")))) "holds" (Bool (Set (Set (Var "I")) ($#k1_binop_1 :::"."::: ) "(" (Set ($#k4_tarski :::"["::: ) (Set (Var "d")) "," (Set (Var "e")) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set (Var "f")) "," (Set (Var "g")) ($#k4_tarski :::"]"::: ) ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "d")) "," (Set (Var "f")) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set (Var "e")) "," (Set (Var "g")) ($#k4_tarski :::"]"::: ) ) ($#k4_tarski :::"]"::: ) )) ")" ) ")" ))) ; theorem :: PRVECT_3:2 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "D")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "D"))) ($#r1_hidden :::"="::: ) (Set ($#k6_domain_1 :::"{"::: ) (Num 1) ($#k6_domain_1 :::"}"::: ) )) & (Bool (Set (Set (Var "D")) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Var "X")))) "holds" (Bool "ex" (Set (Var "I")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set "(" ($#k4_card_3 :::"product"::: ) (Set (Var "D")) ")" ) "st" (Bool "(" (Bool (Set (Var "I")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool (Set (Var "I")) "is" ($#v2_funct_2 :::"onto"::: ) ) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Set (Var "I")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "x")) ($#k9_finseq_1 :::"*>"::: ) )) ")" ) ")" )))) ; theorem :: PRVECT_3:3 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "D")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "D"))) ($#r1_hidden :::"="::: ) (Set ($#k7_domain_1 :::"{"::: ) (Num 1) "," (Num 2) ($#k7_domain_1 :::"}"::: ) )) & (Bool (Set (Set (Var "D")) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Var "X"))) & (Bool (Set (Set (Var "D")) ($#k1_funct_1 :::"."::: ) (Num 2)) ($#r1_hidden :::"="::: ) (Set (Var "Y")))) "holds" (Bool "ex" (Set (Var "I")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "(" ($#k4_card_3 :::"product"::: ) (Set (Var "D")) ")" ) "st" (Bool "(" (Bool (Set (Var "I")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool (Set (Var "I")) "is" ($#v2_funct_2 :::"onto"::: ) ) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "Y")))) "holds" (Bool (Set (Set (Var "I")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) )) ")" ) ")" )))) ; theorem :: PRVECT_3:4 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "ex" (Set (Var "I")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set "(" ($#k4_card_3 :::"product"::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "X")) ($#k9_finseq_1 :::"*>"::: ) ) ")" ) "st" (Bool "(" (Bool (Set (Var "I")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool (Set (Var "I")) "is" ($#v2_funct_2 :::"onto"::: ) ) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Set (Var "I")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "x")) ($#k9_finseq_1 :::"*>"::: ) )) ")" ) ")" ))) ; registrationlet "X", "Y" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_relat_1 :::"non-empty"::: ) ($#m1_hidden :::"FinSequence":::); cluster (Set "X" ($#k7_finseq_1 :::"^"::: ) "Y") -> ($#v2_relat_1 :::"non-empty"::: ) ; end; theorem :: PRVECT_3:5 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "ex" (Set (Var "I")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "(" ($#k4_card_3 :::"product"::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k10_finseq_1 :::"*>"::: ) ) ")" ) "st" (Bool "(" (Bool (Set (Var "I")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool (Set (Var "I")) "is" ($#v2_funct_2 :::"onto"::: ) ) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "Y")))) "holds" (Bool (Set (Set (Var "I")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) )) ")" ) ")" ))) ; theorem :: PRVECT_3:6 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_relat_1 :::"non-empty"::: ) ($#m1_hidden :::"FinSequence":::) (Bool "ex" (Set (Var "I")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k4_card_3 :::"product"::: ) (Set (Var "X")) ")" ) "," (Set "(" ($#k4_card_3 :::"product"::: ) (Set (Var "Y")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "(" ($#k4_card_3 :::"product"::: ) (Set "(" (Set (Var "X")) ($#k7_finseq_1 :::"^"::: ) (Set (Var "Y")) ")" ) ")" ) "st" (Bool "(" (Bool (Set (Var "I")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool (Set (Var "I")) "is" ($#v2_funct_2 :::"onto"::: ) ) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k4_card_3 :::"product"::: ) (Set (Var "X")))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k4_card_3 :::"product"::: ) (Set (Var "Y"))))) "holds" (Bool (Set (Set (Var "I")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k7_finseq_1 :::"^"::: ) (Set (Var "y")))) ")" ) ")" ))) ; definitionlet "G", "F" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) ; func :::"prod_ADD"::: "(" "G" "," "F" ")" -> ($#m1_subset_1 :::"BinOp":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "G") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "F") ($#k2_zfmisc_1 :::":]"::: ) ) means :: PRVECT_3:def 1 (Bool "for" (Set (Var "g1")) "," (Set (Var "g2")) "being" ($#m1_subset_1 :::"Point":::) "of" "G" (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_subset_1 :::"Point":::) "of" "F" "holds" (Bool (Set it ($#k5_binop_1 :::"."::: ) "(" (Set ($#k1_domain_1 :::"["::: ) (Set (Var "g1")) "," (Set (Var "f1")) ($#k1_domain_1 :::"]"::: ) ) "," (Set ($#k1_domain_1 :::"["::: ) (Set (Var "g2")) "," (Set (Var "f2")) ($#k1_domain_1 :::"]"::: ) ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set "(" (Set (Var "g1")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "g2")) ")" ) "," (Set "(" (Set (Var "f1")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "f2")) ")" ) ($#k1_domain_1 :::"]"::: ) )))); end; :: deftheorem defines :::"prod_ADD"::: PRVECT_3:def 1 : (Bool "for" (Set (Var "G")) "," (Set (Var "F")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "F"))) ($#k2_zfmisc_1 :::":]"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k1_prvect_3 :::"prod_ADD"::: ) "(" (Set (Var "G")) "," (Set (Var "F")) ")" )) "iff" (Bool "for" (Set (Var "g1")) "," (Set (Var "g2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "F")) "holds" (Bool (Set (Set (Var "b3")) ($#k5_binop_1 :::"."::: ) "(" (Set ($#k1_domain_1 :::"["::: ) (Set (Var "g1")) "," (Set (Var "f1")) ($#k1_domain_1 :::"]"::: ) ) "," (Set ($#k1_domain_1 :::"["::: ) (Set (Var "g2")) "," (Set (Var "f2")) ($#k1_domain_1 :::"]"::: ) ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set "(" (Set (Var "g1")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "g2")) ")" ) "," (Set "(" (Set (Var "f1")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "f2")) ")" ) ($#k1_domain_1 :::"]"::: ) )))) ")" ))); definitionlet "G", "F" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rlvect_1 :::"RLSStruct"::: ) ; func :::"prod_MLT"::: "(" "G" "," "F" ")" -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "G") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "F") ($#k2_zfmisc_1 :::":]"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "G") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "F") ($#k2_zfmisc_1 :::":]"::: ) ) means :: PRVECT_3:def 2 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Point":::) "of" "G" (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Point":::) "of" "F" "holds" (Bool (Set it ($#k2_binop_1 :::"."::: ) "(" (Set (Var "r")) "," (Set ($#k1_domain_1 :::"["::: ) (Set (Var "g")) "," (Set (Var "f")) ($#k1_domain_1 :::"]"::: ) ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set "(" (Set (Var "r")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "g")) ")" ) "," (Set "(" (Set (Var "r")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "f")) ")" ) ($#k1_domain_1 :::"]"::: ) ))))); end; :: deftheorem defines :::"prod_MLT"::: PRVECT_3:def 2 : (Bool "for" (Set (Var "G")) "," (Set (Var "F")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rlvect_1 :::"RLSStruct"::: ) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "F"))) ($#k2_zfmisc_1 :::":]"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "F"))) ($#k2_zfmisc_1 :::":]"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k2_prvect_3 :::"prod_MLT"::: ) "(" (Set (Var "G")) "," (Set (Var "F")) ")" )) "iff" (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "F")) "holds" (Bool (Set (Set (Var "b3")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "r")) "," (Set ($#k1_domain_1 :::"["::: ) (Set (Var "g")) "," (Set (Var "f")) ($#k1_domain_1 :::"]"::: ) ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set "(" (Set (Var "r")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "g")) ")" ) "," (Set "(" (Set (Var "r")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "f")) ")" ) ($#k1_domain_1 :::"]"::: ) ))))) ")" ))); definitionlet "G", "F" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) ; func :::"prod_ZERO"::: "(" "G" "," "F" ")" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "G") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "F") ($#k2_zfmisc_1 :::":]"::: ) ) equals :: PRVECT_3:def 3 (Set ($#k1_domain_1 :::"["::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) "G" ")" ) "," (Set "(" ($#k4_struct_0 :::"0."::: ) "F" ")" ) ($#k1_domain_1 :::"]"::: ) ); end; :: deftheorem defines :::"prod_ZERO"::: PRVECT_3:def 3 : (Bool "for" (Set (Var "G")) "," (Set (Var "F")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) "holds" (Bool (Set ($#k3_prvect_3 :::"prod_ZERO"::: ) "(" (Set (Var "G")) "," (Set (Var "F")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "G")) ")" ) "," (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "F")) ")" ) ($#k1_domain_1 :::"]"::: ) ))); definitionlet "G", "F" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) ; func :::"[:":::"G" "," "F":::":]"::: -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v8_algstr_0 :::"strict"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) equals :: PRVECT_3:def 4 (Set ($#g2_algstr_0 :::"addLoopStr"::: ) "(#" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "G") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "F") ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "(" ($#k1_prvect_3 :::"prod_ADD"::: ) "(" "G" "," "F" ")" ")" ) "," (Set "(" ($#k3_prvect_3 :::"prod_ZERO"::: ) "(" "G" "," "F" ")" ")" ) "#)" ); end; :: deftheorem defines :::"[:"::: PRVECT_3:def 4 : (Bool "for" (Set (Var "G")) "," (Set (Var "F")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) "holds" (Bool (Set ($#k4_prvect_3 :::"[:"::: ) (Set (Var "G")) "," (Set (Var "F")) ($#k4_prvect_3 :::":]"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#g2_algstr_0 :::"addLoopStr"::: ) "(#" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "F"))) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "(" ($#k1_prvect_3 :::"prod_ADD"::: ) "(" (Set (Var "G")) "," (Set (Var "F")) ")" ")" ) "," (Set "(" ($#k3_prvect_3 :::"prod_ZERO"::: ) "(" (Set (Var "G")) "," (Set (Var "F")) ")" ")" ) "#)" ))); registrationlet "G", "F" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) ; cluster (Set ($#k4_prvect_3 :::"[:"::: ) "G" "," "F" ($#k4_prvect_3 :::":]"::: ) ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v8_algstr_0 :::"strict"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ; end; registrationlet "G", "F" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) ; cluster (Set ($#k4_prvect_3 :::"[:"::: ) "G" "," "F" ($#k4_prvect_3 :::":]"::: ) ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v8_algstr_0 :::"strict"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ; end; registrationlet "G", "F" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) ; cluster (Set ($#k4_prvect_3 :::"[:"::: ) "G" "," "F" ($#k4_prvect_3 :::":]"::: ) ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v8_algstr_0 :::"strict"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ; end; registrationlet "G", "F" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) ; cluster (Set ($#k4_prvect_3 :::"[:"::: ) "G" "," "F" ($#k4_prvect_3 :::":]"::: ) ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v8_algstr_0 :::"strict"::: ) ($#v13_algstr_0 :::"right_complementable"::: ) ; end; theorem :: PRVECT_3:7 (Bool "for" (Set (Var "G")) "," (Set (Var "F")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) "holds" (Bool "(" (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) "is" ($#m1_subset_1 :::"Point":::) "of" (Set ($#k4_prvect_3 :::"[:"::: ) (Set (Var "G")) "," (Set (Var "F")) ($#k4_prvect_3 :::":]"::: ) )) "iff" (Bool "ex" (Set (Var "x1")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "G"))(Bool "ex" (Set (Var "x2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "F")) "st" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k1_domain_1 :::"]"::: ) )))) ")" ) ")" ) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set ($#k4_prvect_3 :::"[:"::: ) (Set (Var "G")) "," (Set (Var "F")) ($#k4_prvect_3 :::":]"::: ) ) (Bool "for" (Set (Var "x1")) "," (Set (Var "y1")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "x2")) "," (Set (Var "y2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "F")) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k1_domain_1 :::"]"::: ) )) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "y1")) "," (Set (Var "y2")) ($#k1_domain_1 :::"]"::: ) ))) "holds" (Bool (Set (Set (Var "x")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set "(" (Set (Var "x1")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "y1")) ")" ) "," (Set "(" (Set (Var "x2")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "y2")) ")" ) ($#k1_domain_1 :::"]"::: ) )))) ")" ) & (Bool (Set ($#k4_struct_0 :::"0."::: ) (Set ($#k4_prvect_3 :::"[:"::: ) (Set (Var "G")) "," (Set (Var "F")) ($#k4_prvect_3 :::":]"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "G")) ")" ) "," (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "F")) ")" ) ($#k1_domain_1 :::"]"::: ) )) ")" )) ; theorem :: PRVECT_3:8 (Bool "for" (Set (Var "G")) "," (Set (Var "F")) "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 "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set ($#k4_prvect_3 :::"[:"::: ) (Set (Var "G")) "," (Set (Var "F")) ($#k4_prvect_3 :::":]"::: ) ) (Bool "for" (Set (Var "x1")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "x2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "F")) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k1_domain_1 :::"]"::: ) ))) "holds" (Bool (Set ($#k4_algstr_0 :::"-"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "x1")) ")" ) "," (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "x2")) ")" ) ($#k1_domain_1 :::"]"::: ) )))))) ; registrationlet "G", "F" be ($#~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"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) ; cluster (Set ($#k4_prvect_3 :::"[:"::: ) "G" "," "F" ($#k4_prvect_3 :::":]"::: ) ) -> ($#~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"::: ) ; end; definitionlet "G", "F" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rlvect_1 :::"RLSStruct"::: ) ; func :::"[:":::"G" "," "F":::":]"::: -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_rlvect_1 :::"strict"::: ) ($#l1_rlvect_1 :::"RLSStruct"::: ) equals :: PRVECT_3:def 5 (Set ($#g1_rlvect_1 :::"RLSStruct"::: ) "(#" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "G") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "F") ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "(" ($#k3_prvect_3 :::"prod_ZERO"::: ) "(" "G" "," "F" ")" ")" ) "," (Set "(" ($#k1_prvect_3 :::"prod_ADD"::: ) "(" "G" "," "F" ")" ")" ) "," (Set "(" ($#k2_prvect_3 :::"prod_MLT"::: ) "(" "G" "," "F" ")" ")" ) "#)" ); end; :: deftheorem defines :::"[:"::: PRVECT_3:def 5 : (Bool "for" (Set (Var "G")) "," (Set (Var "F")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rlvect_1 :::"RLSStruct"::: ) "holds" (Bool (Set ($#k5_prvect_3 :::"[:"::: ) (Set (Var "G")) "," (Set (Var "F")) ($#k5_prvect_3 :::":]"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#g1_rlvect_1 :::"RLSStruct"::: ) "(#" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "F"))) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "(" ($#k3_prvect_3 :::"prod_ZERO"::: ) "(" (Set (Var "G")) "," (Set (Var "F")) ")" ")" ) "," (Set "(" ($#k1_prvect_3 :::"prod_ADD"::: ) "(" (Set (Var "G")) "," (Set (Var "F")) ")" ")" ) "," (Set "(" ($#k2_prvect_3 :::"prod_MLT"::: ) "(" (Set (Var "G")) "," (Set (Var "F")) ")" ")" ) "#)" ))); registrationlet "G", "F" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#l1_rlvect_1 :::"RLSStruct"::: ) ; cluster (Set ($#k5_prvect_3 :::"[:"::: ) "G" "," "F" ($#k5_prvect_3 :::":]"::: ) ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_rlvect_1 :::"strict"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ; end; registrationlet "G", "F" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#l1_rlvect_1 :::"RLSStruct"::: ) ; cluster (Set ($#k5_prvect_3 :::"[:"::: ) "G" "," "F" ($#k5_prvect_3 :::":]"::: ) ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_rlvect_1 :::"strict"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ; end; registrationlet "G", "F" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_rlvect_1 :::"RLSStruct"::: ) ; cluster (Set ($#k5_prvect_3 :::"[:"::: ) "G" "," "F" ($#k5_prvect_3 :::":]"::: ) ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_rlvect_1 :::"strict"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ; end; registrationlet "G", "F" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#l1_rlvect_1 :::"RLSStruct"::: ) ; cluster (Set ($#k5_prvect_3 :::"[:"::: ) "G" "," "F" ($#k5_prvect_3 :::":]"::: ) ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v1_rlvect_1 :::"strict"::: ) ; end; theorem :: PRVECT_3:9 (Bool "for" (Set (Var "G")) "," (Set (Var "F")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_rlvect_1 :::"RLSStruct"::: ) "holds" (Bool "(" (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) "is" ($#m1_subset_1 :::"Point":::) "of" (Set ($#k5_prvect_3 :::"[:"::: ) (Set (Var "G")) "," (Set (Var "F")) ($#k5_prvect_3 :::":]"::: ) )) "iff" (Bool "ex" (Set (Var "x1")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "G"))(Bool "ex" (Set (Var "x2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "F")) "st" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k1_domain_1 :::"]"::: ) )))) ")" ) ")" ) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set ($#k5_prvect_3 :::"[:"::: ) (Set (Var "G")) "," (Set (Var "F")) ($#k5_prvect_3 :::":]"::: ) ) (Bool "for" (Set (Var "x1")) "," (Set (Var "y1")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "x2")) "," (Set (Var "y2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "F")) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k1_domain_1 :::"]"::: ) )) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "y1")) "," (Set (Var "y2")) ($#k1_domain_1 :::"]"::: ) ))) "holds" (Bool (Set (Set (Var "x")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set "(" (Set (Var "x1")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "y1")) ")" ) "," (Set "(" (Set (Var "x2")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "y2")) ")" ) ($#k1_domain_1 :::"]"::: ) )))) ")" ) & (Bool (Set ($#k4_struct_0 :::"0."::: ) (Set ($#k5_prvect_3 :::"[:"::: ) (Set (Var "G")) "," (Set (Var "F")) ($#k5_prvect_3 :::":]"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "G")) ")" ) "," (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "F")) ")" ) ($#k1_domain_1 :::"]"::: ) )) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set ($#k5_prvect_3 :::"[:"::: ) (Set (Var "G")) "," (Set (Var "F")) ($#k5_prvect_3 :::":]"::: ) ) (Bool "for" (Set (Var "x1")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "x2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "a")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k1_domain_1 :::"]"::: ) ))) "holds" (Bool (Set (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set "(" (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "x1")) ")" ) "," (Set "(" (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "x2")) ")" ) ($#k1_domain_1 :::"]"::: ) ))))) ")" ) ")" )) ; theorem :: PRVECT_3:10 (Bool "for" (Set (Var "G")) "," (Set (Var "F")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l1_rlvect_1 :::"RLSStruct"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set ($#k5_prvect_3 :::"[:"::: ) (Set (Var "G")) "," (Set (Var "F")) ($#k5_prvect_3 :::":]"::: ) ) (Bool "for" (Set (Var "x1")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "x2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "F")) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k1_domain_1 :::"]"::: ) ))) "holds" (Bool (Set ($#k4_algstr_0 :::"-"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "x1")) ")" ) "," (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "x2")) ")" ) ($#k1_domain_1 :::"]"::: ) )))))) ; registrationlet "G", "F" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v5_rlvect_1 :::"vector-distributive"::: ) ($#l1_rlvect_1 :::"RLSStruct"::: ) ; cluster (Set ($#k5_prvect_3 :::"[:"::: ) "G" "," "F" ($#k5_prvect_3 :::":]"::: ) ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_rlvect_1 :::"strict"::: ) ($#v5_rlvect_1 :::"vector-distributive"::: ) ; end; registrationlet "G", "F" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v6_rlvect_1 :::"scalar-distributive"::: ) ($#l1_rlvect_1 :::"RLSStruct"::: ) ; cluster (Set ($#k5_prvect_3 :::"[:"::: ) "G" "," "F" ($#k5_prvect_3 :::":]"::: ) ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_rlvect_1 :::"strict"::: ) ($#v6_rlvect_1 :::"scalar-distributive"::: ) ; end; registrationlet "G", "F" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v7_rlvect_1 :::"scalar-associative"::: ) ($#l1_rlvect_1 :::"RLSStruct"::: ) ; cluster (Set ($#k5_prvect_3 :::"[:"::: ) "G" "," "F" ($#k5_prvect_3 :::":]"::: ) ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_rlvect_1 :::"strict"::: ) ($#v7_rlvect_1 :::"scalar-associative"::: ) ; end; registrationlet "G", "F" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v8_rlvect_1 :::"scalar-unital"::: ) ($#l1_rlvect_1 :::"RLSStruct"::: ) ; cluster (Set ($#k5_prvect_3 :::"[:"::: ) "G" "," "F" ($#k5_prvect_3 :::":]"::: ) ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_rlvect_1 :::"strict"::: ) ($#v8_rlvect_1 :::"scalar-unital"::: ) ; end; registrationlet "G" 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"::: ) ($#v5_rlvect_1 :::"vector-distributive"::: ) ($#v6_rlvect_1 :::"scalar-distributive"::: ) ($#v7_rlvect_1 :::"scalar-associative"::: ) ($#v8_rlvect_1 :::"scalar-unital"::: ) ($#l1_rlvect_1 :::"RLSStruct"::: ) ; cluster (Set ($#k5_finseq_1 :::"<*"::: ) "G" ($#k5_finseq_1 :::"*>"::: ) ) -> ($#v1_prvect_2 :::"RealLinearSpace-yielding"::: ) ; end; registrationlet "G", "F" 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"::: ) ($#v5_rlvect_1 :::"vector-distributive"::: ) ($#v6_rlvect_1 :::"scalar-distributive"::: ) ($#v7_rlvect_1 :::"scalar-associative"::: ) ($#v8_rlvect_1 :::"scalar-unital"::: ) ($#l1_rlvect_1 :::"RLSStruct"::: ) ; cluster (Set ($#k10_finseq_1 :::"<*"::: ) "G" "," "F" ($#k10_finseq_1 :::"*>"::: ) ) -> ($#v1_prvect_2 :::"RealLinearSpace-yielding"::: ) ; end; begin theorem :: PRVECT_3:11 (Bool "for" (Set (Var "X")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "ex" (Set (Var "I")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set "(" ($#k10_prvect_2 :::"product"::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "X")) ($#k9_finseq_1 :::"*>"::: ) ) ")" ) "st" (Bool "(" (Bool (Set (Var "I")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool (Set (Var "I")) "is" ($#v2_funct_2 :::"onto"::: ) ) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "I")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "x")) ($#k12_finseq_1 :::"*>"::: ) )) ")" ) & (Bool "(" "for" (Set (Var "v")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "I")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "v")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "w")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "I")) ($#k3_funct_2 :::"."::: ) (Set (Var "v")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "I")) ($#k3_funct_2 :::"."::: ) (Set (Var "w")) ")" ))) ")" ) & (Bool "(" "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set (Set (Var "I")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "r")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "v")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set (Var "I")) ($#k3_funct_2 :::"."::: ) (Set (Var "v")) ")" )))) ")" ) & (Bool (Set (Set (Var "I")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "X")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k10_prvect_2 :::"product"::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "X")) ($#k9_finseq_1 :::"*>"::: ) ) ")" ))) ")" ))) ; registrationlet "G", "F" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_prvect_2 :::"RealLinearSpace-yielding"::: ) ($#m1_hidden :::"FinSequence":::); cluster (Set "G" ($#k7_finseq_1 :::"^"::: ) "F") -> ($#v1_prvect_2 :::"RealLinearSpace-yielding"::: ) ; end; theorem :: PRVECT_3:12 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "ex" (Set (Var "I")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_prvect_3 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k5_prvect_3 :::":]"::: ) ) "," (Set "(" ($#k10_prvect_2 :::"product"::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k10_finseq_1 :::"*>"::: ) ) ")" ) "st" (Bool "(" (Bool (Set (Var "I")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool (Set (Var "I")) "is" ($#v2_funct_2 :::"onto"::: ) ) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "Y")) "holds" (Bool (Set (Set (Var "I")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) ))) ")" ) & (Bool "(" "for" (Set (Var "v")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set ($#k5_prvect_3 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k5_prvect_3 :::":]"::: ) ) "holds" (Bool (Set (Set (Var "I")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "v")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "w")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "I")) ($#k3_funct_2 :::"."::: ) (Set (Var "v")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "I")) ($#k3_funct_2 :::"."::: ) (Set (Var "w")) ")" ))) ")" ) & (Bool "(" "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set ($#k5_prvect_3 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k5_prvect_3 :::":]"::: ) ) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set (Set (Var "I")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "r")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "v")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set (Var "I")) ($#k3_funct_2 :::"."::: ) (Set (Var "v")) ")" )))) ")" ) & (Bool (Set (Set (Var "I")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set ($#k5_prvect_3 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k5_prvect_3 :::":]"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k10_prvect_2 :::"product"::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k10_finseq_1 :::"*>"::: ) ) ")" ))) ")" ))) ; theorem :: PRVECT_3:13 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"RealLinearSpace-Sequence":::) (Bool "ex" (Set (Var "I")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_prvect_3 :::"[:"::: ) (Set "(" ($#k10_prvect_2 :::"product"::: ) (Set (Var "X")) ")" ) "," (Set "(" ($#k10_prvect_2 :::"product"::: ) (Set (Var "Y")) ")" ) ($#k5_prvect_3 :::":]"::: ) ) "," (Set "(" ($#k10_prvect_2 :::"product"::: ) (Set "(" (Set (Var "X")) ($#k7_finseq_1 :::"^"::: ) (Set (Var "Y")) ")" ) ")" ) "st" (Bool "(" (Bool (Set (Var "I")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool (Set (Var "I")) "is" ($#v2_funct_2 :::"onto"::: ) ) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k10_prvect_2 :::"product"::: ) (Set (Var "X")) ")" ) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k10_prvect_2 :::"product"::: ) (Set (Var "Y")) ")" ) (Bool "ex" (Set (Var "x1")) "," (Set (Var "y1")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "x1"))) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Var "y1"))) & (Bool (Set (Set (Var "I")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "x1")) ($#k7_finseq_1 :::"^"::: ) (Set (Var "y1")))) ")" ))) ")" ) & (Bool "(" "for" (Set (Var "v")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set ($#k5_prvect_3 :::"[:"::: ) (Set "(" ($#k10_prvect_2 :::"product"::: ) (Set (Var "X")) ")" ) "," (Set "(" ($#k10_prvect_2 :::"product"::: ) (Set (Var "Y")) ")" ) ($#k5_prvect_3 :::":]"::: ) ) "holds" (Bool (Set (Set (Var "I")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "v")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "w")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "I")) ($#k3_funct_2 :::"."::: ) (Set (Var "v")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "I")) ($#k3_funct_2 :::"."::: ) (Set (Var "w")) ")" ))) ")" ) & (Bool "(" "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set ($#k5_prvect_3 :::"[:"::: ) (Set "(" ($#k10_prvect_2 :::"product"::: ) (Set (Var "X")) ")" ) "," (Set "(" ($#k10_prvect_2 :::"product"::: ) (Set (Var "Y")) ")" ) ($#k5_prvect_3 :::":]"::: ) ) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set (Set (Var "I")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "r")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "v")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set (Var "I")) ($#k3_funct_2 :::"."::: ) (Set (Var "v")) ")" )))) ")" ) & (Bool (Set (Set (Var "I")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set ($#k5_prvect_3 :::"[:"::: ) (Set "(" ($#k10_prvect_2 :::"product"::: ) (Set (Var "X")) ")" ) "," (Set "(" ($#k10_prvect_2 :::"product"::: ) (Set (Var "Y")) ")" ) ($#k5_prvect_3 :::":]"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k10_prvect_2 :::"product"::: ) (Set "(" (Set (Var "X")) ($#k7_finseq_1 :::"^"::: ) (Set (Var "Y")) ")" ) ")" ))) ")" ))) ; theorem :: PRVECT_3:14 (Bool "for" (Set (Var "G")) "," (Set (Var "F")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) "holds" (Bool "(" (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) "is" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k10_prvect_2 :::"product"::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "G")) "," (Set (Var "F")) ($#k10_finseq_1 :::"*>"::: ) ) ")" )) "iff" (Bool "ex" (Set (Var "x1")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "G"))(Bool "ex" (Set (Var "x2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "F")) "st" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k10_finseq_1 :::"*>"::: ) )))) ")" ) ")" ) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k10_prvect_2 :::"product"::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "G")) "," (Set (Var "F")) ($#k10_finseq_1 :::"*>"::: ) ) ")" ) (Bool "for" (Set (Var "x1")) "," (Set (Var "y1")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "x2")) "," (Set (Var "y2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "F")) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k10_finseq_1 :::"*>"::: ) )) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "y1")) "," (Set (Var "y2")) ($#k10_finseq_1 :::"*>"::: ) ))) "holds" (Bool (Set (Set (Var "x")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set "(" (Set (Var "x1")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "y1")) ")" ) "," (Set "(" (Set (Var "x2")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "y2")) ")" ) ($#k10_finseq_1 :::"*>"::: ) )))) ")" ) & (Bool (Set ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k10_prvect_2 :::"product"::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "G")) "," (Set (Var "F")) ($#k10_finseq_1 :::"*>"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "G")) ")" ) "," (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "F")) ")" ) ($#k10_finseq_1 :::"*>"::: ) )) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k10_prvect_2 :::"product"::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "G")) "," (Set (Var "F")) ($#k10_finseq_1 :::"*>"::: ) ) ")" ) (Bool "for" (Set (Var "x1")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "x2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "F")) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k10_finseq_1 :::"*>"::: ) ))) "holds" (Bool (Set ($#k4_algstr_0 :::"-"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "x1")) ")" ) "," (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "x2")) ")" ) ($#k10_finseq_1 :::"*>"::: ) )))) ")" ) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k10_prvect_2 :::"product"::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "G")) "," (Set (Var "F")) ($#k10_finseq_1 :::"*>"::: ) ) ")" ) (Bool "for" (Set (Var "x1")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "x2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "a")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k10_finseq_1 :::"*>"::: ) ))) "holds" (Bool (Set (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set "(" (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "x1")) ")" ) "," (Set "(" (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "x2")) ")" ) ($#k10_finseq_1 :::"*>"::: ) ))))) ")" ) ")" )) ; begin definitionlet "G", "F" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_normsp_1 :::"NORMSTR"::: ) ; func :::"prod_NORM"::: "(" "G" "," "F" ")" -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "G") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "F") ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) means :: PRVECT_3:def 6 (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Point":::) "of" "G" (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Point":::) "of" "F" (Bool "ex" (Set (Var "v")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 2)) "st" (Bool "(" (Bool (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set ($#k2_finseq_4 :::"<*"::: ) (Set ($#k1_normsp_0 :::"||."::: ) (Set (Var "g")) ($#k1_normsp_0 :::".||"::: ) ) "," (Set ($#k1_normsp_0 :::"||."::: ) (Set (Var "f")) ($#k1_normsp_0 :::".||"::: ) ) ($#k2_finseq_4 :::"*>"::: ) )) & (Bool (Set it ($#k2_binop_1 :::"."::: ) "(" (Set (Var "g")) "," (Set (Var "f")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k12_euclid :::"|."::: ) (Set (Var "v")) ($#k12_euclid :::".|"::: ) )) ")" )))); end; :: deftheorem defines :::"prod_NORM"::: PRVECT_3:def 6 : (Bool "for" (Set (Var "G")) "," (Set (Var "F")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_normsp_1 :::"NORMSTR"::: ) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "F"))) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k6_prvect_3 :::"prod_NORM"::: ) "(" (Set (Var "G")) "," (Set (Var "F")) ")" )) "iff" (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "F")) (Bool "ex" (Set (Var "v")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 2)) "st" (Bool "(" (Bool (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set ($#k2_finseq_4 :::"<*"::: ) (Set ($#k1_normsp_0 :::"||."::: ) (Set (Var "g")) ($#k1_normsp_0 :::".||"::: ) ) "," (Set ($#k1_normsp_0 :::"||."::: ) (Set (Var "f")) ($#k1_normsp_0 :::".||"::: ) ) ($#k2_finseq_4 :::"*>"::: ) )) & (Bool (Set (Set (Var "b3")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "g")) "," (Set (Var "f")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k12_euclid :::"|."::: ) (Set (Var "v")) ($#k12_euclid :::".|"::: ) )) ")" )))) ")" ))); definitionlet "G", "F" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_normsp_1 :::"NORMSTR"::: ) ; func :::"[:":::"G" "," "F":::":]"::: -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_normsp_1 :::"strict"::: ) ($#l1_normsp_1 :::"NORMSTR"::: ) equals :: PRVECT_3:def 7 (Set ($#g1_normsp_1 :::"NORMSTR"::: ) "(#" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "G") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "F") ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "(" ($#k3_prvect_3 :::"prod_ZERO"::: ) "(" "G" "," "F" ")" ")" ) "," (Set "(" ($#k1_prvect_3 :::"prod_ADD"::: ) "(" "G" "," "F" ")" ")" ) "," (Set "(" ($#k2_prvect_3 :::"prod_MLT"::: ) "(" "G" "," "F" ")" ")" ) "," (Set "(" ($#k6_prvect_3 :::"prod_NORM"::: ) "(" "G" "," "F" ")" ")" ) "#)" ); end; :: deftheorem defines :::"[:"::: PRVECT_3:def 7 : (Bool "for" (Set (Var "G")) "," (Set (Var "F")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_normsp_1 :::"NORMSTR"::: ) "holds" (Bool (Set ($#k7_prvect_3 :::"[:"::: ) (Set (Var "G")) "," (Set (Var "F")) ($#k7_prvect_3 :::":]"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#g1_normsp_1 :::"NORMSTR"::: ) "(#" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "F"))) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "(" ($#k3_prvect_3 :::"prod_ZERO"::: ) "(" (Set (Var "G")) "," (Set (Var "F")) ")" ")" ) "," (Set "(" ($#k1_prvect_3 :::"prod_ADD"::: ) "(" (Set (Var "G")) "," (Set (Var "F")) ")" ")" ) "," (Set "(" ($#k2_prvect_3 :::"prod_MLT"::: ) "(" (Set (Var "G")) "," (Set (Var "F")) ")" ")" ) "," (Set "(" ($#k6_prvect_3 :::"prod_NORM"::: ) "(" (Set (Var "G")) "," (Set (Var "F")) ")" ")" ) "#)" ))); registrationlet "G", "F" be ($#l1_normsp_1 :::"RealNormSpace":::); cluster (Set ($#k7_prvect_3 :::"[:"::: ) "G" "," "F" ($#k7_prvect_3 :::":]"::: ) ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_normsp_0 :::"discerning"::: ) ($#v4_normsp_0 :::"reflexive"::: ) ($#v1_normsp_1 :::"strict"::: ) ($#v2_normsp_1 :::"RealNormSpace-like"::: ) ; end; registrationlet "G", "F" 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"::: ) ($#v5_rlvect_1 :::"vector-distributive"::: ) ($#v6_rlvect_1 :::"scalar-distributive"::: ) ($#v7_rlvect_1 :::"scalar-associative"::: ) ($#v8_rlvect_1 :::"scalar-unital"::: ) ($#v3_normsp_0 :::"discerning"::: ) ($#v4_normsp_0 :::"reflexive"::: ) ($#v2_normsp_1 :::"RealNormSpace-like"::: ) ($#l1_normsp_1 :::"NORMSTR"::: ) ; cluster (Set ($#k7_prvect_3 :::"[:"::: ) "G" "," "F" ($#k7_prvect_3 :::":]"::: ) ) -> ($#~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"::: ) ($#v3_normsp_0 :::"discerning"::: ) ($#v4_normsp_0 :::"reflexive"::: ) ($#v1_normsp_1 :::"strict"::: ) ($#v2_normsp_1 :::"RealNormSpace-like"::: ) ; end; registrationlet "G" 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"::: ) ($#v5_rlvect_1 :::"vector-distributive"::: ) ($#v6_rlvect_1 :::"scalar-distributive"::: ) ($#v7_rlvect_1 :::"scalar-associative"::: ) ($#v8_rlvect_1 :::"scalar-unital"::: ) ($#v3_normsp_0 :::"discerning"::: ) ($#v4_normsp_0 :::"reflexive"::: ) ($#v2_normsp_1 :::"RealNormSpace-like"::: ) ($#l1_normsp_1 :::"NORMSTR"::: ) ; cluster (Set ($#k5_finseq_1 :::"<*"::: ) "G" ($#k5_finseq_1 :::"*>"::: ) ) -> ($#v2_prvect_2 :::"RealNormSpace-yielding"::: ) ; end; registrationlet "G", "F" 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"::: ) ($#v5_rlvect_1 :::"vector-distributive"::: ) ($#v6_rlvect_1 :::"scalar-distributive"::: ) ($#v7_rlvect_1 :::"scalar-associative"::: ) ($#v8_rlvect_1 :::"scalar-unital"::: ) ($#v3_normsp_0 :::"discerning"::: ) ($#v4_normsp_0 :::"reflexive"::: ) ($#v2_normsp_1 :::"RealNormSpace-like"::: ) ($#l1_normsp_1 :::"NORMSTR"::: ) ; cluster (Set ($#k10_finseq_1 :::"<*"::: ) "G" "," "F" ($#k10_finseq_1 :::"*>"::: ) ) -> ($#v2_prvect_2 :::"RealNormSpace-yielding"::: ) ; end; theorem :: PRVECT_3:15 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "ex" (Set (Var "I")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k7_prvect_3 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k7_prvect_3 :::":]"::: ) ) "," (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k10_finseq_1 :::"*>"::: ) ) ")" ) "st" (Bool "(" (Bool (Set (Var "I")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool (Set (Var "I")) "is" ($#v2_funct_2 :::"onto"::: ) ) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "Y")) "holds" (Bool (Set (Set (Var "I")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) ))) ")" ) & (Bool "(" "for" (Set (Var "v")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set ($#k7_prvect_3 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k7_prvect_3 :::":]"::: ) ) "holds" (Bool (Set (Set (Var "I")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "v")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "w")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "I")) ($#k3_funct_2 :::"."::: ) (Set (Var "v")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "I")) ($#k3_funct_2 :::"."::: ) (Set (Var "w")) ")" ))) ")" ) & (Bool "(" "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set ($#k7_prvect_3 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k7_prvect_3 :::":]"::: ) ) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set (Set (Var "I")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "r")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "v")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set (Var "I")) ($#k3_funct_2 :::"."::: ) (Set (Var "v")) ")" )))) ")" ) & (Bool (Set ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k10_finseq_1 :::"*>"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "I")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set ($#k7_prvect_3 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k7_prvect_3 :::":]"::: ) ) ")" ))) & (Bool "(" "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set ($#k7_prvect_3 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k7_prvect_3 :::":]"::: ) ) "holds" (Bool (Set ($#k1_normsp_0 :::"||."::: ) (Set "(" (Set (Var "I")) ($#k3_funct_2 :::"."::: ) (Set (Var "v")) ")" ) ($#k1_normsp_0 :::".||"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k1_normsp_0 :::"||."::: ) (Set (Var "v")) ($#k1_normsp_0 :::".||"::: ) )) ")" ) ")" ))) ; theorem :: PRVECT_3:16 (Bool "for" (Set (Var "X")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "ex" (Set (Var "I")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "X")) ($#k9_finseq_1 :::"*>"::: ) ) ")" ) "st" (Bool "(" (Bool (Set (Var "I")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool (Set (Var "I")) "is" ($#v2_funct_2 :::"onto"::: ) ) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "I")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "x")) ($#k12_finseq_1 :::"*>"::: ) )) ")" ) & (Bool "(" "for" (Set (Var "v")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "I")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "v")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "w")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "I")) ($#k3_funct_2 :::"."::: ) (Set (Var "v")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "I")) ($#k3_funct_2 :::"."::: ) (Set (Var "w")) ")" ))) ")" ) & (Bool "(" "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set (Set (Var "I")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "r")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "v")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set (Var "I")) ($#k3_funct_2 :::"."::: ) (Set (Var "v")) ")" )))) ")" ) & (Bool (Set ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "X")) ($#k9_finseq_1 :::"*>"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "I")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "X")) ")" ))) & (Bool "(" "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k1_normsp_0 :::"||."::: ) (Set "(" (Set (Var "I")) ($#k3_funct_2 :::"."::: ) (Set (Var "v")) ")" ) ($#k1_normsp_0 :::".||"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k1_normsp_0 :::"||."::: ) (Set (Var "v")) ($#k1_normsp_0 :::".||"::: ) )) ")" ) ")" ))) ; registrationlet "G", "F" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_prvect_2 :::"RealNormSpace-yielding"::: ) ($#m1_hidden :::"FinSequence":::); cluster (Set "G" ($#k7_finseq_1 :::"^"::: ) "F") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_prvect_2 :::"RealNormSpace-yielding"::: ) ; end; theorem :: PRVECT_3:17 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"RealNormSpace-Sequence":::) (Bool "ex" (Set (Var "I")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k7_prvect_3 :::"[:"::: ) (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set (Var "X")) ")" ) "," (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set (Var "Y")) ")" ) ($#k7_prvect_3 :::":]"::: ) ) "," (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set "(" (Set (Var "X")) ($#k7_finseq_1 :::"^"::: ) (Set (Var "Y")) ")" ) ")" ) "st" (Bool "(" (Bool (Set (Var "I")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool (Set (Var "I")) "is" ($#v2_funct_2 :::"onto"::: ) ) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set (Var "X")) ")" ) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set (Var "Y")) ")" ) (Bool "ex" (Set (Var "x1")) "," (Set (Var "y1")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "x1"))) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Var "y1"))) & (Bool (Set (Set (Var "I")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "x1")) ($#k7_finseq_1 :::"^"::: ) (Set (Var "y1")))) ")" ))) ")" ) & (Bool "(" "for" (Set (Var "v")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set ($#k7_prvect_3 :::"[:"::: ) (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set (Var "X")) ")" ) "," (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set (Var "Y")) ")" ) ($#k7_prvect_3 :::":]"::: ) ) "holds" (Bool (Set (Set (Var "I")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "v")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "w")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "I")) ($#k3_funct_2 :::"."::: ) (Set (Var "v")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "I")) ($#k3_funct_2 :::"."::: ) (Set (Var "w")) ")" ))) ")" ) & (Bool "(" "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set ($#k7_prvect_3 :::"[:"::: ) (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set (Var "X")) ")" ) "," (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set (Var "Y")) ")" ) ($#k7_prvect_3 :::":]"::: ) ) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set (Set (Var "I")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "r")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "v")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set (Var "I")) ($#k3_funct_2 :::"."::: ) (Set (Var "v")) ")" )))) ")" ) & (Bool (Set (Set (Var "I")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set ($#k7_prvect_3 :::"[:"::: ) (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set (Var "X")) ")" ) "," (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set (Var "Y")) ")" ) ($#k7_prvect_3 :::":]"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set "(" (Set (Var "X")) ($#k7_finseq_1 :::"^"::: ) (Set (Var "Y")) ")" ) ")" ))) & (Bool "(" "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set ($#k7_prvect_3 :::"[:"::: ) (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set (Var "X")) ")" ) "," (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set (Var "Y")) ")" ) ($#k7_prvect_3 :::":]"::: ) ) "holds" (Bool (Set ($#k1_normsp_0 :::"||."::: ) (Set "(" (Set (Var "I")) ($#k3_funct_2 :::"."::: ) (Set (Var "v")) ")" ) ($#k1_normsp_0 :::".||"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k1_normsp_0 :::"||."::: ) (Set (Var "v")) ($#k1_normsp_0 :::".||"::: ) )) ")" ) ")" ))) ; theorem :: PRVECT_3:18 (Bool "for" (Set (Var "G")) "," (Set (Var "F")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) "holds" (Bool "(" (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) "is" ($#m1_subset_1 :::"Point":::) "of" (Set ($#k7_prvect_3 :::"[:"::: ) (Set (Var "G")) "," (Set (Var "F")) ($#k7_prvect_3 :::":]"::: ) )) "iff" (Bool "ex" (Set (Var "x1")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "G"))(Bool "ex" (Set (Var "x2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "F")) "st" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k1_domain_1 :::"]"::: ) )))) ")" ) ")" ) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set ($#k7_prvect_3 :::"[:"::: ) (Set (Var "G")) "," (Set (Var "F")) ($#k7_prvect_3 :::":]"::: ) ) (Bool "for" (Set (Var "x1")) "," (Set (Var "y1")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "x2")) "," (Set (Var "y2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "F")) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k1_domain_1 :::"]"::: ) )) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "y1")) "," (Set (Var "y2")) ($#k1_domain_1 :::"]"::: ) ))) "holds" (Bool (Set (Set (Var "x")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set "(" (Set (Var "x1")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "y1")) ")" ) "," (Set "(" (Set (Var "x2")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "y2")) ")" ) ($#k1_domain_1 :::"]"::: ) )))) ")" ) & (Bool (Set ($#k4_struct_0 :::"0."::: ) (Set ($#k7_prvect_3 :::"[:"::: ) (Set (Var "G")) "," (Set (Var "F")) ($#k7_prvect_3 :::":]"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "G")) ")" ) "," (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "F")) ")" ) ($#k1_domain_1 :::"]"::: ) )) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set ($#k7_prvect_3 :::"[:"::: ) (Set (Var "G")) "," (Set (Var "F")) ($#k7_prvect_3 :::":]"::: ) ) (Bool "for" (Set (Var "x1")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "x2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "F")) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k1_domain_1 :::"]"::: ) ))) "holds" (Bool (Set ($#k4_algstr_0 :::"-"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "x1")) ")" ) "," (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "x2")) ")" ) ($#k1_domain_1 :::"]"::: ) )))) ")" ) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set ($#k7_prvect_3 :::"[:"::: ) (Set (Var "G")) "," (Set (Var "F")) ($#k7_prvect_3 :::":]"::: ) ) (Bool "for" (Set (Var "x1")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "x2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "a")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k1_domain_1 :::"]"::: ) ))) "holds" (Bool (Set (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set "(" (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "x1")) ")" ) "," (Set "(" (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "x2")) ")" ) ($#k1_domain_1 :::"]"::: ) ))))) ")" ) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set ($#k7_prvect_3 :::"[:"::: ) (Set (Var "G")) "," (Set (Var "F")) ($#k7_prvect_3 :::":]"::: ) ) (Bool "for" (Set (Var "x1")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "x2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "F")) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k1_domain_1 :::"]"::: ) ))) "holds" (Bool "ex" (Set (Var "w")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 2)) "st" (Bool "(" (Bool (Set (Var "w")) ($#r1_hidden :::"="::: ) (Set ($#k2_finseq_4 :::"<*"::: ) (Set ($#k1_normsp_0 :::"||."::: ) (Set (Var "x1")) ($#k1_normsp_0 :::".||"::: ) ) "," (Set ($#k1_normsp_0 :::"||."::: ) (Set (Var "x2")) ($#k1_normsp_0 :::".||"::: ) ) ($#k2_finseq_4 :::"*>"::: ) )) & (Bool (Set ($#k1_normsp_0 :::"||."::: ) (Set (Var "x")) ($#k1_normsp_0 :::".||"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k12_euclid :::"|."::: ) (Set (Var "w")) ($#k12_euclid :::".|"::: ) )) ")" )))) ")" ) ")" )) ; theorem :: PRVECT_3:19 (Bool "for" (Set (Var "G")) "," (Set (Var "F")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) "holds" (Bool "(" (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) "is" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "G")) "," (Set (Var "F")) ($#k10_finseq_1 :::"*>"::: ) ) ")" )) "iff" (Bool "ex" (Set (Var "x1")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "G"))(Bool "ex" (Set (Var "x2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "F")) "st" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k10_finseq_1 :::"*>"::: ) )))) ")" ) ")" ) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "G")) "," (Set (Var "F")) ($#k10_finseq_1 :::"*>"::: ) ) ")" ) (Bool "for" (Set (Var "x1")) "," (Set (Var "y1")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "x2")) "," (Set (Var "y2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "F")) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k10_finseq_1 :::"*>"::: ) )) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "y1")) "," (Set (Var "y2")) ($#k10_finseq_1 :::"*>"::: ) ))) "holds" (Bool (Set (Set (Var "x")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set "(" (Set (Var "x1")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "y1")) ")" ) "," (Set "(" (Set (Var "x2")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "y2")) ")" ) ($#k10_finseq_1 :::"*>"::: ) )))) ")" ) & (Bool (Set ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "G")) "," (Set (Var "F")) ($#k10_finseq_1 :::"*>"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "G")) ")" ) "," (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "F")) ")" ) ($#k10_finseq_1 :::"*>"::: ) )) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "G")) "," (Set (Var "F")) ($#k10_finseq_1 :::"*>"::: ) ) ")" ) (Bool "for" (Set (Var "x1")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "x2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "F")) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k10_finseq_1 :::"*>"::: ) ))) "holds" (Bool (Set ($#k4_algstr_0 :::"-"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "x1")) ")" ) "," (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "x2")) ")" ) ($#k10_finseq_1 :::"*>"::: ) )))) ")" ) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "G")) "," (Set (Var "F")) ($#k10_finseq_1 :::"*>"::: ) ) ")" ) (Bool "for" (Set (Var "x1")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "x2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "F")) (Bool "for" (Set (Var "a")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k10_finseq_1 :::"*>"::: ) ))) "holds" (Bool (Set (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set "(" (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "x1")) ")" ) "," (Set "(" (Set (Var "a")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "x2")) ")" ) ($#k10_finseq_1 :::"*>"::: ) ))))) ")" ) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "G")) "," (Set (Var "F")) ($#k10_finseq_1 :::"*>"::: ) ) ")" ) (Bool "for" (Set (Var "x1")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "G")) (Bool "for" (Set (Var "x2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "F")) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k10_finseq_1 :::"*>"::: ) ))) "holds" (Bool "ex" (Set (Var "w")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set ($#k1_euclid :::"REAL"::: ) (Num 2)) "st" (Bool "(" (Bool (Set (Var "w")) ($#r1_hidden :::"="::: ) (Set ($#k2_finseq_4 :::"<*"::: ) (Set ($#k1_normsp_0 :::"||."::: ) (Set (Var "x1")) ($#k1_normsp_0 :::".||"::: ) ) "," (Set ($#k1_normsp_0 :::"||."::: ) (Set (Var "x2")) ($#k1_normsp_0 :::".||"::: ) ) ($#k2_finseq_4 :::"*>"::: ) )) & (Bool (Set ($#k1_normsp_0 :::"||."::: ) (Set (Var "x")) ($#k1_normsp_0 :::".||"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k12_euclid :::"|."::: ) (Set (Var "w")) ($#k12_euclid :::".|"::: ) )) ")" )))) ")" ) ")" )) ; registrationlet "X", "Y" be ($#v3_lopban_1 :::"complete"::: ) ($#l1_normsp_1 :::"RealNormSpace":::); cluster (Set ($#k7_prvect_3 :::"[:"::: ) "X" "," "Y" ($#k7_prvect_3 :::":]"::: ) ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_normsp_1 :::"strict"::: ) ($#v3_lopban_1 :::"complete"::: ) ; end; theorem :: PRVECT_3:20 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"RealNormSpace-Sequence":::) (Bool "ex" (Set (Var "I")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set (Var "X")) ")" ) "," (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set (Var "Y")) ")" ) ($#k10_finseq_1 :::"*>"::: ) ) ")" ) "," (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set "(" (Set (Var "X")) ($#k7_finseq_1 :::"^"::: ) (Set (Var "Y")) ")" ) ")" ) "st" (Bool "(" (Bool (Set (Var "I")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool (Set (Var "I")) "is" ($#v2_funct_2 :::"onto"::: ) ) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set (Var "X")) ")" ) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set (Var "Y")) ")" ) (Bool "ex" (Set (Var "x1")) "," (Set (Var "y1")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "x1"))) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Var "y1"))) & (Bool (Set (Set (Var "I")) ($#k1_funct_1 :::"."::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set (Var "x1")) ($#k7_finseq_1 :::"^"::: ) (Set (Var "y1")))) ")" ))) ")" ) & (Bool "(" "for" (Set (Var "v")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set (Var "X")) ")" ) "," (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set (Var "Y")) ")" ) ($#k10_finseq_1 :::"*>"::: ) ) ")" ) "holds" (Bool (Set (Set (Var "I")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "v")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "w")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "I")) ($#k3_funct_2 :::"."::: ) (Set (Var "v")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "I")) ($#k3_funct_2 :::"."::: ) (Set (Var "w")) ")" ))) ")" ) & (Bool "(" "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set (Var "X")) ")" ) "," (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set (Var "Y")) ")" ) ($#k10_finseq_1 :::"*>"::: ) ) ")" ) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set (Set (Var "I")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "r")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "v")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set (Var "I")) ($#k3_funct_2 :::"."::: ) (Set (Var "v")) ")" )))) ")" ) & (Bool (Set (Set (Var "I")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set (Var "X")) ")" ) "," (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set (Var "Y")) ")" ) ($#k10_finseq_1 :::"*>"::: ) ) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set "(" (Set (Var "X")) ($#k7_finseq_1 :::"^"::: ) (Set (Var "Y")) ")" ) ")" ))) & (Bool "(" "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set (Var "X")) ")" ) "," (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set (Var "Y")) ")" ) ($#k10_finseq_1 :::"*>"::: ) ) ")" ) "holds" (Bool (Set ($#k1_normsp_0 :::"||."::: ) (Set "(" (Set (Var "I")) ($#k3_funct_2 :::"."::: ) (Set (Var "v")) ")" ) ($#k1_normsp_0 :::".||"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k1_normsp_0 :::"||."::: ) (Set (Var "v")) ($#k1_normsp_0 :::".||"::: ) )) ")" ) ")" ))) ; theorem :: PRVECT_3:21 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "ex" (Set (Var "I")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_prvect_3 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k5_prvect_3 :::":]"::: ) ) "," (Set ($#k5_prvect_3 :::"[:"::: ) (Set (Var "X")) "," (Set "(" ($#k10_prvect_2 :::"product"::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "Y")) ($#k9_finseq_1 :::"*>"::: ) ) ")" ) ($#k5_prvect_3 :::":]"::: ) ) "st" (Bool "(" (Bool (Set (Var "I")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool (Set (Var "I")) "is" ($#v2_funct_2 :::"onto"::: ) ) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "Y")) "holds" (Bool (Set (Set (Var "I")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "x")) "," (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "y")) ($#k12_finseq_1 :::"*>"::: ) ) ($#k1_domain_1 :::"]"::: ) ))) ")" ) & (Bool "(" "for" (Set (Var "v")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set ($#k5_prvect_3 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k5_prvect_3 :::":]"::: ) ) "holds" (Bool (Set (Set (Var "I")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "v")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "w")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "I")) ($#k3_funct_2 :::"."::: ) (Set (Var "v")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "I")) ($#k3_funct_2 :::"."::: ) (Set (Var "w")) ")" ))) ")" ) & (Bool "(" "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set ($#k5_prvect_3 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k5_prvect_3 :::":]"::: ) ) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set (Set (Var "I")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "r")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "v")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set (Var "I")) ($#k3_funct_2 :::"."::: ) (Set (Var "v")) ")" )))) ")" ) & (Bool (Set (Set (Var "I")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set ($#k5_prvect_3 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k5_prvect_3 :::":]"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set ($#k5_prvect_3 :::"[:"::: ) (Set (Var "X")) "," (Set "(" ($#k10_prvect_2 :::"product"::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "Y")) ($#k9_finseq_1 :::"*>"::: ) ) ")" ) ($#k5_prvect_3 :::":]"::: ) ))) ")" ))) ; theorem :: PRVECT_3:22 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"RealLinearSpace-Sequence":::) (Bool "for" (Set (Var "Y")) "being" ($#l1_rlvect_1 :::"RealLinearSpace":::) (Bool "ex" (Set (Var "I")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_prvect_3 :::"[:"::: ) (Set "(" ($#k10_prvect_2 :::"product"::: ) (Set (Var "X")) ")" ) "," (Set (Var "Y")) ($#k5_prvect_3 :::":]"::: ) ) "," (Set "(" ($#k10_prvect_2 :::"product"::: ) (Set "(" (Set (Var "X")) ($#k7_finseq_1 :::"^"::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "Y")) ($#k9_finseq_1 :::"*>"::: ) ) ")" ) ")" ) "st" (Bool "(" (Bool (Set (Var "I")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool (Set (Var "I")) "is" ($#v2_funct_2 :::"onto"::: ) ) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k10_prvect_2 :::"product"::: ) (Set (Var "X")) ")" ) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "Y")) (Bool "ex" (Set (Var "x1")) "," (Set (Var "y1")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "x1"))) & (Bool (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "y")) ($#k12_finseq_1 :::"*>"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "y1"))) & (Bool (Set (Set (Var "I")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "x1")) ($#k7_finseq_1 :::"^"::: ) (Set (Var "y1")))) ")" ))) ")" ) & (Bool "(" "for" (Set (Var "v")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set ($#k5_prvect_3 :::"[:"::: ) (Set "(" ($#k10_prvect_2 :::"product"::: ) (Set (Var "X")) ")" ) "," (Set (Var "Y")) ($#k5_prvect_3 :::":]"::: ) ) "holds" (Bool (Set (Set (Var "I")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "v")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "w")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "I")) ($#k3_funct_2 :::"."::: ) (Set (Var "v")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "I")) ($#k3_funct_2 :::"."::: ) (Set (Var "w")) ")" ))) ")" ) & (Bool "(" "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set ($#k5_prvect_3 :::"[:"::: ) (Set "(" ($#k10_prvect_2 :::"product"::: ) (Set (Var "X")) ")" ) "," (Set (Var "Y")) ($#k5_prvect_3 :::":]"::: ) ) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set (Set (Var "I")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "r")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "v")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set (Var "I")) ($#k3_funct_2 :::"."::: ) (Set (Var "v")) ")" )))) ")" ) & (Bool (Set (Set (Var "I")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set ($#k5_prvect_3 :::"[:"::: ) (Set "(" ($#k10_prvect_2 :::"product"::: ) (Set (Var "X")) ")" ) "," (Set (Var "Y")) ($#k5_prvect_3 :::":]"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k10_prvect_2 :::"product"::: ) (Set "(" (Set (Var "X")) ($#k7_finseq_1 :::"^"::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "Y")) ($#k9_finseq_1 :::"*>"::: ) ) ")" ) ")" ))) ")" )))) ; theorem :: PRVECT_3:23 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "ex" (Set (Var "I")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k7_prvect_3 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k7_prvect_3 :::":]"::: ) ) "," (Set ($#k7_prvect_3 :::"[:"::: ) (Set (Var "X")) "," (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "Y")) ($#k9_finseq_1 :::"*>"::: ) ) ")" ) ($#k7_prvect_3 :::":]"::: ) ) "st" (Bool "(" (Bool (Set (Var "I")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool (Set (Var "I")) "is" ($#v2_funct_2 :::"onto"::: ) ) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "Y")) "holds" (Bool (Set (Set (Var "I")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "x")) "," (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "y")) ($#k12_finseq_1 :::"*>"::: ) ) ($#k1_domain_1 :::"]"::: ) ))) ")" ) & (Bool "(" "for" (Set (Var "v")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set ($#k7_prvect_3 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k7_prvect_3 :::":]"::: ) ) "holds" (Bool (Set (Set (Var "I")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "v")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "w")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "I")) ($#k3_funct_2 :::"."::: ) (Set (Var "v")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "I")) ($#k3_funct_2 :::"."::: ) (Set (Var "w")) ")" ))) ")" ) & (Bool "(" "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set ($#k7_prvect_3 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k7_prvect_3 :::":]"::: ) ) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set (Set (Var "I")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "r")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "v")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set (Var "I")) ($#k3_funct_2 :::"."::: ) (Set (Var "v")) ")" )))) ")" ) & (Bool (Set (Set (Var "I")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set ($#k7_prvect_3 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k7_prvect_3 :::":]"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set ($#k7_prvect_3 :::"[:"::: ) (Set (Var "X")) "," (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "Y")) ($#k9_finseq_1 :::"*>"::: ) ) ")" ) ($#k7_prvect_3 :::":]"::: ) ))) & (Bool "(" "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set ($#k7_prvect_3 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k7_prvect_3 :::":]"::: ) ) "holds" (Bool (Set ($#k1_normsp_0 :::"||."::: ) (Set "(" (Set (Var "I")) ($#k3_funct_2 :::"."::: ) (Set (Var "v")) ")" ) ($#k1_normsp_0 :::".||"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k1_normsp_0 :::"||."::: ) (Set (Var "v")) ($#k1_normsp_0 :::".||"::: ) )) ")" ) ")" ))) ; theorem :: PRVECT_3:24 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"RealNormSpace-Sequence":::) (Bool "for" (Set (Var "Y")) "being" ($#l1_normsp_1 :::"RealNormSpace":::) (Bool "ex" (Set (Var "I")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k7_prvect_3 :::"[:"::: ) (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set (Var "X")) ")" ) "," (Set (Var "Y")) ($#k7_prvect_3 :::":]"::: ) ) "," (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set "(" (Set (Var "X")) ($#k7_finseq_1 :::"^"::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "Y")) ($#k9_finseq_1 :::"*>"::: ) ) ")" ) ")" ) "st" (Bool "(" (Bool (Set (Var "I")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool (Set (Var "I")) "is" ($#v2_funct_2 :::"onto"::: ) ) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set (Var "X")) ")" ) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "Y")) (Bool "ex" (Set (Var "x1")) "," (Set (Var "y1")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "x1"))) & (Bool (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "y")) ($#k12_finseq_1 :::"*>"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "y1"))) & (Bool (Set (Set (Var "I")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "x1")) ($#k7_finseq_1 :::"^"::: ) (Set (Var "y1")))) ")" ))) ")" ) & (Bool "(" "for" (Set (Var "v")) "," (Set (Var "w")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set ($#k7_prvect_3 :::"[:"::: ) (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set (Var "X")) ")" ) "," (Set (Var "Y")) ($#k7_prvect_3 :::":]"::: ) ) "holds" (Bool (Set (Set (Var "I")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "v")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "w")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "I")) ($#k3_funct_2 :::"."::: ) (Set (Var "v")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "I")) ($#k3_funct_2 :::"."::: ) (Set (Var "w")) ")" ))) ")" ) & (Bool "(" "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set ($#k7_prvect_3 :::"[:"::: ) (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set (Var "X")) ")" ) "," (Set (Var "Y")) ($#k7_prvect_3 :::":]"::: ) ) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set (Set (Var "I")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "r")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "v")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k1_rlvect_1 :::"*"::: ) (Set "(" (Set (Var "I")) ($#k3_funct_2 :::"."::: ) (Set (Var "v")) ")" )))) ")" ) & (Bool (Set (Set (Var "I")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set ($#k7_prvect_3 :::"[:"::: ) (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set (Var "X")) ")" ) "," (Set (Var "Y")) ($#k7_prvect_3 :::":]"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set "(" (Set (Var "X")) ($#k7_finseq_1 :::"^"::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "Y")) ($#k9_finseq_1 :::"*>"::: ) ) ")" ) ")" ))) & (Bool "(" "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set ($#k7_prvect_3 :::"[:"::: ) (Set "(" ($#k14_prvect_2 :::"product"::: ) (Set (Var "X")) ")" ) "," (Set (Var "Y")) ($#k7_prvect_3 :::":]"::: ) ) "holds" (Bool (Set ($#k1_normsp_0 :::"||."::: ) (Set "(" (Set (Var "I")) ($#k3_funct_2 :::"."::: ) (Set (Var "v")) ")" ) ($#k1_normsp_0 :::".||"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k1_normsp_0 :::"||."::: ) (Set (Var "v")) ($#k1_normsp_0 :::".||"::: ) )) ")" ) ")" )))) ;