fvsum_1.miz



    begin

    reserve i,j,k for Nat;

    theorem :: FVSUM_1:1

    

     Th1: for K be Abelian non empty addLoopStr holds the addF of K is commutative

    proof

      let K be Abelian non empty addLoopStr;

      now

        let a,b be Element of K;

        

        thus (the addF of K . (a,b)) = (a + b)

        .= (the addF of K . (b,a)) by RLVECT_1: 2;

      end;

      hence thesis by BINOP_1:def 2;

    end;

    theorem :: FVSUM_1:2

    

     Th2: for K be add-associative non empty addLoopStr holds the addF of K is associative

    proof

      let K be add-associative non empty addLoopStr;

      now

        let a,b,c be Element of K;

        

        thus (the addF of K . (a,(the addF of K . (b,c)))) = (a + (b + c))

        .= ((a + b) + c) by RLVECT_1:def 3

        .= (the addF of K . ((the addF of K . (a,b)),c));

      end;

      hence thesis by BINOP_1:def 3;

    end;

    theorem :: FVSUM_1:3

    

     Th3: for K be commutative non empty multMagma holds the multF of K is commutative

    proof

      let K be commutative non empty multMagma;

      now

        let a,b be Element of K;

        

        thus (the multF of K . (a,b)) = (a * b)

        .= (b * a)

        .= (the multF of K . (b,a));

      end;

      hence thesis by BINOP_1:def 2;

    end;

    registration

      let K be Abelian non empty addLoopStr;

      cluster the addF of K -> commutative;

      coherence by Th1;

    end

    registration

      let K be add-associative non empty addLoopStr;

      cluster the addF of K -> associative;

      coherence by Th2;

    end

    registration

      let K be commutative non empty multMagma;

      cluster the multF of K -> commutative;

      coherence by Th3;

    end

    theorem :: FVSUM_1:4

    

     Th4: for K be commutative left_unital non empty multLoopStr holds ( 1. K) is_a_unity_wrt the multF of K

    proof

      let K be commutative left_unital non empty multLoopStr;

      set o = the multF of K;

      now

        let h be Element of K;

        

        thus (o . (( 1. K),h)) = (( 1. K) * h)

        .= h;

        

        thus (o . (h,( 1. K))) = (h * ( 1. K))

        .= h;

      end;

      hence thesis by BINOP_1: 3;

    end;

    theorem :: FVSUM_1:5

    

     Th5: for K be commutative left_unital non empty multLoopStr holds ( the_unity_wrt the multF of K) = ( 1. K)

    proof

      let K be commutative left_unital non empty multLoopStr;

      reconsider e = ( 1. K) as Element of K;

      e is_a_unity_wrt the multF of K by Th4;

      hence thesis by BINOP_1:def 8;

    end;

    theorem :: FVSUM_1:6

    

     Th6: for K be left_zeroed right_zeroed non empty addLoopStr holds ( 0. K) is_a_unity_wrt the addF of K

    proof

      let K be left_zeroed right_zeroed non empty addLoopStr;

      now

        let a be Element of K;

        

        thus (the addF of K . (( 0. K),a)) = (( 0. K) + a)

        .= a by ALGSTR_1:def 2;

        

        thus (the addF of K . (a,( 0. K))) = (a + ( 0. K))

        .= a by RLVECT_1:def 4;

      end;

      hence thesis by BINOP_1: 3;

    end;

    theorem :: FVSUM_1:7

    

     Th7: for K be left_zeroed right_zeroed non empty addLoopStr holds ( the_unity_wrt the addF of K) = ( 0. K)

    proof

      let K be left_zeroed right_zeroed non empty addLoopStr;

      reconsider e = ( 0. K) as Element of K;

      e is_a_unity_wrt the addF of K by Th6;

      hence thesis by BINOP_1:def 8;

    end;

    theorem :: FVSUM_1:8

    

     Th8: for K be left_zeroed right_zeroed non empty addLoopStr holds the addF of K is having_a_unity

    proof

      let K be left_zeroed right_zeroed non empty addLoopStr;

      take ( 0. K);

      thus thesis by Th6;

    end;

    theorem :: FVSUM_1:9

    for K be commutative left_unital non empty multLoopStr holds the multF of K is having_a_unity;

    theorem :: FVSUM_1:10

    

     Th10: for K be distributive non empty doubleLoopStr holds the multF of K is_distributive_wrt the addF of K

    proof

      let K be distributive non empty doubleLoopStr;

      now

        let a1,a2,a3 be Element of K;

        

        thus (the multF of K . (a1,(the addF of K . (a2,a3)))) = (a1 * (a2 + a3))

        .= ((a1 * a2) + (a1 * a3)) by VECTSP_1:def 7

        .= (the addF of K . ((the multF of K . (a1,a2)),(the multF of K . (a1,a3))));

        

        thus (the multF of K . ((the addF of K . (a1,a2)),a3)) = ((a1 + a2) * a3)

        .= ((a1 * a3) + (a2 * a3)) by VECTSP_1:def 7

        .= (the addF of K . ((the multF of K . (a1,a3)),(the multF of K . (a2,a3))));

      end;

      hence thesis by BINOP_1: 11;

    end;

    definition

      let K be non empty multMagma;

      let a be Element of K;

      :: FVSUM_1:def1

      func a multfield -> UnOp of the carrier of K equals (the multF of K [;] (a,( id the carrier of K)));

      coherence ;

    end

    definition

      let K be non empty addLoopStr;

      :: FVSUM_1:def2

      func diffield (K) -> BinOp of the carrier of K equals (the addF of K * (( id the carrier of K),( comp K)));

      correctness ;

    end

    theorem :: FVSUM_1:11

    

     Th11: for K be non empty addLoopStr, a1,a2 be Element of K holds (( diffield K) . (a1,a2)) = (a1 - a2)

    proof

      let K be non empty addLoopStr, a1,a2 be Element of K;

      

      thus (( diffield K) . (a1,a2)) = (the addF of K . (a1,(( comp K) . a2))) by FINSEQOP: 82

      .= (a1 - a2) by VECTSP_1:def 13;

    end;

    

     Lm1: for K be non empty multMagma, a,b be Element of K holds ((the multF of K [;] (b,( id the carrier of K))) . a) = (b * a)

    proof

      let K be non empty multMagma, a,b be Element of K;

      

      thus ((the multF of K [;] (b,( id the carrier of K))) . a) = (the multF of K . (b,(( id the carrier of K) . a))) by FUNCOP_1: 53

      .= (b * a);

    end;

    theorem :: FVSUM_1:12

    

     Th12: for K be distributive non empty doubleLoopStr, a be Element of K holds (a multfield ) is_distributive_wrt the addF of K by Th10, FINSEQOP: 54;

    theorem :: FVSUM_1:13

    

     Th13: for K be left_zeroed right_zeroed add-associative right_complementable non empty addLoopStr holds ( comp K) is_an_inverseOp_wrt the addF of K

    proof

      let K be left_zeroed right_zeroed add-associative right_complementable non empty addLoopStr;

      now

        let a be Element of K;

        

        thus (the addF of K . (a,(( comp K) . a))) = (a + ( - a)) by VECTSP_1:def 13

        .= ( 0. K) by RLVECT_1: 5

        .= ( the_unity_wrt the addF of K) by Th7;

        

        thus (the addF of K . ((( comp K) . a),a)) = (( - a) + a) by VECTSP_1:def 13

        .= ( 0. K) by RLVECT_1: 5

        .= ( the_unity_wrt the addF of K) by Th7;

      end;

      hence thesis by FINSEQOP:def 1;

    end;

    theorem :: FVSUM_1:14

    

     Th14: for K be left_zeroed right_zeroed add-associative right_complementable non empty addLoopStr holds the addF of K is having_an_inverseOp

    proof

      let K be left_zeroed right_zeroed add-associative right_complementable non empty addLoopStr;

      ( comp K) is_an_inverseOp_wrt the addF of K by Th13;

      hence thesis by FINSEQOP:def 2;

    end;

    theorem :: FVSUM_1:15

    

     Th15: for K be left_zeroed right_zeroed add-associative right_complementable non empty addLoopStr holds ( the_inverseOp_wrt the addF of K) = ( comp K)

    proof

      let K be left_zeroed right_zeroed add-associative right_complementable non empty addLoopStr;

      

       A1: ( comp K) is_an_inverseOp_wrt the addF of K by Th13;

      the addF of K is having_a_unity & the addF of K is having_an_inverseOp by Th8, Th14;

      hence thesis by A1, FINSEQOP:def 3;

    end;

    theorem :: FVSUM_1:16

    for K be right_zeroed add-associative right_complementable Abelian non empty addLoopStr holds ( comp K) is_distributive_wrt the addF of K

    proof

      let K be right_zeroed add-associative right_complementable Abelian non empty addLoopStr;

      the addF of K is having_a_unity by Th8;

      then ( the_inverseOp_wrt the addF of K) is_distributive_wrt the addF of K by Th14, FINSEQOP: 63;

      hence thesis by Th15;

    end;

    begin

    definition

      let K be non empty addLoopStr;

      let p1,p2 be FinSequence of the carrier of K;

      :: FVSUM_1:def3

      func p1 + p2 -> FinSequence of the carrier of K equals (the addF of K .: (p1,p2));

      correctness ;

    end

    theorem :: FVSUM_1:17

    for K be non empty addLoopStr, p1,p2 be FinSequence of the carrier of K, a1,a2 be Element of K, i be Nat st i in ( dom (p1 + p2)) & a1 = (p1 . i) & a2 = (p2 . i) holds ((p1 + p2) . i) = (a1 + a2) by FUNCOP_1: 22;

    definition

      let i;

      let K be non empty addLoopStr;

      let R1,R2 be Element of (i -tuples_on the carrier of K);

      :: original: +

      redefine

      func R1 + R2 -> Element of (i -tuples_on the carrier of K) ;

      coherence by FINSEQ_2: 120;

    end

    theorem :: FVSUM_1:18

    for K be non empty addLoopStr, a1,a2 be Element of K, R1,R2 be Element of (i -tuples_on the carrier of K) holds j in ( Seg i) & a1 = (R1 . j) & a2 = (R2 . j) implies ((R1 + R2) . j) = (a1 + a2)

    proof

      let K be non empty addLoopStr, a1,a2 be Element of K, R1,R2 be Element of (i -tuples_on the carrier of K);

      assume j in ( Seg i);

      then j in ( Seg ( len (R1 + R2))) by CARD_1:def 7;

      then j in ( dom (R1 + R2)) by FINSEQ_1:def 3;

      hence thesis by FUNCOP_1: 22;

    end;

    theorem :: FVSUM_1:19

    for K be non empty addLoopStr, a1,a2 be Element of K holds ( <*a1*> + <*a2*>) = <*(a1 + a2)*> by FINSEQ_2: 74;

    theorem :: FVSUM_1:20

    for K be non empty addLoopStr, a1,a2 be Element of K holds ((i |-> a1) + (i |-> a2)) = (i |-> (a1 + a2)) by FINSEQOP: 17;

    

     Lm2: for K be left_zeroed right_zeroed non empty addLoopStr, R be Element of (i -tuples_on the carrier of K) holds (R + (i |-> ( 0. K))) = R

    proof

      let K be left_zeroed right_zeroed non empty addLoopStr, R be Element of (i -tuples_on the carrier of K);

      ( the_unity_wrt the addF of K) = ( 0. K) & the addF of K is having_a_unity by Th7, Th8;

      hence thesis by FINSEQOP: 56;

    end;

    theorem :: FVSUM_1:21

    

     Th21: for K be Abelian left_zeroed right_zeroed non empty addLoopStr, R be Element of (i -tuples_on the carrier of K) holds (R + (i |-> ( 0. K))) = R & R = ((i |-> ( 0. K)) + R)

    proof

      let K be Abelian left_zeroed right_zeroed non empty addLoopStr, R be Element of (i -tuples_on the carrier of K);

      thus (R + (i |-> ( 0. K))) = R by Lm2;

      hence thesis by FINSEQOP: 33;

    end;

    definition

      let K be non empty addLoopStr;

      let p be FinSequence of the carrier of K;

      :: FVSUM_1:def4

      func - p -> FinSequence of the carrier of K equals (( comp K) * p);

      correctness ;

    end

    reserve K for non empty addLoopStr,

a for Element of K,

p for FinSequence of the carrier of K,

R for Element of (i -tuples_on the carrier of K);

    theorem :: FVSUM_1:22

    

     Th22: i in ( dom ( - p)) & a = (p . i) implies (( - p) . i) = ( - a)

    proof

      assume i in ( dom ( - p)) & a = (p . i);

      then (( - p) . i) = (( comp K) . a) by FUNCT_1: 12;

      hence thesis by VECTSP_1:def 13;

    end;

    definition

      let i;

      let K be non empty addLoopStr;

      let R be Element of (i -tuples_on the carrier of K);

      :: original: -

      redefine

      func - R -> Element of (i -tuples_on the carrier of K) ;

      coherence by FINSEQ_2: 113;

    end

    theorem :: FVSUM_1:23

    j in ( Seg i) & a = (R . j) implies (( - R) . j) = ( - a)

    proof

      assume j in ( Seg i);

      then j in ( Seg ( len ( - R))) by CARD_1:def 7;

      then j in ( dom ( - R)) by FINSEQ_1:def 3;

      hence thesis by Th22;

    end;

    theorem :: FVSUM_1:24

    ( - <*a*>) = <*( - a)*>

    proof

      

      thus ( - <*a*>) = <*(( comp K) . a)*> by FINSEQ_2: 35

      .= <*( - a)*> by VECTSP_1:def 13;

    end;

    theorem :: FVSUM_1:25

    

     Th25: ( - (i |-> a)) = (i |-> ( - a))

    proof

      

      thus ( - (i |-> a)) = (i |-> (( comp K) . a)) by FINSEQOP: 16

      .= (i |-> ( - a)) by VECTSP_1:def 13;

    end;

    

     Lm3: for K be left_zeroed right_zeroed add-associative right_complementable non empty addLoopStr, R be Element of (i -tuples_on the carrier of K) holds (R + ( - R)) = (i |-> ( 0. K))

    proof

      let K be left_zeroed right_zeroed add-associative right_complementable non empty addLoopStr, R be Element of (i -tuples_on the carrier of K);

      

       A1: the addF of K is having_an_inverseOp & the addF of K is having_a_unity by Th8, Th14;

      

      thus (R + ( - R)) = (the addF of K .: (R,(( the_inverseOp_wrt the addF of K) * R))) by Th15

      .= (i |-> ( the_unity_wrt the addF of K)) by A1, FINSEQOP: 73

      .= (i |-> ( 0. K)) by Th7;

    end;

    theorem :: FVSUM_1:26

    

     Th26: for K be Abelian right_zeroed add-associative right_complementable non empty addLoopStr, R be Element of (i -tuples_on the carrier of K) holds (R + ( - R)) = (i |-> ( 0. K)) & (( - R) + R) = (i |-> ( 0. K))

    proof

      let K be Abelian right_zeroed add-associative right_complementable non empty addLoopStr, R be Element of (i -tuples_on the carrier of K);

      thus (R + ( - R)) = (i |-> ( 0. K)) by Lm3;

      hence thesis by FINSEQOP: 33;

    end;

    reserve K for left_zeroed right_zeroed add-associative right_complementable non empty addLoopStr,

R,R1,R2 for Element of (i -tuples_on the carrier of K);

    theorem :: FVSUM_1:27

    

     Th27: (R1 + R2) = (i |-> ( 0. K)) implies R1 = ( - R2) & R2 = ( - R1)

    proof

      

       A1: the addF of K is having_an_inverseOp & ( the_inverseOp_wrt the addF of K) = ( comp K) by Th14, Th15;

      ( the_unity_wrt the addF of K) = ( 0. K) & the addF of K is having_a_unity by Th7, Th8;

      hence thesis by A1, FINSEQOP: 74;

    end;

    theorem :: FVSUM_1:28

    

     Th28: ( - ( - R)) = R

    proof

      (R + ( - R)) = (i |-> ( 0. K)) by Lm3;

      hence thesis by Th27;

    end;

    theorem :: FVSUM_1:29

    ( - R1) = ( - R2) implies R1 = R2

    proof

      assume ( - R1) = ( - R2);

      

      hence R1 = ( - ( - R2)) by Th28

      .= R2 by Th28;

    end;

    

     Lm4: (R1 + R) = (R2 + R) implies R1 = R2

    proof

      assume (R1 + R) = (R2 + R);

      then (R1 + (R + ( - R))) = ((R2 + R) + ( - R)) by FINSEQOP: 28;

      then

       A1: (R1 + (R + ( - R))) = (R2 + (R + ( - R))) by FINSEQOP: 28;

      (R + ( - R)) = (i |-> ( 0. K)) by Lm3;

      then R1 = (R2 + (i |-> ( 0. K))) by A1, Lm2;

      hence thesis by Lm2;

    end;

    theorem :: FVSUM_1:30

    for K be Abelian right_zeroed add-associative right_complementable non empty addLoopStr, R,R1,R2 be Element of (i -tuples_on the carrier of K) holds (R1 + R) = (R2 + R) or (R1 + R) = (R + R2) implies R1 = R2

    proof

      let K be Abelian right_zeroed add-associative right_complementable non empty addLoopStr, R,R1,R2 be Element of (i -tuples_on the carrier of K);

      (R1 + R) = (R2 + R) iff (R1 + R) = (R + R2) by FINSEQOP: 33;

      hence thesis by Lm4;

    end;

    theorem :: FVSUM_1:31

    

     Th31: for K be Abelian right_zeroed add-associative right_complementable non empty addLoopStr, R1,R2 be Element of (i -tuples_on the carrier of K) holds ( - (R1 + R2)) = (( - R1) + ( - R2))

    proof

      let K be Abelian right_zeroed add-associative right_complementable non empty addLoopStr, R1,R2 be Element of (i -tuples_on the carrier of K);

      ((R1 + R2) + (( - R1) + ( - R2))) = (((R1 + R2) + ( - R1)) + ( - R2)) by FINSEQOP: 28

      .= (((R2 + R1) + ( - R1)) + ( - R2)) by FINSEQOP: 33

      .= ((R2 + (R1 + ( - R1))) + ( - R2)) by FINSEQOP: 28

      .= ((R2 + (i |-> ( 0. K))) + ( - R2)) by Lm3

      .= (R2 + ( - R2)) by Lm2

      .= (i |-> ( 0. K)) by Lm3;

      hence thesis by Th27;

    end;

    definition

      let K be non empty addLoopStr;

      let p1,p2 be FinSequence of the carrier of K;

      :: FVSUM_1:def5

      func p1 - p2 -> FinSequence of the carrier of K equals (( diffield K) .: (p1,p2));

      correctness ;

    end

    reserve K for non empty addLoopStr,

a1,a2 for Element of K,

p1,p2 for FinSequence of the carrier of K,

R1,R2 for Element of (i -tuples_on the carrier of K);

    theorem :: FVSUM_1:32

    

     Th32: i in ( dom (p1 - p2)) & a1 = (p1 . i) & a2 = (p2 . i) implies ((p1 - p2) . i) = (a1 - a2)

    proof

      assume i in ( dom (p1 - p2)) & a1 = (p1 . i) & a2 = (p2 . i);

      then ((p1 - p2) . i) = (( diffield K) . (a1,a2)) by FUNCOP_1: 22;

      hence thesis by Th11;

    end;

    definition

      let i;

      let K be non empty addLoopStr;

      let R1,R2 be Element of (i -tuples_on the carrier of K);

      :: original: -

      redefine

      func R1 - R2 -> Element of (i -tuples_on the carrier of K) ;

      coherence by FINSEQ_2: 120;

    end

    theorem :: FVSUM_1:33

    j in ( Seg i) & a1 = (R1 . j) & a2 = (R2 . j) implies ((R1 - R2) . j) = (a1 - a2)

    proof

      assume j in ( Seg i);

      then j in ( Seg ( len (R1 - R2))) by CARD_1:def 7;

      then j in ( dom (R1 - R2)) by FINSEQ_1:def 3;

      hence thesis by Th32;

    end;

    theorem :: FVSUM_1:34

    ( <*a1*> - <*a2*>) = <*(a1 - a2)*>

    proof

      

      thus ( <*a1*> - <*a2*>) = <*(( diffield K) . (a1,a2))*> by FINSEQ_2: 74

      .= <*(a1 - a2)*> by Th11;

    end;

    theorem :: FVSUM_1:35

    ((i |-> a1) - (i |-> a2)) = (i |-> (a1 - a2))

    proof

      

      thus ((i |-> a1) - (i |-> a2)) = (i |-> (( diffield K) . (a1,a2))) by FINSEQOP: 17

      .= (i |-> (a1 - a2)) by Th11;

    end;

    theorem :: FVSUM_1:36

    for K be add-associative right_complementable left_zeroed right_zeroed non empty addLoopStr, R be Element of (i -tuples_on the carrier of K) holds (R - (i |-> ( 0. K))) = R

    proof

      let K be add-associative right_complementable left_zeroed right_zeroed non empty addLoopStr, R be Element of (i -tuples_on the carrier of K);

      

      thus (R - (i |-> ( 0. K))) = (R + ( - (i |-> ( 0. K)))) by FINSEQOP: 84

      .= (R + (i |-> ( - ( 0. K)))) by Th25

      .= (R + (i |-> ( 0. K))) by RLVECT_1: 12

      .= R by Lm2;

    end;

    theorem :: FVSUM_1:37

    for K be Abelian left_zeroed right_zeroed non empty addLoopStr, R be Element of (i -tuples_on the carrier of K) holds ((i |-> ( 0. K)) - R) = ( - R)

    proof

      let K be Abelian left_zeroed right_zeroed non empty addLoopStr, R be Element of (i -tuples_on the carrier of K);

      

      thus ((i |-> ( 0. K)) - R) = ((i |-> ( 0. K)) + ( - R)) by FINSEQOP: 84

      .= ( - R) by Th21;

    end;

    theorem :: FVSUM_1:38

    for K be left_zeroed right_zeroed add-associative right_complementable non empty addLoopStr, R1,R2 be Element of (i -tuples_on the carrier of K) holds (R1 - ( - R2)) = (R1 + R2)

    proof

      let K be left_zeroed right_zeroed add-associative right_complementable non empty addLoopStr, R1,R2 be Element of (i -tuples_on the carrier of K);

      

      thus (R1 - ( - R2)) = (R1 + ( - ( - R2))) by FINSEQOP: 84

      .= (R1 + R2) by Th28;

    end;

    reserve K for Abelian right_zeroed add-associative right_complementable non empty addLoopStr,

R,R1,R2,R3 for Element of (i -tuples_on the carrier of K);

    theorem :: FVSUM_1:39

    ( - (R1 - R2)) = (R2 - R1)

    proof

      

      thus ( - (R1 - R2)) = ( - (R1 + ( - R2))) by FINSEQOP: 84

      .= (( - R1) + ( - ( - R2))) by Th31

      .= (( - R1) + R2) by Th28

      .= (R2 + ( - R1)) by FINSEQOP: 33

      .= (R2 - R1) by FINSEQOP: 84;

    end;

    theorem :: FVSUM_1:40

    

     Th40: ( - (R1 - R2)) = (( - R1) + R2)

    proof

      

      thus ( - (R1 - R2)) = ( - (R1 + ( - R2))) by FINSEQOP: 84

      .= (( - R1) + ( - ( - R2))) by Th31

      .= (( - R1) + R2) by Th28;

    end;

    theorem :: FVSUM_1:41

    

     Th41: (R - R) = (i |-> ( 0. K))

    proof

      

      thus (R - R) = (R + ( - R)) by FINSEQOP: 84

      .= (i |-> ( 0. K)) by Lm3;

    end;

    theorem :: FVSUM_1:42

    (R1 - R2) = (i |-> ( 0. K)) implies R1 = R2

    proof

      assume (R1 - R2) = (i |-> ( 0. K));

      then (R1 + ( - R2)) = (i |-> ( 0. K)) by FINSEQOP: 84;

      then R1 = ( - ( - R2)) by Th27;

      hence thesis by Th28;

    end;

    theorem :: FVSUM_1:43

    ((R1 - R2) - R3) = (R1 - (R2 + R3))

    proof

      

      thus ((R1 - R2) - R3) = ((R1 - R2) + ( - R3)) by FINSEQOP: 84

      .= ((R1 + ( - R2)) + ( - R3)) by FINSEQOP: 84

      .= (R1 + (( - R2) + ( - R3))) by FINSEQOP: 28

      .= (R1 + ( - (R2 + R3))) by Th31

      .= (R1 - (R2 + R3)) by FINSEQOP: 84;

    end;

    theorem :: FVSUM_1:44

    

     Th44: (R1 + (R2 - R3)) = ((R1 + R2) - R3)

    proof

      

      thus (R1 + (R2 - R3)) = (R1 + (R2 + ( - R3))) by FINSEQOP: 84

      .= ((R1 + R2) + ( - R3)) by FINSEQOP: 28

      .= ((R1 + R2) - R3) by FINSEQOP: 84;

    end;

    theorem :: FVSUM_1:45

    (R1 - (R2 - R3)) = ((R1 - R2) + R3)

    proof

      

      thus (R1 - (R2 - R3)) = (R1 + ( - (R2 - R3))) by FINSEQOP: 84

      .= (R1 + (( - R2) + R3)) by Th40

      .= ((R1 + ( - R2)) + R3) by FINSEQOP: 28

      .= ((R1 - R2) + R3) by FINSEQOP: 84;

    end;

    theorem :: FVSUM_1:46

    R1 = ((R1 + R) - R)

    proof

      

      thus R1 = (R1 + (i |-> ( 0. K))) by Lm2

      .= (R1 + (R - R)) by Th41

      .= ((R1 + R) - R) by Th44;

    end;

    theorem :: FVSUM_1:47

    R1 = ((R1 - R) + R)

    proof

      

      thus R1 = (R1 + (i |-> ( 0. K))) by Lm2

      .= (R1 + (( - R) + R)) by Th26

      .= ((R1 + ( - R)) + R) by FINSEQOP: 28

      .= ((R1 - R) + R) by FINSEQOP: 84;

    end;

    reserve K for non empty multMagma,

a,a9,a1,a2 for Element of K,

p for FinSequence of the carrier of K,

R for Element of (i -tuples_on the carrier of K);

    theorem :: FVSUM_1:48

    

     Th48: for a,b be Element of K holds ((the multF of K [;] (a,( id the carrier of K))) . b) = (a * b)

    proof

      let a,b be Element of K;

      

      thus ((the multF of K [;] (a,( id the carrier of K))) . b) = (the multF of K . (a,(( id the carrier of K) . b))) by FUNCOP_1: 53

      .= (a * b);

    end;

    theorem :: FVSUM_1:49

    for a,b be Element of K holds ((a multfield ) . b) = (a * b) by Th48;

    definition

      let K be non empty multMagma;

      let p be FinSequence of the carrier of K;

      let a be Element of K;

      :: FVSUM_1:def6

      func a * p -> FinSequence of the carrier of K equals ((a multfield ) * p);

      correctness ;

    end

    theorem :: FVSUM_1:50

    

     Th50: i in ( dom (a * p)) & a9 = (p . i) implies ((a * p) . i) = (a * a9)

    proof

      assume

       A1: i in ( dom (a * p)) & a9 = (p . i);

      then

       A2: a9 in ( dom (the multF of K [;] (a,( id the carrier of K)))) by FUNCT_1: 11;

      

      thus ((a * p) . i) = ((the multF of K [;] (a,( id the carrier of K))) . a9) by A1, FUNCT_1: 12

      .= (the multF of K . (a,(( id the carrier of K) . a9))) by A2, FUNCOP_1: 32

      .= (a * a9);

    end;

    definition

      let i;

      let K be non empty multMagma;

      let R be Element of (i -tuples_on the carrier of K);

      let a be Element of K;

      :: original: *

      redefine

      func a * R -> Element of (i -tuples_on the carrier of K) ;

      coherence by FINSEQ_2: 113;

    end

    theorem :: FVSUM_1:51

    j in ( Seg i) & a9 = (R . j) implies ((a * R) . j) = (a * a9)

    proof

      assume j in ( Seg i);

      then j in ( Seg ( len (a * R))) by CARD_1:def 7;

      then j in ( dom (a * R)) by FINSEQ_1:def 3;

      hence thesis by Th50;

    end;

    theorem :: FVSUM_1:52

    (a * <*a1*>) = <*(a * a1)*>

    proof

      

      thus (a * <*a1*>) = <*((the multF of K [;] (a,( id the carrier of K))) . a1)*> by FINSEQ_2: 35

      .= <*(a * a1)*> by Th48;

    end;

    theorem :: FVSUM_1:53

    

     Th53: (a1 * (i |-> a2)) = (i |-> (a1 * a2))

    proof

      

      thus (a1 * (i |-> a2)) = (i |-> ((the multF of K [;] (a1,( id the carrier of K))) . a2)) by FINSEQOP: 16

      .= (i |-> (a1 * a2)) by Th48;

    end;

    theorem :: FVSUM_1:54

    for K be associative non empty multMagma, a1,a2 be Element of K, R be Element of (i -tuples_on the carrier of K) holds ((a1 * a2) * R) = (a1 * (a2 * R))

    proof

      let K be associative non empty multMagma, a1,a2 be Element of K, R be Element of (i -tuples_on the carrier of K);

      set F = the multF of K;

      set f = ( id the carrier of K);

      

      thus ((a1 * a2) * R) = ((F [;] (a1,(F [;] (a2,f)))) * R) by FUNCOP_1: 62

      .= (((the multF of K [;] (a1,( id the carrier of K))) * (the multF of K [;] (a2,( id the carrier of K)))) * R) by FUNCOP_1: 55

      .= (a1 * (a2 * R)) by RELAT_1: 36;

    end;

    reserve K for distributive non empty doubleLoopStr,

a,a1,a2 for Element of K,

R,R1,R2 for Element of (i -tuples_on the carrier of K);

    theorem :: FVSUM_1:55

    ((a1 + a2) * R) = ((a1 * R) + (a2 * R))

    proof

      

      thus ((a1 + a2) * R) = ((the addF of K .: ((the multF of K [;] (a1,( id the carrier of K))),(the multF of K [;] (a2,( id the carrier of K))))) * R) by Th10, FINSEQOP: 35

      .= ((a1 * R) + (a2 * R)) by FUNCOP_1: 25;

    end;

    theorem :: FVSUM_1:56

    (a * (R1 + R2)) = ((a * R1) + (a * R2)) by Th12, FINSEQOP: 51;

    theorem :: FVSUM_1:57

    for K be distributive commutative left_unital non empty doubleLoopStr, R be Element of (i -tuples_on the carrier of K) holds (( 1. K) * R) = R

    proof

      let K be distributive commutative left_unital non empty doubleLoopStr, R be Element of (i -tuples_on the carrier of K);

      

       A1: ( rng R) c= the carrier of K by FINSEQ_1:def 4;

      ( the_unity_wrt the multF of K) = ( 1. K) by Th5;

      

      hence (( 1. K) * R) = (( id the carrier of K) * R) by FINSEQOP: 44

      .= R by A1, RELAT_1: 53;

    end;

    theorem :: FVSUM_1:58

    for K be add-associative right_zeroed right_complementable distributive non empty doubleLoopStr, R be Element of (i -tuples_on the carrier of K) holds (( 0. K) * R) = (i |-> ( 0. K))

    proof

      let K be add-associative right_zeroed right_complementable distributive non empty doubleLoopStr, R be Element of (i -tuples_on the carrier of K);

      

       A1: ( rng R) c= the carrier of K by FINSEQ_1:def 4;

      

       A2: the addF of K is having_an_inverseOp by Th14;

      

       A3: ( the_unity_wrt the addF of K) = ( 0. K) & the addF of K is having_a_unity by Th7, Th8;

      

      thus (( 0. K) * R) = (the multF of K [;] (( 0. K),(( id the carrier of K) * R))) by FUNCOP_1: 34

      .= (the multF of K [;] (( 0. K),R)) by A1, RELAT_1: 53

      .= (i |-> ( 0. K)) by A3, A2, Th10, FINSEQOP: 76;

    end;

    theorem :: FVSUM_1:59

    for K be add-associative right_zeroed right_complementable commutative left_unital distributive non empty doubleLoopStr, R be Element of (i -tuples_on the carrier of K) holds (( - ( 1. K)) * R) = ( - R)

    proof

      let K be add-associative right_zeroed right_complementable commutative left_unital distributive non empty doubleLoopStr, R be Element of (i -tuples_on the carrier of K);

      

       A1: (( comp K) . ( 1. K)) = ( - ( 1. K)) & ( the_unity_wrt the multF of K) = ( 1. K) by Th5, VECTSP_1:def 13;

      

       A2: the addF of K is having_an_inverseOp & ( the_inverseOp_wrt the addF of K) = ( comp K) by Th14, Th15;

      the multF of K is having_a_unity & the addF of K is having_a_unity by Th8;

      hence thesis by A1, A2, Th10, FINSEQOP: 68;

    end;

    definition

      let M be non empty multMagma, p1,p2 be FinSequence of the carrier of M;

      :: FVSUM_1:def7

      func mlt (p1,p2) -> FinSequence of the carrier of M equals (the multF of M .: (p1,p2));

      correctness ;

    end

    reserve K for non empty multMagma,

a1,a2,b1,b2 for Element of K,

p1,p2 for FinSequence of the carrier of K,

R1,R2 for Element of (i -tuples_on the carrier of K);

    theorem :: FVSUM_1:60

    i in ( dom ( mlt (p1,p2))) & a1 = (p1 . i) & a2 = (p2 . i) implies (( mlt (p1,p2)) . i) = (a1 * a2) by FUNCOP_1: 22;

    definition

      let i;

      let K be non empty multMagma;

      let R1,R2 be Element of (i -tuples_on the carrier of K);

      :: original: mlt

      redefine

      func mlt (R1,R2) -> Element of (i -tuples_on the carrier of K) ;

      coherence by FINSEQ_2: 120;

    end

    theorem :: FVSUM_1:61

    j in ( Seg i) & a1 = (R1 . j) & a2 = (R2 . j) implies (( mlt (R1,R2)) . j) = (a1 * a2)

    proof

      assume j in ( Seg i);

      then j in ( Seg ( len ( mlt (R1,R2)))) by CARD_1:def 7;

      then j in ( dom ( mlt (R1,R2))) by FINSEQ_1:def 3;

      hence thesis by FUNCOP_1: 22;

    end;

    theorem :: FVSUM_1:62

    ( mlt ( <*a1*>, <*a2*>)) = <*(a1 * a2)*> by FINSEQ_2: 74;

    

     Lm5: ( mlt ( <*a1, a2*>, <*b1, b2*>)) = <*(a1 * b1), (a2 * b2)*>

    proof

       <*a1, a2*> = ( <*a1*> ^ <*a2*>) & <*b1, b2*> = ( <*b1*> ^ <*b2*>) by FINSEQ_1:def 9;

      

      hence ( mlt ( <*a1, a2*>, <*b1, b2*>)) = (( mlt ( <*a1*>, <*b1*>)) ^ <*(a2 * b2)*>) by FINSEQOP: 10

      .= ( <*(a1 * b1)*> ^ <*(a2 * b2)*>) by FINSEQ_2: 74

      .= <*(a1 * b1), (a2 * b2)*> by FINSEQ_1:def 9;

    end;

    reserve K for commutative non empty multMagma,

p,q for FinSequence of the carrier of K,

R1,R2 for Element of (i -tuples_on the carrier of K);

    theorem :: FVSUM_1:63

    ( mlt (R1,R2)) = ( mlt (R2,R1)) by FINSEQOP: 33;

    theorem :: FVSUM_1:64

    

     Th64: ( mlt (p,q)) = ( mlt (q,p))

    proof

      reconsider r = ( mlt (p,q)) as FinSequence of the carrier of K;

      reconsider s = ( mlt (q,p)) as FinSequence of the carrier of K;

      reconsider k = ( min (( len p),( len q))) as Element of NAT by XXREAL_0: 15;

      

       A1: ( len r) = ( min (( len p),( len q))) by FINSEQ_2: 71;

      then

       A2: ( dom r) = ( Seg k) by FINSEQ_1:def 3;

      ( min (( len p),( len q))) <= ( len q) by XXREAL_0: 17;

      then ( Seg k) c= ( Seg ( len q)) by FINSEQ_1: 5;

      then

       A3: ( Seg k) c= ( dom q) by FINSEQ_1:def 3;

      ( min (( len p),( len q))) <= ( len p) by XXREAL_0: 17;

      then ( Seg k) c= ( Seg ( len p)) by FINSEQ_1: 5;

      then

       A4: ( Seg k) c= ( dom p) by FINSEQ_1:def 3;

      

       A5: ( len s) = ( min (( len q),( len p))) by FINSEQ_2: 71;

      then

       A6: ( dom s) = ( Seg k) by FINSEQ_1:def 3;

      

       A7: ( dom r) = ( Seg k) by A1, FINSEQ_1:def 3;

      now

        let i be Nat;

        assume

         A8: i in ( dom r);

        then

        reconsider d1 = (p . i), d2 = (q . i) as Element of K by A4, A3, A2, FINSEQ_2: 11;

        

        thus (r . i) = (d1 * d2) by A8, FUNCOP_1: 22

        .= (d2 * d1)

        .= (s . i) by A7, A6, A8, FUNCOP_1: 22;

      end;

      hence thesis by A1, A5, FINSEQ_2: 9;

    end;

    theorem :: FVSUM_1:65

    for K be associative non empty multMagma, R1,R2,R3 be Element of (i -tuples_on the carrier of K) holds ( mlt (R1,( mlt (R2,R3)))) = ( mlt (( mlt (R1,R2)),R3)) by FINSEQOP: 28;

    reserve K for commutative associative non empty multMagma,

a,a1,a2 for Element of K,

R for Element of (i -tuples_on the carrier of K);

    theorem :: FVSUM_1:66

    

     Th66: ( mlt ((i |-> a),R)) = (a * R) & ( mlt (R,(i |-> a))) = (a * R)

    proof

      

      thus ( mlt ((i |-> a),R)) = (the multF of K [;] (a,R)) by FINSEQOP: 20

      .= (a * R) by FINSEQOP: 22;

      hence thesis by FINSEQOP: 33;

    end;

    theorem :: FVSUM_1:67

    ( mlt ((i |-> a1),(i |-> a2))) = (i |-> (a1 * a2))

    proof

      

      thus ( mlt ((i |-> a1),(i |-> a2))) = (a1 * (i |-> a2)) by Th66

      .= (i |-> (a1 * a2)) by Th53;

    end;

    theorem :: FVSUM_1:68

    for K be associative non empty multMagma, a be Element of K, R1,R2 be Element of (i -tuples_on the carrier of K) holds (a * ( mlt (R1,R2))) = ( mlt ((a * R1),R2)) by FINSEQOP: 26;

    reserve K for commutative associative non empty multMagma,

a for Element of K,

R,R1,R2 for Element of (i -tuples_on the carrier of K);

    theorem :: FVSUM_1:69

    (a * ( mlt (R1,R2))) = ( mlt ((a * R1),R2)) & (a * ( mlt (R1,R2))) = ( mlt (R1,(a * R2)))

    proof

      thus (a * ( mlt (R1,R2))) = ( mlt ((a * R1),R2)) by FINSEQOP: 26;

      

      thus (a * ( mlt (R1,R2))) = (a * ( mlt (R2,R1))) by FINSEQOP: 33

      .= ( mlt ((a * R2),R1)) by FINSEQOP: 26

      .= ( mlt (R1,(a * R2))) by FINSEQOP: 33;

    end;

    theorem :: FVSUM_1:70

    (a * R) = ( mlt ((i |-> a),R)) by Th66;

    begin

    registration

      cluster Abelian right_zeroed -> left_zeroed for non empty addLoopStr;

      coherence

      proof

        let L be non empty addLoopStr such that

         A1: L is Abelian and

         A2: L is right_zeroed;

        let x be Element of L;

        

        thus (( 0. L) + x) = (x + ( 0. L)) by A1, RLVECT_1:def 2

        .= x by A2, RLVECT_1:def 4;

      end;

    end

    definition

      let K be Abelian add-associative right_zeroed right_complementable non empty addLoopStr;

      let p be FinSequence of the carrier of K;

      :: original: Sum

      redefine

      :: FVSUM_1:def8

      func Sum (p) equals (the addF of K $$ p);

      compatibility

      proof

        set q = ( <*> the carrier of K);

        deffunc F( Nat) = (the addF of K $$ (p | $1));

        let s be Element of K;

        consider f be sequence of the carrier of K such that

         A1: for i be Element of NAT holds (f . i) = F(i) from FUNCT_2:sch 4;

        

         A2: for i be Nat holds (f . i) = F(i)

        proof

          let i be Nat;

          i in NAT by ORDINAL1:def 12;

          hence thesis by A1;

        end;

        hereby

          defpred P[ set, set] means ex q be FinSequence of the carrier of K st q = (p * ( Sgm ( dom (p | $1)))) & $2 = ( Sum q);

          assume

           A3: s = ( Sum p);

          

           A4: for x be Element of ( Fin NAT ) holds ex y be Element of K st P[x, y]

          proof

            let B be Element of ( Fin NAT );

            per cases ;

              suppose

               A5: ( dom p) = {} ;

              reconsider u = ( Sum ( <*> the carrier of K)) as Element of K;

              reconsider q = ( <*> the carrier of K) as FinSequence of the carrier of K;

              take u, q;

              p = {} by A5;

              hence q = (p * ( Sgm ( dom (p | B))));

              thus thesis;

            end;

              suppose ( dom p) <> {} ;

              then

              reconsider domp = ( dom p) as non empty set;

              reconsider p9 = p as Function of domp, the carrier of K by FINSEQ_2: 26;

              

               A6: ( dom (p | B)) c= ( dom p) by RELAT_1: 60;

              reconsider pB = (p | B) as FinSubsequence;

              ( rng ( Sgm ( dom pB))) = ( dom pB) by FINSEQ_1: 50;

              then

              reconsider p99 = ( Sgm ( dom (p | B))) as FinSequence of domp by A6, FINSEQ_1:def 4;

              reconsider q = (p9 * p99) as FinSequence of the carrier of K;

              reconsider u = ( Sum q) as Element of K;

              take u, q;

              thus thesis;

            end;

          end;

          consider G be Function of ( Fin NAT ), the carrier of K such that

           A7: for B be Element of ( Fin NAT ) holds P[B, (G . B)] from FUNCT_2:sch 3( A4);

           A8:

          now

            let B9 be Element of ( Fin NAT ) such that B9 c= ( dom p) and B9 <> {} ;

            let x be Element of NAT ;

            set f2 = ( Sgm ( dom (p | (B9 \/ {x})))), f3 = (f2 -| x), f4 = (f2 |-- x);

            reconsider Y = (( finSeg ( len f2)) \ (f2 " {x})) as finite set;

            

             A9: ( Seg ( len f2)) = ( dom f2) by FINSEQ_1:def 3;

            set R = ( rng (f2 | Y));

            set M = (f2 * ( Sgm Y));

            

             A10: ( rng ( Sgm Y)) = Y by FINSEQ_1:def 13;

            ( dom ( Sgm Y)) = ( finSeg ( card Y)) by FINSEQ_3: 40;

            then ( dom M) = ( Seg ( card Y)) by A9, A10, RELAT_1: 27;

            then

            reconsider M as FinSequence by FINSEQ_1:def 2;

            ( rng f2) c= NAT & ( rng M) c= ( rng f2) by FINSEQ_1:def 4, RELAT_1: 26;

            then ( rng M) c= NAT by XBOOLE_1: 1;

            then

            reconsider L = (f2 * ( Sgm Y)) as FinSequence of NAT by FINSEQ_1:def 4;

            now

              let y be object;

              hereby

                assume y in ( rng L);

                then

                consider x be object such that

                 A11: x in ( dom L) and

                 A12: y = (L . x) by FUNCT_1:def 3;

                x in ( dom ( Sgm Y)) by A11, FUNCT_1: 11;

                then

                 A13: (( Sgm Y) . x) in Y by A10, FUNCT_1:def 3;

                y = (f2 . (( Sgm Y) . x)) by A11, A12, FUNCT_1: 12;

                hence y in R by A9, A13, FUNCT_1: 50;

              end;

              assume y in R;

              then

              consider x be object such that

               A14: x in ( dom (f2 | Y)) and

               A15: y = ((f2 | Y) . x) by FUNCT_1:def 3;

              

               A16: x in (( dom f2) /\ Y) by A14, RELAT_1: 61;

              then

               A17: x in Y by XBOOLE_0:def 4;

              then

              consider z be object such that

               A18: z in ( dom ( Sgm Y)) and

               A19: x = (( Sgm Y) . z) by A10, FUNCT_1:def 3;

              x in ( dom f2) by A16, XBOOLE_0:def 4;

              then

               A20: z in ( dom (f2 * ( Sgm Y))) by A18, A19, FUNCT_1: 11;

              

              then (L . z) = (f2 . (( Sgm Y) . z)) by FUNCT_1: 12

              .= y by A15, A17, A19, FUNCT_1: 49;

              hence y in ( rng L) by A20, FUNCT_1:def 3;

            end;

            then

             A21: ( rng L) = R by TARSKI: 2;

            x in {x} by TARSKI:def 1;

            then

             A22: x in (B9 \/ {x}) by XBOOLE_0:def 3;

            ( dom (p | (B9 \/ {x}))) = (( dom p) /\ (B9 \/ {x})) by RELAT_1: 61;

            then ( dom (p | (B9 \/ {x}))) c= ( dom p) by XBOOLE_1: 17;

            then

             A23: ( dom (p | (B9 \/ {x}))) c= ( Seg ( len p)) by FINSEQ_1:def 3;

            reconsider pB9x = (p | (B9 \/ {x})) as FinSubsequence;

            ( rng f2) c= ( Seg ( len p)) by A23, FINSEQ_1:def 13;

            then

             A24: ( rng f2) c= ( dom p) by FINSEQ_1:def 3;

            R c= ( rng f2) by RELAT_1: 70;

            then R c= ( dom p) by A24, XBOOLE_1: 1;

            then

             A25: R c= ( Seg ( len p)) by FINSEQ_1:def 3;

            reconsider pp = (p | (B9 \/ {x})) as FinSubsequence;

            

             A26: ( dom (p | B9)) = (( dom p) /\ B9) by RELAT_1: 61;

             A27:

            now

              let l,m,k1,k2 be Nat;

              assume that

               A28: 1 <= l and

               A29: l < m and

               A30: m <= ( len L) and

               A31: k1 = (L . l) & k2 = (L . m);

              l <= ( len L) by A29, A30, XXREAL_0: 2;

              then

               A32: l in ( dom L) by A28, FINSEQ_3: 25;

              then

               A33: (L . l) = (f2 . (( Sgm Y) . l)) by FUNCT_1: 12;

              

               A34: (( Sgm Y) . l) in ( dom f2) by A32, FUNCT_1: 11;

              1 <= m by A28, A29, XXREAL_0: 2;

              then

               A35: m in ( dom L) by A30, FINSEQ_3: 25;

              then

               A36: (L . m) = (f2 . (( Sgm Y) . m)) by FUNCT_1: 12;

              m in ( dom ( Sgm Y)) by A35, FUNCT_1: 11;

              then

               A37: m <= ( len ( Sgm Y)) by FINSEQ_3: 25;

              

               A38: (( Sgm Y) . m) in ( dom f2) by A35, FUNCT_1: 11;

              reconsider l, m as Element of NAT by ORDINAL1:def 12;

              reconsider K1 = (( Sgm Y) . l), K2 = (( Sgm Y) . m) as Element of NAT by A34, A38;

              

               A39: 1 <= K1 by A34, FINSEQ_3: 25;

              

               A40: K2 <= ( len f2) by A38, FINSEQ_3: 25;

              K1 < K2 by A28, A29, A37, FINSEQ_1:def 13;

              hence k1 < k2 by A23, A31, A33, A36, A39, A40, FINSEQ_1:def 13;

            end;

            assume

             A41: x in (( dom p) \ B9);

            then

             A42: x in ( dom p) by XBOOLE_0:def 5;

            then

            reconsider D = ( dom p), E = ( rng p) as non empty set by RELAT_1: 42;

            x in ( dom p) by A41, XBOOLE_0:def 5;

            then

             A43: {x} c= ( dom p) by ZFMISC_1: 31;

            (p . x) = (p /. x) by A42, PARTFUN1:def 6;

            then

            reconsider px = (p . x) as Element of K;

            

             A44: ( dom <*px*>) = ( Seg 1) by FINSEQ_1: 38;

            ( rng <*x*>) = {x} by FINSEQ_1: 38;

            then ( dom <*x*>) = ( Seg 1) & ( rng <*x*>) c= ( dom p) by A42, FINSEQ_1: 38, ZFMISC_1: 31;

            then

             A45: ( dom (p * <*x*>)) = ( dom <*px*>) by A44, RELAT_1: 27;

             A46:

            now

              let e be object;

              assume

               A47: e in ( dom <*px*>);

              then

               A48: e = 1 by A44, FINSEQ_1: 2, TARSKI:def 1;

              

              thus ((p * <*x*>) . e) = (p . ( <*x*> . e)) by A45, A47, FUNCT_1: 12

              .= (p . x) by A48, FINSEQ_1: 40

              .= ( <*px*> . e) by A48, FINSEQ_1: 40;

            end;

            reconsider x9 = x as Element of D by A41, XBOOLE_0:def 5;

            reconsider p9 = p as Function of D, E by FUNCT_2: 1;

            

             A49: E c= the carrier of K by FINSEQ_1:def 4;

             not x in B9 by A41, XBOOLE_0:def 5;

            then

             A50: not x in ( dom (p | B9)) by A26, XBOOLE_0:def 4;

            

             A51: ( rng ( Sgm ( dom pp))) = ( dom pp) by FINSEQ_1: 50;

            then

             A52: ( rng f2) c= ( dom p) by RELAT_1: 60;

            ( dom pp) = (( dom p) /\ (B9 \/ {x})) by RELAT_1: 61;

            then

             A53: x in ( rng f2) by A51, A42, A22, XBOOLE_0:def 4;

            then ( rng f4) c= ( rng f2) by FINSEQ_4: 44;

            then

             A54: ( rng f4) c= D by A52, XBOOLE_1: 1;

            ( rng f3) c= ( rng f2) by A53, FINSEQ_4: 39;

            then ( rng f3) c= D by A52, XBOOLE_1: 1;

            then

            reconsider f39 = f3, f49 = f4 as FinSequence of D by A54, FINSEQ_1:def 4;

            consider q2 be FinSequence of the carrier of K such that

             A55: q2 = (p * ( Sgm ( dom (p | (B9 \/ {x}))))) and

             A56: (G . (B9 \/ {.x.})) = ( Sum q2) by A7;

            reconsider p3 = (p9 * f39), p4 = (p9 * f49) as FinSequence of E;

            ( rng p3) c= E by FINSEQ_1:def 4;

            then

             A57: ( rng p3) c= the carrier of K by A49, XBOOLE_1: 1;

            ( rng p4) c= E by FINSEQ_1:def 4;

            then ( rng p4) c= the carrier of K by A49, XBOOLE_1: 1;

            then

            reconsider p3, p4 as FinSequence of the carrier of K by A57, FINSEQ_1:def 4;

            consider q1 be FinSequence of the carrier of K such that

             A58: q1 = (p * ( Sgm ( dom (p | B9)))) and

             A59: (G . B9) = ( Sum q1) by A7;

            

             A60: f2 is one-to-one by A23, FINSEQ_3: 92;

            ( rng (( Sgm ( dom (p | (B9 \/ {x})))) | (( Seg ( len f2)) \ (f2 " {x})))) = (( Sgm ( dom (p | (B9 \/ {x})))) .: (( Seg ( len f2)) \ (f2 " {x}))) by RELAT_1: 115

            .= (( Sgm ( dom (p | (B9 \/ {x})))) .: (( dom f2) \ (f2 " {x}))) by FINSEQ_1:def 3

            .= ((( Sgm ( dom (p | (B9 \/ {x})))) .: ( dom f2)) \ {x}) by SETWISEO: 6

            .= (( rng ( Sgm ( dom pB9x))) \ {x}) by RELAT_1: 113

            .= (( dom (p | (B9 \/ {x}))) \ {x}) by FINSEQ_1: 50

            .= ((( dom p) /\ (B9 \/ {x})) \ {x}) by RELAT_1: 61

            .= (((( dom p) /\ B9) \/ (( dom p) /\ {x})) \ {x}) by XBOOLE_1: 23

            .= (((( dom p) /\ B9) \/ {x}) \ {x}) by A43, XBOOLE_1: 28

            .= (( dom (p | B9)) \ {x}) by A26, XBOOLE_1: 40

            .= ( dom (p | B9)) by A50, ZFMISC_1: 57;

            

            then ( Sgm ( dom (p | B9))) = (f2 * ( Sgm (( Seg ( len f2)) \ (f2 " {x})))) by A25, A21, A27, FINSEQ_1:def 13

            .= (f2 * ( Sgm (( dom f2) \ (f2 " {x})))) by FINSEQ_1:def 3

            .= (f2 - {x}) by FINSEQ_3:def 1

            .= (f3 ^ f4) by A53, A60, FINSEQ_4: 55;

            then

             A61: q1 = (p3 ^ p4) by A58, FINSEQOP: 9;

            q2 = (p9 * ((f39 ^ <*x9*>) ^ f49)) by A55, A53, FINSEQ_4: 51

            .= ((p9 * (f39 ^ <*x9*>)) ^ (p9 * f49)) by FINSEQOP: 9

            .= (((p9 * f39) ^ (p9 * <*x9*>)) ^ (p9 * f49)) by FINSEQOP: 9

            .= ((p3 ^ <*px*>) ^ p4) by A45, A46, FUNCT_1: 2;

            

            hence (G . (B9 \/ {x})) = (( Sum (p3 ^ <*px*>)) + ( Sum p4)) by A56, RLVECT_1: 41

            .= ((( Sum p3) + ( Sum <*px*>)) + ( Sum p4)) by RLVECT_1: 41

            .= ((( Sum p3) + ( Sum p4)) + ( Sum <*px*>)) by RLVECT_1:def 3

            .= (( Sum q1) + ( Sum <*px*>)) by A61, RLVECT_1: 41

            .= (the addF of K . (( Sum q1),px)) by RLVECT_1: 44

            .= (the addF of K . ((G . B9),(( [#] (p,( the_unity_wrt the addF of K))) . x))) by A59, A42, SETWOP_2: 20;

          end;

           A62:

          now

            let x be Element of NAT ;

            consider q be FinSequence of the carrier of K such that

             A63: q = (p * ( Sgm ( dom (p | {x})))) and

             A64: (G . {.x.}) = ( Sum q) by A7;

            

             A65: {} c= ( Seg 0 );

            per cases ;

              suppose

               A66: not x in ( dom p);

              then ( dom p) misses {x} by ZFMISC_1: 50;

              then (( dom p) /\ {x}) = {} by XBOOLE_0:def 7;

              

              then q = (p * ( Sgm {} )) by A63, RELAT_1: 61

              .= (p * {} ) by A65, FINSEQ_1: 51

              .= ( <*> the carrier of K);

              

              hence (G . {x}) = ( 0. K) by A64, RLVECT_1: 43

              .= ( the_unity_wrt the addF of K) by Th7

              .= (( [#] (p,( the_unity_wrt the addF of K))) . x) by A66, SETWOP_2: 20;

            end;

              suppose

               A67: x in ( dom p);

              then (p . x) = (p /. x) by PARTFUN1:def 6;

              then

              reconsider px = (p . x) as Element of K;

              

               A68: ( dom <*px*>) = ( Seg 1) by FINSEQ_1: 38;

              ( rng <*x*>) = {x} by FINSEQ_1: 38;

              then ( dom <*x*>) = ( Seg 1) & ( rng <*x*>) c= ( dom p) by A67, FINSEQ_1: 38, ZFMISC_1: 31;

              then

               A69: ( dom (p * <*x*>)) = ( dom <*px*>) by A68, RELAT_1: 27;

               A70:

              now

                let e be object;

                assume

                 A71: e in ( dom <*px*>);

                then

                 A72: e = 1 by A68, FINSEQ_1: 2, TARSKI:def 1;

                

                thus ((p * <*x*>) . e) = (p . ( <*x*> . e)) by A69, A71, FUNCT_1: 12

                .= (p . x) by A72, FINSEQ_1: 40

                .= ( <*px*> . e) by A72, FINSEQ_1: 40;

              end;

              

               A73: x <> 0 by A67, FINSEQ_3: 25;

              q = (p * ( Sgm (( dom p) /\ {x}))) by A63, RELAT_1: 61

              .= (p * ( Sgm {x})) by A67, ZFMISC_1: 46

              .= (p * <*x*>) by A73, FINSEQ_3: 44

              .= <*px*> by A69, A70, FUNCT_1: 2;

              

              hence (G . {x}) = px by A64, RLVECT_1: 44

              .= (( [#] (p,( the_unity_wrt the addF of K))) . x) by A67, SETWOP_2: 20;

            end;

          end;

           A74:

          now

            let e be Element of K;

            assume

             A75: e is_a_unity_wrt the addF of K;

            ( 0. K) is_a_unity_wrt the addF of K by Th6;

            then

             A76: e = ( 0. K) by A75, BINOP_1: 10;

            

             A77: {} c= ( Seg 0 );

            consider q be FinSequence of the carrier of K such that

             A78: q = (p * ( Sgm ( dom (p | ( {}. NAT ) qua set)))) and

             A79: (G . ( {}. NAT )) = ( Sum q) by A7;

            q = (p * ( Sgm ( dom {} ))) by A78

            .= (p * {} ) by A77, FINSEQ_1: 51

            .= ( <*> the carrier of K);

            hence e = (G . {} ) by A79, A76, RLVECT_1: 43;

          end;

          consider q1 be FinSequence of the carrier of K such that

           A80: q1 = (p * ( Sgm ( dom (p | ( dom p))))) and

           A81: (G . ( findom p)) = ( Sum q1) by A7;

          

           A82: the addF of K is having_a_unity by Th8;

          q1 = (p * ( Sgm ( dom p))) by A80

          .= (p * ( Sgm ( Seg ( len p)))) by FINSEQ_1:def 3

          .= (p * ( idseq ( len p))) by FINSEQ_3: 48

          .= p by FINSEQ_2: 54;

          

          hence s = (the addF of K $$ (( findom p),( [#] (p,( the_unity_wrt the addF of K))))) by A3, A82, A81, A74, A62, A8, SETWISEO:def 3

          .= (the addF of K $$ p) by Th8, SETWOP_2:def 2;

        end;

        

         A83: (p | ( len p)) = (p | ( Seg ( len p))) by FINSEQ_1:def 15

        .= (p | ( dom p)) by FINSEQ_1:def 3

        .= p;

         A84:

        now

          let j be Nat;

          let a be Element of K;

          assume that

           A85: j < ( len p) and

           A86: a = (p . (j + 1));

          

           A87: (j + 1) <= ( len p) by A85, NAT_1: 13;

          then

           A88: ( len (p | (j + 1))) = (j + 1) by FINSEQ_1: 59;

          j <= (j + 1) by NAT_1: 11;

          then

           A89: ( Seg j) c= ( Seg (j + 1)) by FINSEQ_1: 5;

          

           A90: (p | j) = (p | ( Seg j)) by FINSEQ_1:def 15

          .= ((p | ( Seg (j + 1))) | ( Seg j)) by A89, RELAT_1: 74

          .= ((p | (j + 1)) | ( Seg j)) by FINSEQ_1:def 15;

          

           A91: 1 <= (j + 1) by NAT_1: 11;

          then

           A92: (j + 1) in ( dom (p | (j + 1))) by A88, FINSEQ_3: 25;

          (j + 1) in ( dom p) by A87, A91, FINSEQ_3: 25;

          

          then a = (p /. (j + 1)) by A86, PARTFUN1:def 6

          .= ((p | (j + 1)) /. (j + 1)) by A92, FINSEQ_4: 70

          .= ((p | (j + 1)) . (j + 1)) by A92, PARTFUN1:def 6;

          then (p | (j + 1)) = ((p | j) ^ <*a*>) by A88, A90, FINSEQ_3: 55;

          

          hence (f . (j + 1)) = (the addF of K $$ ((p | j) ^ <*a*>)) by A2

          .= (the addF of K . ((the addF of K $$ (p | j)),a)) by Th8, FINSOP_1: 4

          .= ((f . j) + a) by A2;

        end;

        (p | 0 ) = q;

        

        then

         A93: (f . 0 ) = (the addF of K $$ q) by A2

        .= ( the_unity_wrt the addF of K) by Th8, FINSOP_1: 10

        .= ( 0. K) by Th7;

        assume s = (the addF of K $$ p);

        then s = (f . ( len p)) by A2, A83;

        hence thesis by A93, A84, RLVECT_1:def 12;

      end;

    end

    reserve K for add-associative right_zeroed right_complementable non empty addLoopStr,

a for Element of K,

p for FinSequence of the carrier of K;

    theorem :: FVSUM_1:71

    ( Sum (p ^ <*a*>)) = (( Sum p) + a)

    proof

      

      thus ( Sum (p ^ <*a*>)) = (( Sum p) + ( Sum <*a*>)) by RLVECT_1: 41

      .= (( Sum p) + a) by RLVECT_1: 44;

    end;

    theorem :: FVSUM_1:72

    ( Sum ( <*a*> ^ p)) = (a + ( Sum p))

    proof

      

      thus ( Sum ( <*a*> ^ p)) = (( Sum <*a*>) + ( Sum p)) by RLVECT_1: 41

      .= (a + ( Sum p)) by RLVECT_1: 44;

    end;

    theorem :: FVSUM_1:73

    for K be Abelian add-associative right_zeroed right_complementable distributive non empty doubleLoopStr, a be Element of K, p be FinSequence of the carrier of K holds ( Sum (a * p)) = (a * ( Sum p))

    proof

      let K be Abelian add-associative right_zeroed distributive right_complementable non empty doubleLoopStr, a be Element of K, p be FinSequence of the carrier of K;

      set rM = (the multF of K [;] (a,( id the carrier of K)));

      the addF of K is having_a_unity & the multF of K is_distributive_wrt the addF of K by Th8, Th10;

      

      hence ( Sum (a * p)) = (rM . ( Sum p)) by Th14, SETWOP_2: 30

      .= (a * ( Sum p)) by Lm1;

    end;

    theorem :: FVSUM_1:74

    for K be non empty addLoopStr holds for R be Element of ( 0 -tuples_on the carrier of K) holds ( Sum R) = ( 0. K)

    proof

      let K be non empty addLoopStr, R be Element of ( 0 -tuples_on the carrier of K);

      R = ( <*> the carrier of K);

      hence thesis by RLVECT_1: 43;

    end;

    reserve K for Abelian add-associative right_zeroed right_complementable non empty addLoopStr,

p for FinSequence of the carrier of K,

R1,R2 for Element of (i -tuples_on the carrier of K);

    theorem :: FVSUM_1:75

    ( Sum ( - p)) = ( - ( Sum p))

    proof

      the addF of K is having_an_inverseOp & ( the_inverseOp_wrt the addF of K) = ( comp K) by Th14, Th15;

      

      hence ( Sum ( - p)) = (( comp K) . ( Sum p)) by Th8, SETWOP_2: 31

      .= ( - ( Sum p)) by VECTSP_1:def 13;

    end;

    theorem :: FVSUM_1:76

    ( Sum (R1 + R2)) = (( Sum R1) + ( Sum R2)) by Th8, SETWOP_2: 35;

    theorem :: FVSUM_1:77

    ( Sum (R1 - R2)) = (( Sum R1) - ( Sum R2))

    proof

      the addF of K is having_an_inverseOp & ( the_inverseOp_wrt the addF of K) = ( comp K) by Th14, Th15;

      

      hence ( Sum (R1 - R2)) = (( diffield K) . (( Sum R1),(the addF of K $$ R2))) by Th8, SETWOP_2: 37

      .= (( Sum R1) - ( Sum R2)) by Th11;

    end;

    begin

    

     Lm6: for K be commutative well-unital non empty multLoopStr holds ( Product ( <*> the carrier of K)) = ( 1. K)

    proof

      let K be commutative well-unital non empty multLoopStr;

      ( 1. K) = ( 1_ K);

      hence thesis by GROUP_4: 8;

    end;

    reserve K for commutative associative well-unital non empty doubleLoopStr,

a,a1,a2,a3 for Element of K,

p1 for FinSequence of the carrier of K,

R1,R2 for Element of (i -tuples_on the carrier of K);

    theorem :: FVSUM_1:78

    ( Product ( <*a*> ^ p1)) = (a * ( Product p1))

    proof

      

      thus ( Product ( <*a*> ^ p1)) = (( Product <*a*>) * ( Product p1)) by GROUP_4: 5

      .= (a * ( Product p1)) by FINSOP_1: 11;

    end;

    theorem :: FVSUM_1:79

    ( Product <*a1, a2, a3*>) = ((a1 * a2) * a3)

    proof

      

      thus ( Product <*a1, a2, a3*>) = ( Product ( <*a1, a2*> ^ <*a3*>)) by FINSEQ_1: 43

      .= (( Product <*a1, a2*>) * a3) by GROUP_4: 6

      .= ((a1 * a2) * a3) by FINSOP_1: 12;

    end;

    theorem :: FVSUM_1:80

    for R be Element of ( 0 -tuples_on the carrier of K) holds ( Product R) = ( 1. K)

    proof

      let R be Element of ( 0 -tuples_on the carrier of K);

      R = ( <*> the carrier of K);

      hence thesis by Lm6;

    end;

    theorem :: FVSUM_1:81

    ( Product (i |-> ( 1_ K))) = ( 1_ K)

    proof

      ( the_unity_wrt the multF of K) = ( 1_ K) by Th5;

      hence thesis by SETWOP_2: 25;

    end;

    theorem :: FVSUM_1:82

    for K be add-associative right_zeroed right_complementable Abelian commutative associative well-unital distributive almost_left_invertible non degenerated non empty doubleLoopStr holds for p be FinSequence of the carrier of K holds (ex k st k in ( dom p) & (p . k) = ( 0. K)) iff ( Product p) = ( 0. K)

    proof

      let K be add-associative right_zeroed right_complementable Abelian commutative associative well-unital distributive almost_left_invertible non degenerated non empty doubleLoopStr;

      let p be FinSequence of the carrier of K;

      defpred P[ Nat] means for p be FinSequence of the carrier of K st ( len p) = $1 holds (ex k st k in ( Seg $1) & (p . k) = ( 0. K)) iff ( Product p) = ( 0. K);

      

       A1: for i st P[i] holds P[(i + 1)]

      proof

        let i such that

         A2: for p be FinSequence of the carrier of K st ( len p) = i holds (ex k st k in ( Seg i) & (p . k) = ( 0. K)) iff ( Product p) = ( 0. K);

        let p be FinSequence of the carrier of K;

        assume

         A3: ( len p) = (i + 1);

        then

        consider p9 be FinSequence of the carrier of K, a be Element of K such that

         A4: p = (p9 ^ <*a*>) by FINSEQ_2: 19;

        

         A5: (i + 1) = (( len p9) + 1) by A3, A4, FINSEQ_2: 16;

        then

         A6: i = ( len p9) by XCMPLX_1: 2;

        

         A7: ( Product p) = (( Product p9) * a) by A4, GROUP_4: 6;

        thus (ex k st k in ( Seg (i + 1)) & (p . k) = ( 0. K)) implies ( Product p) = ( 0. K)

        proof

          given k such that

           A8: k in ( Seg (i + 1)) and

           A9: (p . k) = ( 0. K);

          now

            per cases by A8, FINSEQ_2: 7;

              suppose

               A10: k in ( Seg i);

              then k in ( dom p9) by A6, FINSEQ_1:def 3;

              then (p9 . k) = (p . k) by A4, FINSEQ_1:def 7;

              then ( Product p9) = ( 0. K) by A2, A6, A9, A10;

              hence thesis by A7;

            end;

              suppose k = (i + 1);

              then a = ( 0. K) by A4, A5, A9, FINSEQ_1: 42;

              hence thesis by A7;

            end;

          end;

          hence thesis;

        end;

        assume

         A11: ( Product p) = ( 0. K);

        per cases by A7, A11, VECTSP_1: 12;

          suppose ( Product p9) = ( 0. K);

          then

          consider k such that

           A12: k in ( Seg i) and

           A13: (p9 . k) = ( 0. K) by A2, A6;

          k in ( dom p9) by A6, A12, FINSEQ_1:def 3;

          then (p . k) = ( 0. K) by A4, A13, FINSEQ_1:def 7;

          hence thesis by A12, FINSEQ_2: 8;

        end;

          suppose a = ( 0. K);

          then (p . (i + 1)) = ( 0. K) by A4, A5, FINSEQ_1: 42;

          hence thesis by FINSEQ_1: 4;

        end;

      end;

      

       A14: ( Seg ( len p)) = ( dom p) by FINSEQ_1:def 3;

      

       A15: P[ 0 ]

      proof

        let p be FinSequence of the carrier of K;

        assume ( len p) = 0 ;

        then p = ( <*> the carrier of K);

        then

         A16: ( Product p) = ( 1. K) by Lm6;

        thus (ex k st k in ( Seg 0 ) & (p . k) = ( 0. K)) implies ( Product p) = ( 0. K);

        assume ( Product p) = ( 0. K);

        hence thesis by A16;

      end;

      for i holds P[i] from NAT_1:sch 2( A15, A1);

      hence thesis by A14;

    end;

    theorem :: FVSUM_1:83

    ( Product ((i + j) |-> a)) = (( Product (i |-> a)) * ( Product (j |-> a))) by SETWOP_2: 26;

    theorem :: FVSUM_1:84

    ( Product ((i * j) |-> a)) = ( Product (j |-> ( Product (i |-> a)))) by SETWOP_2: 27;

    theorem :: FVSUM_1:85

    ( Product (i |-> (a1 * a2))) = (( Product (i |-> a1)) * ( Product (i |-> a2))) by SETWOP_2: 36;

    theorem :: FVSUM_1:86

    

     Th86: ( Product ( mlt (R1,R2))) = (( Product R1) * ( Product R2)) by SETWOP_2: 35;

    theorem :: FVSUM_1:87

    ( Product (a * R1)) = (( Product (i |-> a)) * ( Product R1))

    proof

      

      thus ( Product (a * R1)) = ( Product ( mlt ((i |-> a),R1))) by Th66

      .= (( Product (i |-> a)) * ( Product R1)) by Th86;

    end;

    begin

    definition

      let K be non empty doubleLoopStr;

      let p,q be FinSequence of the carrier of K;

      :: FVSUM_1:def9

      func p "*" q -> Element of K equals ( Sum ( mlt (p,q)));

      coherence ;

    end

    theorem :: FVSUM_1:88

    for K be commutative associative left_unital Abelian add-associative right_zeroed right_complementable non empty doubleLoopStr holds for a,b be Element of K holds ( <*a*> "*" <*b*>) = (a * b)

    proof

      let K be commutative associative left_unital Abelian add-associative right_zeroed right_complementable non empty doubleLoopStr;

      let a,b be Element of K;

      set p = <*a*>, q = <*b*>;

      set m = ( mlt (p,q));

      m = <*(a * b)*> by FINSEQ_2: 74;

      then m = (1 |-> (a * b)) by FINSEQ_2: 59;

      hence thesis by FINSOP_1: 16;

    end;

    theorem :: FVSUM_1:89

    for K be commutative associative left_unital Abelian add-associative right_zeroed right_complementable non empty doubleLoopStr holds for a1,a2,b1,b2 be Element of K holds ( <*a1, a2*> "*" <*b1, b2*>) = ((a1 * b1) + (a2 * b2))

    proof

      let K be commutative associative left_unital Abelian add-associative right_zeroed right_complementable non empty doubleLoopStr;

      let a1,a2,b1,b2 be Element of K;

      set p = <*a1, a2*>;

      set q = <*b1, b2*>;

      (the addF of K $$ ( mlt (p,q))) = (the addF of K $$ <*(a1 * b1), (a2 * b2)*>) by Lm5

      .= ((a1 * b1) + (a2 * b2)) by FINSOP_1: 12;

      hence thesis;

    end;

    theorem :: FVSUM_1:90

    for p,q be FinSequence of the carrier of K holds (p "*" q) = (q "*" p) by Th64;