prvect_1.miz



    begin

    reserve G for Abelian add-associative right_complementable right_zeroed non empty addLoopStr;

    deffunc car( 1-sorted) = the carrier of $1;

    deffunc ad( addLoopStr) = the addF of $1;

    deffunc cc( non empty addLoopStr) = ( comp $1);

    deffunc zr( addLoopStr) = ( 0. $1);

    theorem :: PRVECT_1:1

    

     Th1: ( 0. G) is_a_unity_wrt the addF of G

    proof

      now

        let x be Element of G;

        

        thus (the addF of G . (( 0. G),x)) = (( 0. G) + x)

        .= x by RLVECT_1: 4;

        

        thus (the addF of G . (x,( 0. G))) = (x + ( 0. G))

        .= x by RLVECT_1: 4;

      end;

      hence thesis by BINOP_1: 3;

    end;

    theorem :: PRVECT_1:2

    

     Th2: for G be AbGroup holds ( comp G) is_an_inverseOp_wrt the addF of G

    proof

      let G be AbGroup;

      

       A1: ( 0. G) is_a_unity_wrt the addF of G by Th1;

      now

        let x be Element of G;

        

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

        .= ( 0. G) by RLVECT_1: 5

        .= ( the_unity_wrt the addF of G) by A1, BINOP_1:def 8;

        

        thus (the addF of G . ((( comp G) . x),x)) = ((( comp G) . x) + x)

        .= (x + ( - x)) by VECTSP_1:def 13

        .= ( 0. G) by RLVECT_1: 5

        .= ( the_unity_wrt the addF of G) by A1, BINOP_1:def 8;

      end;

      hence thesis;

    end;

    

     Lm1: ( comp G) is_an_inverseOp_wrt the addF of G

    proof

      

       A1: ( 0. G) is_a_unity_wrt the addF of G by Th1;

      now

        let x be Element of G;

        

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

        .= ( 0. G) by RLVECT_1: 5

        .= ( the_unity_wrt the addF of G) by A1, BINOP_1:def 8;

        

        thus (the addF of G . ((( comp G) . x),x)) = ((( comp G) . x) + x)

        .= (x + ( - x)) by VECTSP_1:def 13

        .= ( 0. G) by RLVECT_1: 5

        .= ( the_unity_wrt the addF of G) by A1, BINOP_1:def 8;

      end;

      hence thesis;

    end;

    reserve GS for non empty addLoopStr;

    theorem :: PRVECT_1:3

    the addF of GS is commutative associative & ( 0. GS) is_a_unity_wrt the addF of GS & ( comp GS) is_an_inverseOp_wrt the addF of GS implies GS is AbGroup

    proof

      assume that

       A1: the addF of GS is commutative & the addF of GS is associative and

       A2: ( 0. GS) is_a_unity_wrt the addF of GS and

       A3: ( comp GS) is_an_inverseOp_wrt the addF of GS;

      

       A4: GS is right_complementable

      proof

        let x be Element of GS;

        reconsider b = (( comp GS) . x) as Element of GS;

        take b;

        

        thus (x + b) = ( the_unity_wrt the addF of GS) by A3

        .= ( 0. GS) by A2, BINOP_1:def 8;

      end;

      for x,y,z be Element of GS holds (x + y) = (y + x) & ((x + y) + z) = (x + (y + z)) & (x + ( 0. GS)) = x by A1, A2, BINOP_1: 3;

      hence thesis by A4, RLVECT_1:def 2, RLVECT_1:def 3, RLVECT_1:def 4;

    end;

    

     Lm2: the addF of GS is commutative associative implies GS is Abelian add-associative;

    

     Lm3: ( 0. GS) is_a_unity_wrt the addF of GS implies GS is right_zeroed by BINOP_1: 3;

    reserve F for Field;

    

     Lm4: the multF of F is associative

    proof

      let x,y,z be Element of F;

      

      thus (the multF of F . (x,(the multF of F . (y,z)))) = (x * (y * z))

      .= ((x * y) * z) by GROUP_1:def 3

      .= (the multF of F . ((the multF of F . (x,y)),z));

    end;

    theorem :: PRVECT_1:4

    ( 0. F) is_a_unity_wrt the addF of F

    proof

      now

        let x be Element of F;

        

        thus (the addF of F . (( 0. F),x)) = (x + ( 0. F)) by RLVECT_1: 2

        .= x by RLVECT_1: 4;

        

        thus (the addF of F . (x,( 0. F))) = (x + ( 0. F))

        .= x by RLVECT_1: 4;

      end;

      hence thesis by BINOP_1: 3;

    end;

    theorem :: PRVECT_1:5

    

     Th5: ( 1_ F) is_a_unity_wrt the multF of F

    proof

      now

        let x be Element of F;

        

        thus (the multF of F . (( 1_ F),x)) = (( 1_ F) * x)

        .= x;

        

        thus (the multF of F . (x,( 1_ F))) = (x * ( 1_ F))

        .= x;

      end;

      hence thesis by BINOP_1: 3;

    end;

    

     Lm5: the multF of F is_distributive_wrt the addF of F

    proof

      now

        let x,y,z be Element of F;

        

        thus (the multF of F . (x,(the addF of F . (y,z)))) = (x * (y + z))

        .= ((x * y) + (x * z)) by VECTSP_1:def 7

        .= (the addF of F . ((the multF of F . (x,y)),(the multF of F . (x,z))));

        

        thus (the multF of F . ((the addF of F . (x,y)),z)) = ((x + y) * z)

        .= ((x * z) + (y * z)) by VECTSP_1:def 7

        .= (the addF of F . ((the multF of F . (x,z)),(the multF of F . (y,z))));

      end;

      hence thesis by BINOP_1: 11;

    end;

    begin

    reserve F for Field,

n for Nat,

D for non empty set,

d for Element of D,

B for BinOp of D,

C for UnOp of D;

    definition

      let D, n;

      let F be BinOp of D;

      let x,y be Element of (n -tuples_on D);

      :: original: .:

      redefine

      func F .: (x,y) -> Element of (n -tuples_on D) ;

      coherence by FINSEQ_2: 120;

    end

    definition

      let D be non empty set;

      let F be BinOp of D;

      let n be Nat;

      :: PRVECT_1:def1

      func product (F,n) -> BinOp of (n -tuples_on D) means

      : Def1: for x,y be Element of (n -tuples_on D) holds (it . (x,y)) = (F .: (x,y));

      existence

      proof

        defpred P[ set, set, set] means ex x9,y9 be Element of (n -tuples_on D) st $1 = x9 & $2 = y9 & $3 = (F .: (x9,y9));

        

         A1: for x,y be Element of (n -tuples_on D) qua non empty set holds ex z be Element of (n -tuples_on D) qua non empty set st P[x, y, z]

        proof

          let x,y be Element of (n -tuples_on D) qua non empty set;

          reconsider x9 = x, y9 = y as Element of (n -tuples_on D);

          reconsider z = (F .: (x9,y9)) as Element of (n -tuples_on D) qua non empty set;

          take z;

          take x9, y9;

          thus thesis;

        end;

        consider G be BinOp of (n -tuples_on D) such that

         A2: for x,y be Element of (n -tuples_on D) qua non empty set holds P[x, y, (G . (x,y))] from BINOP_1:sch 3( A1);

        take G;

        let p1,p2 be Element of (n -tuples_on D);

        reconsider x = p1, y = p2 as Element of (n -tuples_on D) qua non empty set;

        ex x9,y9 be Element of (n -tuples_on D) st x = x9 & y = y9 & (G . (x,y)) = (F .: (x9,y9)) by A2;

        hence thesis;

      end;

      uniqueness

      proof

        let G,H be BinOp of (n -tuples_on D);

        assume that

         A3: for x,y be Element of (n -tuples_on D) holds (G . (x,y)) = (F .: (x,y)) and

         A4: for x,y be Element of (n -tuples_on D) holds (H . (x,y)) = (F .: (x,y));

        now

          let x,y be Element of (n -tuples_on D);

          (G . (x,y)) = (F .: (x,y)) by A3;

          hence (G . (x,y)) = (H . (x,y)) by A4;

        end;

        hence G = H;

      end;

    end

    definition

      let D;

      let F be UnOp of D;

      let n;

      :: PRVECT_1:def2

      func product (F,n) -> UnOp of (n -tuples_on D) means

      : Def2: for x be Element of (n -tuples_on D) holds (it . x) = (F * x);

      existence

      proof

        defpred P[ set, set] means ex x9 be Element of (n -tuples_on D) st x9 = $1 & $2 = (F * x9);

        

         A1: for x be Element of (n -tuples_on D) qua non empty set holds ex y be Element of (n -tuples_on D) qua non empty set st P[x, y]

        proof

          let x be Element of (n -tuples_on D) qua non empty set;

          reconsider x9 = x as Element of (n -tuples_on D);

          reconsider y = (F * x9) as Element of (n -tuples_on D) qua non empty set by FINSEQ_2: 113;

          take y, x9;

          thus thesis;

        end;

        consider G be UnOp of (n -tuples_on D) such that

         A2: for x be Element of (n -tuples_on D) qua non empty set holds P[x, (G . x)] from FUNCT_2:sch 3( A1);

        take G;

        let p1 be Element of (n -tuples_on D);

        reconsider x = p1 as Element of (n -tuples_on D) qua non empty set;

        ex x9 be Element of (n -tuples_on D) st x9 = x & (G . x) = (F * x9) by A2;

        hence thesis;

      end;

      uniqueness

      proof

        let G,H be UnOp of (n -tuples_on D);

        assume that

         A3: for x be Element of (n -tuples_on D) holds (G . x) = (F * x) and

         A4: for x be Element of (n -tuples_on D) holds (H . x) = (F * x);

        now

          let x be Element of (n -tuples_on D);

          (G . x) = (F * x) by A3;

          hence (G . x) = (H . x) by A4;

        end;

        hence thesis by FUNCT_2: 63;

      end;

    end

    theorem :: PRVECT_1:6

    

     Th6: B is commutative implies ( product (B,n)) is commutative

    proof

      assume

       A1: B is commutative;

      now

        let x,y be Element of (n -tuples_on D);

        

        thus (( product (B,n)) . (x,y)) = (B .: (x,y)) by Def1

        .= (B .: (y,x)) by A1, FINSEQOP: 33

        .= (( product (B,n)) . (y,x)) by Def1;

      end;

      hence thesis;

    end;

    theorem :: PRVECT_1:7

    

     Th7: B is associative implies ( product (B,n)) is associative

    proof

      assume

       A1: B is associative;

      now

        let x,y,z be Element of (n -tuples_on D);

        

        thus (( product (B,n)) . ((( product (B,n)) . (x,y)),z)) = (( product (B,n)) . ((B .: (x,y)),z)) by Def1

        .= (B .: ((B .: (x,y)),z)) by Def1

        .= (B .: (x,(B .: (y,z)))) by A1, FINSEQOP: 28

        .= (( product (B,n)) . (x,(B .: (y,z)))) by Def1

        .= (( product (B,n)) . (x,(( product (B,n)) . (y,z)))) by Def1;

      end;

      hence thesis;

    end;

    theorem :: PRVECT_1:8

    

     Th8: d is_a_unity_wrt B implies (n |-> d) is_a_unity_wrt ( product (B,n))

    proof

      assume d is_a_unity_wrt B;

      then

       A1: B is having_a_unity & d = ( the_unity_wrt B) by BINOP_1:def 8, SETWISEO:def 2;

      now

        let b be Element of (n -tuples_on D) qua non empty set;

        reconsider b9 = b as Element of (n -tuples_on D);

        

        thus (( product (B,n)) . ((n |-> d),b)) = (B .: ((n |-> d),b9)) by Def1

        .= b by A1, FINSEQOP: 56;

        

        thus (( product (B,n)) . (b,(n |-> d))) = (B .: (b9,(n |-> d))) by Def1

        .= b by A1, FINSEQOP: 56;

      end;

      hence thesis by BINOP_1: 3;

    end;

    theorem :: PRVECT_1:9

    

     Th9: B is having_a_unity & B is associative & C is_an_inverseOp_wrt B implies ( product (C,n)) is_an_inverseOp_wrt ( product (B,n))

    proof

      assume that

       A1: B is having_a_unity and

       A2: B is associative and

       A3: C is_an_inverseOp_wrt B;

      

       A4: B is having_an_inverseOp by A3;

      then

       A5: C = ( the_inverseOp_wrt B) by A1, A2, A3, FINSEQOP:def 3;

       A6:

      now

        let f be Element of (n -tuples_on D) qua non empty set;

        reconsider f9 = f as Element of (n -tuples_on D);

        reconsider cf = (C * f9) as Element of (n -tuples_on D) by FINSEQ_2: 113;

        

        thus (( product (B,n)) . (f,(( product (C,n)) . f))) = (( product (B,n)) . (f9,(C * f9))) by Def2

        .= (B .: (f9,cf)) by Def1

        .= (n |-> ( the_unity_wrt B)) by A1, A2, A4, A5, FINSEQOP: 73;

        

        thus (( product (B,n)) . ((( product (C,n)) . f),f)) = (( product (B,n)) . ((C * f9),f9)) by Def2

        .= (B .: (cf,f9)) by Def1

        .= (n |-> ( the_unity_wrt B)) by A1, A2, A4, A5, FINSEQOP: 73;

      end;

      ex d st d is_a_unity_wrt B by A1, SETWISEO:def 2;

      then ( the_unity_wrt B) is_a_unity_wrt B by BINOP_1:def 8;

      then (n |-> ( the_unity_wrt B)) is_a_unity_wrt ( product (B,n)) by Th8;

      then (n |-> ( the_unity_wrt B)) = ( the_unity_wrt ( product (B,n))) by BINOP_1:def 8;

      hence thesis by A6;

    end;

    begin

    definition

      let F be non empty addLoopStr, n;

      assume

       A1: F is Abelian add-associative right_zeroed right_complementable;

      :: PRVECT_1:def3

      func n -Group_over F -> strict AbGroup equals

      : Def3: addLoopStr (# (n -tuples_on the carrier of F), ( product (the addF of F,n)), (n |-> ( 0. F)) qua Element of (n -tuples_on the carrier of F) #);

      coherence

      proof

        set G = addLoopStr (# (n -tuples_on the carrier of F), ( product (the addF of F,n)), (n |-> ( 0. F)) qua Element of (n -tuples_on the carrier of F) #);

        reconsider G as non empty addLoopStr;

        the addF of F is commutative associative by A1, FVSUM_1: 1, FVSUM_1: 2;

        then

         A2: ( product (the addF of F,n)) is commutative associative by Th6, Th7;

        

         A3: ( 0. F) is_a_unity_wrt the addF of F by A1, Th1;

        

         A4: G is right_complementable

        proof

          set B = the addF of F;

          set C = ( comp F);

          let x be Element of G;

          reconsider y = (( product (( comp F),n)) . x) as Element of G by FUNCT_2: 5;

          take y;

          B is associative & B is having_a_unity by A1, A3, FVSUM_1: 2, SETWISEO:def 2;

          then ( product (C,n)) is_an_inverseOp_wrt ( product (B,n)) by A1, Lm1, Th9;

          then

           A5: (x + y) = ( the_unity_wrt ( product (B,n)));

          ( 0. G) is_a_unity_wrt the addF of G by A1, Th1, Th8;

          hence thesis by A5, BINOP_1:def 8;

        end;

        ( 0. G) = (n |-> ( 0. F)) & (n |-> ( 0. F)) qua Element of (n -tuples_on the carrier of F) is_a_unity_wrt ( product (the addF of F,n)) by A1, Th1, Th8;

        hence thesis by A2, A4, Lm2, Lm3;

      end;

    end

    registration

      let F be AbGroup, n;

      cluster (n -Group_over F) -> non empty;

      coherence ;

    end

    reserve x,y for set;

    definition

      let F, n;

      :: PRVECT_1:def4

      func n -Mult_over F -> Function of [:the carrier of F, (n -tuples_on the carrier of F):], (n -tuples_on the carrier of F) means

      : Def4: for x be Element of F, v be Element of (n -tuples_on the carrier of F) holds (it . (x,v)) = (the multF of F [;] (x,v));

      existence

      proof

        defpred P[ object, object] means (ex x1 be Element of F, v be Element of (n -tuples_on the carrier of F) st $1 = [x1, v] & $2 = (the multF of F [;] (x1,v)));

        

         A1: for x be object st x in [:the carrier of F, (n -tuples_on the carrier of F):] holds ex y be object st y in (n -tuples_on the carrier of F) & P[x, y]

        proof

          let x be object;

          assume x in [:the carrier of F, (n -tuples_on the carrier of F):];

          then

          consider x1,v be object such that

           A2: x1 in the carrier of F and

           A3: v in (n -tuples_on the carrier of F) and

           A4: [x1, v] = x by ZFMISC_1: 84;

          reconsider v as Element of (n -tuples_on the carrier of F) by A3;

          reconsider x1 as Element of F by A2;

          take y = (the multF of F [;] (x1,v));

          y is Element of (n -tuples_on the carrier of F) by FINSEQ_2: 121;

          hence y in (n -tuples_on the carrier of F);

          take x1, v;

          thus thesis by A4;

        end;

        consider f be Function of [:the carrier of F, (n -tuples_on the carrier of F):], (n -tuples_on the carrier of F) such that

         A5: for x be object st x in [:the carrier of F, (n -tuples_on the carrier of F):] holds P[x, (f . x)] from FUNCT_2:sch 1( A1);

        take f;

        let x be Element of F, v be Element of (n -tuples_on the carrier of F);

         [x, v] in [:the carrier of F, (n -tuples_on the carrier of F):] by ZFMISC_1: 87;

        then

        consider x1 be Element of F, v1 be Element of (n -tuples_on the carrier of F) such that

         A6: [x, v] = [x1, v1] and

         A7: (f . [x, v]) = (the multF of F [;] (x1,v1)) by A5;

        x1 = x by A6, XTUPLE_0: 1;

        hence thesis by A6, A7, XTUPLE_0: 1;

      end;

      uniqueness

      proof

        let f,g be Function of [:the carrier of F, (n -tuples_on the carrier of F):], (n -tuples_on the carrier of F);

        assume that

         A8: for x be Element of F, v be Element of (n -tuples_on the carrier of F) holds (f . (x,v)) = (the multF of F [;] (x,v)) and

         A9: for x be Element of F, v be Element of (n -tuples_on the carrier of F) holds (g . (x,v)) = (the multF of F [;] (x,v));

        now

          let x be Element of F, v be Element of (n -tuples_on the carrier of F);

          (f . (x,v)) = (the multF of F [;] (x,v)) by A8;

          hence (f . (x,v)) = (g . (x,v)) by A9;

        end;

        hence thesis;

      end;

    end

    definition

      let F, n;

      :: PRVECT_1:def5

      func n -VectSp_over F -> strict ModuleStr over F means

      : Def5: the addLoopStr of it = (n -Group_over F) & the lmult of it = (n -Mult_over F);

      existence

      proof

        (n -Group_over F) = addLoopStr (# (n -tuples_on the carrier of F), ( product (the addF of F,n)), (n |-> ( 0. F)) qua Element of (n -tuples_on the carrier of F) #) by Def3;

        then

        reconsider d = (n -Mult_over F) as Function of [:the carrier of F, the carrier of (n -Group_over F):], the carrier of (n -Group_over F);

        set G = (n -Group_over F);

        take ModuleStr (# car(G), ad(G), zr(G), d #);

        thus thesis;

      end;

      uniqueness ;

    end

    registration

      let F, n;

      cluster (n -VectSp_over F) -> non empty;

      coherence

      proof

         the addLoopStr of (n -VectSp_over F) = (n -Group_over F) by Def5;

        hence the carrier of (n -VectSp_over F) is non empty;

      end;

    end

    reserve D for non empty set,

H,G for BinOp of D,

d for Element of D,

t1,t2 for Element of (n -tuples_on D);

    theorem :: PRVECT_1:10

    

     Th10: H is_distributive_wrt G implies (H [;] (d,(G .: (t1,t2)))) = (G .: ((H [;] (d,t1)),(H [;] (d,t2))))

    proof

      ( rng (H * <:(( dom t1) --> d), t1:>)) c= ( rng H) & ( rng (H * <:(( dom t2) --> d), t2:>)) c= ( rng H) by RELAT_1: 26;

      then ( rng <:(H * <:(( dom t1) --> d), t1:>), (H * <:(( dom t2) --> d), t2:>):>) c= [:( rng (H * <:(( dom t1) --> d), t1:>)), ( rng (H * <:(( dom t2) --> d), t2:>)):] & [:( rng (H * <:(( dom t1) --> d), t1:>)), ( rng (H * <:(( dom t2) --> d), t2:>)):] c= [:( rng H), ( rng H):] by FUNCT_3: 51, ZFMISC_1: 96;

      then

       A1: ( rng <:(H * <:(( dom t1) --> d), t1:>), (H * <:(( dom t2) --> d), t2:>):>) c= [:( rng H), ( rng H):] by XBOOLE_1: 1;

      ( rng H) c= D by RELAT_1:def 19;

      then [:( rng H), ( rng H):] c= [:D, D:] by ZFMISC_1: 96;

      then ( rng <:(H * <:(( dom t1) --> d), t1:>), (H * <:(( dom t2) --> d), t2:>):>) c= [:D, D:] by A1, XBOOLE_1: 1;

      then

       A2: ( rng <:(H * <:(( dom t1) --> d), t1:>), (H * <:(( dom t2) --> d), t2:>):>) c= ( dom G) by FUNCT_2:def 1;

      

       A3: ( dom t2) = ( Seg ( len t2)) by FINSEQ_1:def 3

      .= ( Seg n) by CARD_1:def 7;

      ( rng t1) c= D & ( rng t2) c= D by FINSEQ_1:def 4;

      then

       A4: [:( rng t1), ( rng t2):] c= [:D, D:] by ZFMISC_1: 96;

      ( rng <:t1, t2:>) c= [:( rng t1), ( rng t2):] by FUNCT_3: 51;

      then ( rng <:t1, t2:>) c= [:D, D:] by A4, XBOOLE_1: 1;

      then

       A5: ( rng <:t1, t2:>) c= ( dom G) by FUNCT_2:def 1;

      

       A6: ( dom (( dom t2) --> d)) = ( dom t2) by FUNCOP_1: 13

      .= ( Seg ( len t2)) by FINSEQ_1:def 3

      .= ( Seg n) by CARD_1:def 7;

      ( dom t1) = ( Seg ( len t1)) by FINSEQ_1:def 3

      .= ( Seg n) by CARD_1:def 7;

      then ( dom <:t1, t2:>) = ( Seg n) by A3, FUNCT_3: 50;

      then

       A7: ( dom (G * <:t1, t2:>)) = ( Seg n) by A5, RELAT_1: 27;

      then ( dom (( dom (G * <:t1, t2:>)) --> d)) = ( Seg n) by FUNCOP_1: 13;

      then

       A8: ( dom <:(( dom (G * <:t1, t2:>)) --> d), (G * <:t1, t2:>):>) = ( Seg n) by A7, FUNCT_3: 50;

      ( rng t2) c= D by FINSEQ_1:def 4;

      then ( rng <:(( dom t2) --> d), t2:>) c= [:( rng (( dom t2) --> d)), ( rng t2):] & [:( rng (( dom t2) --> d)), ( rng t2):] c= [:( rng (( dom t2) --> d)), D:] by FUNCT_3: 51, ZFMISC_1: 96;

      then

       A9: ( rng <:(( dom t2) --> d), t2:>) c= [:( rng (( dom t2) --> d)), D:] by XBOOLE_1: 1;

      ( rng (( dom t2) --> d)) c= {d} by FUNCOP_1: 13;

      then [:( rng (( dom t2) --> d)), D:] c= [: {d}, D:] by ZFMISC_1: 96;

      then

       A10: ( rng <:(( dom t2) --> d), t2:>) c= [: {d}, D:] by A9, XBOOLE_1: 1;

      

       A11: ( dom t1) = ( Seg ( len t1)) by FINSEQ_1:def 3

      .= ( Seg n) by CARD_1:def 7;

      ( rng t1) c= D by FINSEQ_1:def 4;

      then ( rng <:(( dom t1) --> d), t1:>) c= [:( rng (( dom t1) --> d)), ( rng t1):] & [:( rng (( dom t1) --> d)), ( rng t1):] c= [:( rng (( dom t1) --> d)), D:] by FUNCT_3: 51, ZFMISC_1: 96;

      then

       A12: ( rng <:(( dom t1) --> d), t1:>) c= [:( rng (( dom t1) --> d)), D:] by XBOOLE_1: 1;

      ( rng (( dom t1) --> d)) c= {d} by FUNCOP_1: 13;

      then [:( rng (( dom t1) --> d)), D:] c= [: {d}, D:] by ZFMISC_1: 96;

      then

       A13: ( rng <:(( dom t1) --> d), t1:>) c= [: {d}, D:] by A12, XBOOLE_1: 1;

      

       A14: ( dom (( dom t1) --> d)) = ( dom t1) by FUNCOP_1: 13

      .= ( Seg ( len t1)) by FINSEQ_1:def 3

      .= ( Seg n) by CARD_1:def 7;

       {d} c= D by ZFMISC_1: 31;

      then

       A15: [: {d}, D:] c= [:D, D:] by ZFMISC_1: 96;

      ( rng (( dom (G * <:t1, t2:>)) --> d)) c= {d} & {d} c= D by FUNCOP_1: 13, ZFMISC_1: 31;

      then

       A16: ( rng (( dom (G * <:t1, t2:>)) --> d)) c= D by XBOOLE_1: 1;

      

       A17: ( dom t2) = ( Seg ( len t2)) by FINSEQ_1:def 3

      .= ( Seg n) by CARD_1:def 7;

      ( dom H) = [:D, D:] by FUNCT_2:def 1;

      

      then

       A18: ( dom (H * <:(( dom t2) --> d), t2:>)) = ( dom <:(( dom t2) --> d), t2:>) by A10, A15, RELAT_1: 27, XBOOLE_1: 1

      .= ( Seg n) by A6, A17, FUNCT_3: 50;

       {d} c= D by ZFMISC_1: 31;

      then

       A19: [: {d}, D:] c= [:D, D:] by ZFMISC_1: 96;

      set A = (H * <:(( dom (G * <:t1, t2:>)) --> d), (G * <:t1, t2:>):>);

      ( dom H) = [:D, D:] by FUNCT_2:def 1;

      

      then ( dom (H * <:(( dom t1) --> d), t1:>)) = ( dom <:(( dom t1) --> d), t1:>) by A13, A19, RELAT_1: 27, XBOOLE_1: 1

      .= ( Seg n) by A14, A11, FUNCT_3: 50;

      then ( dom <:(H * <:(( dom t1) --> d), t1:>), (H * <:(( dom t2) --> d), t2:>):>) = ( Seg n) by A18, FUNCT_3: 50;

      then

       A20: ( dom (G * <:(H * <:(( dom t1) --> d), t1:>), (H * <:(( dom t2) --> d), t2:>):>)) = ( Seg n) by A2, RELAT_1: 27;

      ( rng (G * <:t1, t2:>)) c= D by RELAT_1:def 19;

      then ( rng <:(( dom (G * <:t1, t2:>)) --> d), (G * <:t1, t2:>):>) c= [:( rng (( dom (G * <:t1, t2:>)) --> d)), ( rng (G * <:t1, t2:>)):] & [:( rng (( dom (G * <:t1, t2:>)) --> d)), ( rng (G * <:t1, t2:>)):] c= [:D, D:] by A16, FUNCT_3: 51, ZFMISC_1: 96;

      then ( rng <:(( dom (G * <:t1, t2:>)) --> d), (G * <:t1, t2:>):>) c= [:D, D:] by XBOOLE_1: 1;

      then

       A21: ( rng <:(( dom (G * <:t1, t2:>)) --> d), (G * <:t1, t2:>):>) c= ( dom H) by FUNCT_2:def 1;

      then

       A22: ( dom A) = ( Seg n) by A8, RELAT_1: 27;

      assume

       A23: H is_distributive_wrt G;

      for x be object st x in ( dom A) holds ((H [;] (d,(G .: (t1,t2)))) . x) = ((G .: ((H [;] (d,t1)),(H [;] (d,t2)))) . x)

      proof

        ( rng t1) c= D by FINSEQ_1:def 4;

        then ( rng <:(( dom t1) --> d), t1:>) c= [:( rng (( dom t1) --> d)), ( rng t1):] & [:( rng (( dom t1) --> d)), ( rng t1):] c= [:( rng (( dom t1) --> d)), D:] by FUNCT_3: 51, ZFMISC_1: 96;

        then

         A24: ( rng <:(( dom t1) --> d), t1:>) c= [:( rng (( dom t1) --> d)), D:] by XBOOLE_1: 1;

        ( rng (( dom t1) --> d)) c= {d} by FUNCOP_1: 13;

        then [:( rng (( dom t1) --> d)), D:] c= [: {d}, D:] by ZFMISC_1: 96;

        then

         A25: ( rng <:(( dom t1) --> d), t1:>) c= [: {d}, D:] by A24, XBOOLE_1: 1;

        

         A26: ( rng t1) c= D & ( rng t2) c= D by FINSEQ_1:def 4;

         {d} c= D by ZFMISC_1: 31;

        then

         A27: [: {d}, D:] c= [:D, D:] by ZFMISC_1: 96;

        

         A28: ( dom (( dom t2) --> d)) = ( dom t2) by FUNCOP_1: 13

        .= ( Seg ( len t2)) by FINSEQ_1:def 3

        .= ( Seg n) by CARD_1:def 7;

         {d} c= D by ZFMISC_1: 31;

        then

         A29: [: {d}, D:] c= [:D, D:] by ZFMISC_1: 96;

        

         A30: ( dom t1) = ( Seg ( len t1)) by FINSEQ_1:def 3

        .= ( Seg n) by CARD_1:def 7;

        ( rng t2) c= D by FINSEQ_1:def 4;

        then ( rng <:(( dom t2) --> d), t2:>) c= [:( rng (( dom t2) --> d)), ( rng t2):] & [:( rng (( dom t2) --> d)), ( rng t2):] c= [:( rng (( dom t2) --> d)), D:] by FUNCT_3: 51, ZFMISC_1: 96;

        then

         A31: ( rng <:(( dom t2) --> d), t2:>) c= [:( rng (( dom t2) --> d)), D:] by XBOOLE_1: 1;

        ( rng (( dom t2) --> d)) c= {d} by FUNCOP_1: 13;

        then [:( rng (( dom t2) --> d)), D:] c= [: {d}, D:] by ZFMISC_1: 96;

        then

         A32: ( rng <:(( dom t2) --> d), t2:>) c= [: {d}, D:] by A31, XBOOLE_1: 1;

        

         A33: ( dom (( dom t1) --> d)) = ( dom t1) by FUNCOP_1: 13

        .= ( Seg ( len t1)) by FINSEQ_1:def 3

        .= ( Seg n) by CARD_1:def 7;

        let x be object;

        

         A34: ( dom <:(( dom (G .: (t1,t2))) --> d), (G .: (t1,t2)):>) = (( dom (( dom (G .: (t1,t2))) --> d)) /\ ( dom (G .: (t1,t2)))) by FUNCT_3:def 7;

        assume

         A35: x in ( dom A);

        then x in ( dom <:(( dom (G .: (t1,t2))) --> d), (G .: (t1,t2)):>) by FUNCT_1: 11;

        then

         A36: x in ( dom (G .: (t1,t2))) by A34, XBOOLE_0:def 4;

        ( dom t1) = ( Seg ( len t1)) by FINSEQ_1:def 3

        .= ( Seg n) by CARD_1:def 7;

        then

         A37: (t1 . x) in ( rng t1) by A22, A35, FUNCT_1:def 3;

        

         A38: ( dom t2) = ( Seg ( len t2)) by FINSEQ_1:def 3

        .= ( Seg n) by CARD_1:def 7;

        ( dom H) = [:D, D:] by FUNCT_2:def 1;

        

        then ( dom (H * <:(( dom t1) --> d), t1:>)) = ( dom <:(( dom t1) --> d), t1:>) by A25, A29, RELAT_1: 27, XBOOLE_1: 1

        .= ( Seg n) by A33, A30, FUNCT_3: 50;

        then

         A39: x in ( dom (H [;] (d,t1))) by A22, A35;

        ( dom t2) = ( Seg ( len t2)) by FINSEQ_1:def 3

        .= ( Seg n) by CARD_1:def 7;

        then

         A40: (t2 . x) in ( rng t2) by A22, A35, FUNCT_1:def 3;

        ( dom H) = [:D, D:] by FUNCT_2:def 1;

        

        then ( dom (H * <:(( dom t2) --> d), t2:>)) = ( dom <:(( dom t2) --> d), t2:>) by A32, A27, RELAT_1: 27, XBOOLE_1: 1

        .= ( Seg n) by A28, A38, FUNCT_3: 50;

        then

         A41: x in ( dom (H [;] (d,t2))) by A22, A35;

        ((H [;] (d,(G .: (t1,t2)))) . x) = (H . (d,((G .: (t1,t2)) . x))) by A35, FUNCOP_1: 32

        .= (H . (d,(G . ((t1 . x),(t2 . x))))) by A36, FUNCOP_1: 22

        .= (G . ((H . (d,(t1 . x))),(H . (d,(t2 . x))))) by A23, A37, A26, A40, BINOP_1: 11

        .= (G . (((H [;] (d,t1)) . x),(H . (d,(t2 . x))))) by A39, FUNCOP_1: 32

        .= (G . (((H [;] (d,t1)) . x),((H [;] (d,t2)) . x))) by A41, FUNCOP_1: 32

        .= ((G .: ((H [;] (d,t1)),(H [;] (d,t2)))) . x) by A22, A20, A35, FUNCOP_1: 22;

        hence thesis;

      end;

      hence thesis by A8, A21, A20, RELAT_1: 27;

    end;

    definition

      let D be non empty set, n be Nat, F be BinOp of D, x be Element of D, v be Element of (n -tuples_on D);

      :: original: [;]

      redefine

      func F [;] (x,v) -> Element of (n -tuples_on D) ;

      coherence by FINSEQ_2: 121;

    end

    registration

      let F, n;

      cluster (n -VectSp_over F) -> vector-distributive scalar-distributive scalar-associative scalar-unital;

      coherence

      proof

        

         A1: the addLoopStr of (n -VectSp_over F) = (n -Group_over F) & (n -Group_over F) = addLoopStr (# (n -tuples_on the carrier of F), ( product (the addF of F,n)), (n |-> ( 0. F)) qua Element of (n -tuples_on the carrier of F) #) by Def3, Def5;

        ( 1_ F) is_a_unity_wrt the multF of F by Th5;

        then

         A2: the multF of F is having_a_unity & ( the_unity_wrt the multF of F) = ( 1_ F) by BINOP_1:def 8, SETWISEO:def 2;

        

         A3: (n -VectSp_over F) is vector-distributive

        proof

          let x be Element of F;

          let v,w be Element of (n -VectSp_over F);

          reconsider v9 = v, w9 = w as Element of (n -tuples_on the carrier of F) by A1;

          

          thus (x * (v + w)) = ((n -Mult_over F) . (x,(( product (the addF of F,n)) . (v,w)))) by A1, Def5

          .= ((n -Mult_over F) . (x,(the addF of F .: (v9,w9)))) by Def1

          .= (the multF of F [;] (x,(the addF of F .: (v9,w9)))) by Def4

          .= (the addF of F .: ((the multF of F [;] (x,v9)),(the multF of F [;] (x,w9)))) by Lm5, Th10

          .= (( product (the addF of F,n)) . ((the multF of F [;] (x,v9)),(the multF of F [;] (x,w9)))) by Def1

          .= (( product (the addF of F,n)) . (((n -Mult_over F) . (x,v9)),(the multF of F [;] (x,w9)))) by Def4

          .= (( product (the addF of F,n)) . (((n -Mult_over F) . (x,v9)),((n -Mult_over F) . (x,w9)))) by Def4

          .= (( product (the addF of F,n)) . ((the lmult of (n -VectSp_over F) . (x,v)),((n -Mult_over F) . (x,w9)))) by Def5

          .= ((x * v) + (x * w)) by A1, Def5;

        end;

        

         A4: (n -VectSp_over F) is scalar-distributive

        proof

          let x,y be Element of F;

          let v be Element of (n -VectSp_over F);

          reconsider v9 = v as Element of (n -tuples_on the carrier of F) by A1;

          

          thus ((x + y) * v) = ((n -Mult_over F) . ((x + y),v9)) by Def5

          .= (the multF of F [;] ((the addF of F . (x,y)),v9)) by Def4

          .= (the addF of F .: ((the multF of F [;] (x,v9)),(the multF of F [;] (y,v9)))) by Lm5, FINSEQOP: 46

          .= (( product (the addF of F,n)) . ((the multF of F [;] (x,v9)),(the multF of F [;] (y,v9)))) by Def1

          .= (( product (the addF of F,n)) . (((n -Mult_over F) . (x,v9)),(the multF of F [;] (y,v9)))) by Def4

          .= (( product (the addF of F,n)) . (((n -Mult_over F) . (x,v9)),((n -Mult_over F) . (y,v9)))) by Def4

          .= (( product (the addF of F,n)) . ((the lmult of (n -VectSp_over F) . (x,v)),((n -Mult_over F) . (y,v9)))) by Def5

          .= ((x * v) + (y * v)) by A1, Def5;

        end;

        

         A5: (n -VectSp_over F) is scalar-associative

        proof

          let x,y be Element of F;

          let v be Element of (n -VectSp_over F);

          reconsider v9 = v as Element of (n -tuples_on the carrier of F) by A1;

          

          thus ((x * y) * v) = ((n -Mult_over F) . ((x * y),v9)) by Def5

          .= (the multF of F [;] ((x * y),v9)) by Def4

          .= (the multF of F [;] (x,(the multF of F [;] (y,v9)))) by Lm4, FINSEQOP: 31

          .= ((n -Mult_over F) . (x,(the multF of F [;] (y,v9)))) by Def4

          .= ((n -Mult_over F) . (x,((n -Mult_over F) . (y,v9)))) by Def4

          .= ((n -Mult_over F) . (x,(the lmult of (n -VectSp_over F) . (y,v)))) by Def5

          .= (x * (y * v)) by Def5;

        end;

        (n -VectSp_over F) is scalar-unital

        proof

          let v be Element of (n -VectSp_over F);

          reconsider v9 = v as Element of (n -tuples_on the carrier of F) by A1;

          

          thus (( 1. F) * v) = ((n -Mult_over F) . (( 1. F),v9)) by Def5

          .= (the multF of F [;] (( 1. F),v9)) by Def4

          .= v by A2, FINSEQOP: 57;

        end;

        hence thesis by A3, A4, A5;

      end;

    end

    begin

    reserve x,y,z for set,

A for AbGroup;

    definition

      mode Domain-Sequence is non empty non-empty FinSequence;

    end

    scheme :: PRVECT_1:sch1

    NEFinSeqLambda { w() -> non empty FinSequence , F( set) -> set } :

ex p be non empty FinSequence st ( len p) = ( len w()) & for i be Element of ( dom w()) holds (p . i) = F(i);

      consider p be FinSequence such that

       A1: ( len p) = ( len w()) & for i be Nat st i in ( dom p) holds (p . i) = F(i) from FINSEQ_1:sch 2;

      reconsider p9 = p as non empty FinSequence by A1;

      take p9;

      thus ( len p9) = ( len w()) by A1;

      let i be Element of ( dom w());

      

       A2: ( dom w()) = ( Seg ( len w())) by FINSEQ_1:def 3;

      ( dom p) = ( Seg ( len w())) by A1, FINSEQ_1:def 3;

      hence thesis by A1, A2;

    end;

    definition

      let a be non-empty non empty Function;

      let f be Element of ( product a);

      let i be Element of ( dom a);

      :: original: .

      redefine

      func f . i -> Element of (a . i) ;

      coherence by CARD_3: 9;

    end

    begin

    reserve a for Domain-Sequence,

i for Element of ( dom a),

p for FinSequence;

    definition

      let a be non-empty non empty Function;

      :: PRVECT_1:def6

      mode BinOps of a -> Function means

      : Def6: ( dom it ) = ( dom a) & for i be Element of ( dom a) holds (it . i) is BinOp of (a . i);

      existence

      proof

        deffunc F( object) = ( pr1 ((a . $1),(a . $1)));

        consider f be Function such that

         A1: ( dom f) = ( dom a) & for x be object st x in ( dom a) holds (f . x) = F(x) from FUNCT_1:sch 3;

        take f;

        thus ( dom f) = ( dom a) by A1;

        let i be Element of ( dom a);

        (f . i) = ( pr1 ((a . i),(a . i))) by A1;

        hence thesis;

      end;

      :: PRVECT_1:def7

      mode UnOps of a -> Function means

      : Def7: ( dom it ) = ( dom a) & for i be Element of ( dom a) holds (it . i) is UnOp of (a . i);

      existence

      proof

        deffunc F( object) = ( id (a . $1));

        consider f be Function such that

         A2: ( dom f) = ( dom a) & for x be object st x in ( dom a) holds (f . x) = F(x) from FUNCT_1:sch 3;

        take f;

        thus ( dom f) = ( dom a) by A2;

        let i be Element of ( dom a);

        (f . i) = ( id (a . i)) by A2;

        hence thesis;

      end;

    end

    registration

      let a;

      cluster -> FinSequence-like for BinOps of a;

      coherence

      proof

        let f be BinOps of a;

        ( dom a) = ( dom f) & ( dom a) = ( Seg ( len a)) by Def6, FINSEQ_1:def 3;

        hence thesis by FINSEQ_1:def 2;

      end;

      cluster -> FinSequence-like for UnOps of a;

      coherence

      proof

        let f be UnOps of a;

        ( dom a) = ( dom f) & ( dom a) = ( Seg ( len a)) by Def7, FINSEQ_1:def 3;

        hence thesis by FINSEQ_1:def 2;

      end;

    end

    registration

      let a;

      cluster -> Function-yielding for BinOps of a;

      coherence

      proof

        let b be BinOps of a;

        let x be object;

        assume x in ( dom b);

        then

        reconsider xx = x as Element of ( dom a) by Def6;

        (b . xx) is BinOp of (a . xx) by Def6;

        hence (b . x) is Function;

      end;

      cluster -> Function-yielding for UnOps of a;

      coherence

      proof

        let b be UnOps of a;

        let x be object;

        assume x in ( dom b);

        then

        reconsider xx = x as Element of ( dom a) by Def7;

        (b . xx) is UnOp of (a . xx) by Def7;

        hence (b . x) is Function;

      end;

    end

    theorem :: PRVECT_1:11

    

     Th11: p is BinOps of a iff ( len p) = ( len a) & for i holds (p . i) is BinOp of (a . i)

    proof

      ( dom p) = ( dom a) iff ( len p) = ( len a) by FINSEQ_3: 29;

      hence thesis by Def6;

    end;

    theorem :: PRVECT_1:12

    

     Th12: p is UnOps of a iff ( len p) = ( len a) & for i holds (p . i) is UnOp of (a . i)

    proof

      ( dom p) = ( dom a) iff ( len p) = ( len a) by FINSEQ_3: 29;

      hence thesis by Def7;

    end;

    definition

      let a;

      let b be BinOps of a;

      let i;

      :: original: .

      redefine

      func b . i -> BinOp of (a . i) ;

      coherence by Th11;

    end

    definition

      let a;

      let u be UnOps of a;

      let i;

      :: original: .

      redefine

      func u . i -> UnOp of (a . i) ;

      coherence by Th12;

    end

    theorem :: PRVECT_1:13

    for d,d9 be UnOp of ( product a) st for f be Element of ( product a), i be Element of ( dom a) holds ((d . f) . i) = ((d9 . f) . i) holds d = d9

    proof

      let d,d9 be UnOp of ( product a) such that

       A1: for f be Element of ( product a), i be Element of ( dom a) holds ((d . f) . i) = ((d9 . f) . i);

      now

        let f be Element of ( product a);

        ( dom (d . f)) = ( dom a) & ( dom (d9 . f)) = ( dom a) by CARD_3: 9;

        hence (d . f) = (d9 . f) by A1;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: PRVECT_1:14

    

     Th14: for u be UnOps of a holds ( doms u) = a & ( product ( rngs u)) c= ( product a)

    proof

      let u be UnOps of a;

      

       A2: ( dom a) = ( Seg ( len a)) & ( dom u) = ( Seg ( len u)) by FINSEQ_1:def 3;

      

       A3: ( len u) = ( len a) by Th12;

      

       A4: ( dom ( doms u)) = ( dom u) by FUNCT_6:def 2;

       A5:

      now

        let x be object;

        assume x in ( dom u);

        then

        reconsider i = x as Element of ( dom a) by A2, Th12;

        (( rngs u) . i) = ( rng (u . i)) by A2, A3, FUNCT_6: 22;

        hence (( rngs u) . x) c= (a . x) by RELAT_1:def 19;

      end;

      now

        let x be object;

        assume x in ( dom u);

        then

        reconsider i = x as Element of ( dom a) by A2, Th12;

        (( doms u) . i) = ( dom (u . i)) by A2, A3, FUNCT_6: 22

        .= (a . i) by FUNCT_2:def 1;

        hence (( doms u) . x) = (a . x);

      end;

      hence ( doms u) = a by A2, Th12, A4;

      ( dom ( rngs u)) = ( dom u) by FUNCT_6:def 3;

      hence thesis by A2, A3, A5, CARD_3: 27;

    end;

    definition

      let a;

      let u be UnOps of a;

      :: original: Frege

      redefine

      func Frege u -> UnOp of ( product a) ;

      coherence

      proof

        

         A1: ( product ( rngs u)) c= ( product a) & ( rng ( Frege u)) = ( product ( rngs u)) by Th14, FUNCT_6: 38;

        ( dom ( Frege u)) = ( product ( doms u)) & ( doms u) = a by Th14, FUNCT_6:def 7;

        hence thesis by A1, FUNCT_2:def 1, RELSET_1: 4;

      end;

    end

    theorem :: PRVECT_1:15

    

     Th15: for u be UnOps of a holds for f be Element of ( product a), i be Element of ( dom a) holds ((( Frege u) . f) . i) = ((u . i) . (f . i))

    proof

      let u be UnOps of a, f be Element of ( product a);

      let i be Element of ( dom a);

      

       A1: ( dom u) = ( Seg ( len u)) & ( doms u) = a by Th14, FINSEQ_1:def 3;

      ( dom a) = ( Seg ( len a)) & ( len a) = ( len u) by Th12, FINSEQ_1:def 3;

      hence thesis by A1, FUNCT_6: 37;

    end;

    theorem :: PRVECT_1:16

    

     Th16: for d,d9 be BinOp of ( product a) st for f,g be Element of ( product a), i be Element of ( dom a) holds ((d . (f,g)) . i) = ((d9 . (f,g)) . i) holds d = d9

    proof

      let d,d9 be BinOp of ( product a) such that

       A1: for f,g be Element of ( product a), i be Element of ( dom a) holds ((d . (f,g)) . i) = ((d9 . (f,g)) . i);

      now

        let f,g be Element of ( product a);

        ( dom (d . (f,g))) = ( dom a) & ( dom (d9 . (f,g))) = ( dom a) by CARD_3: 9;

        hence (d . (f,g)) = (d9 . (f,g)) by A1;

      end;

      hence thesis;

    end;

    reserve i for Element of ( dom a);

    definition

      let a;

      let b be BinOps of a;

      :: PRVECT_1:def8

      func [:b:] -> BinOp of ( product a) means

      : Def8: for f,g be Element of ( product a), i be Element of ( dom a) holds ((it . (f,g)) . i) = ((b . i) . ((f . i),(g . i)));

      existence

      proof

        defpred Q[ Element of ( product a), Element of ( product a), Element of ( product a)] means for i be Element of ( dom a) holds ($3 . i) = ((b . i) . (($1 . i),($2 . i)));

        

         A1: for f,g be Element of ( product a) holds ex z be Element of ( product a) st Q[f, g, z]

        proof

          let f,g be Element of ( product a);

          defpred P[ object, object] means ex i st $1 = i & $2 = ((b . i) . ((f . i),(g . i)));

          

           A2: for x be object st x in ( dom a) holds ex z be object st P[x, z]

          proof

            let x be object;

            assume x in ( dom a);

            then

            reconsider i = x as Element of ( dom a);

            take ((b . i) . ((f . i),(g . i)));

            thus thesis;

          end;

          consider z be Function such that

           A3: ( dom z) = ( dom a) & for x be object st x in ( dom a) holds P[x, (z . x)] from CLASSES1:sch 1( A2);

          now

            let x be object;

            assume x in ( dom a);

            then ex i st x = i & (z . x) = ((b . i) . ((f . i),(g . i))) by A3;

            hence (z . x) in (a . x);

          end;

          then

          reconsider z9 = z as Element of ( product a) by A3, CARD_3: 9;

          take z9;

          let i;

          ex j be Element of ( dom a) st j = i & (z . i) = ((b . j) . ((f . j),(g . j))) by A3;

          hence thesis;

        end;

        consider d be BinOp of ( product a) such that

         A4: for f,g be Element of ( product a) holds Q[f, g, (d . (f,g))] from BINOP_1:sch 3( A1);

        take d;

        thus thesis by A4;

      end;

      uniqueness

      proof

        let d,d9 be BinOp of ( product a) such that

         A5: for f,g be Element of ( product a), i be Element of ( dom a) holds ((d . (f,g)) . i) = ((b . i) . ((f . i),(g . i))) and

         A6: for f,g be Element of ( product a), i be Element of ( dom a) holds ((d9 . (f,g)) . i) = ((b . i) . ((f . i),(g . i)));

        now

          let f,g be Element of ( product a);

          let i be Element of ( dom a);

          

          thus ((d . (f,g)) . i) = ((b . i) . ((f . i),(g . i))) by A5

          .= ((d9 . (f,g)) . i) by A6;

        end;

        hence thesis by Th16;

      end;

    end

    theorem :: PRVECT_1:17

    

     Th17: for b be BinOps of a st for i holds (b . i) is commutative holds [:b:] is commutative

    proof

      let b be BinOps of a such that

       A1: for i holds (b . i) is commutative;

      let x,y be Element of ( product a);

       A2:

      now

        let z be object;

        assume z in ( dom a);

        then

        reconsider i = z as Element of ( dom a);

        

         A3: (( [:b:] . (y,x)) . i) = ((b . i) . ((y . i),(x . i))) by Def8;

        (b . i) is commutative & (( [:b:] . (x,y)) . i) = ((b . i) . ((x . i),(y . i))) by A1, Def8;

        hence (( [:b:] . (x,y)) . z) = (( [:b:] . (y,x)) . z) by A3;

      end;

      ( dom ( [:b:] . (x,y))) = ( dom a) & ( dom ( [:b:] . (y,x))) = ( dom a) by CARD_3: 9;

      hence thesis by A2, FUNCT_1: 2;

    end;

    theorem :: PRVECT_1:18

    

     Th18: for b be BinOps of a st for i holds (b . i) is associative holds [:b:] is associative

    proof

      let b be BinOps of a such that

       A1: for i holds (b . i) is associative;

      let x,y,z be Element of ( product a);

       A2:

      now

        set xy = ( [:b:] . (x,y)), yz = ( [:b:] . (y,z));

        let v be object;

        assume v in ( dom a);

        then

        reconsider i = v as Element of ( dom a);

        

         A3: (( [:b:] . (y,z)) . i) = ((b . i) . ((y . i),(z . i))) & (( [:b:] . (x,yz)) . i) = ((b . i) . ((x . i),(yz . i))) by Def8;

        

         A4: (( [:b:] . (xy,z)) . i) = ((b . i) . ((xy . i),(z . i))) by Def8;

        (b . i) is associative & (( [:b:] . (x,y)) . i) = ((b . i) . ((x . i),(y . i))) by A1, Def8;

        hence (( [:b:] . (x,( [:b:] . (y,z)))) . v) = (( [:b:] . (( [:b:] . (x,y)),z)) . v) by A3, A4;

      end;

      ( dom ( [:b:] . (x,( [:b:] . (y,z))))) = ( dom a) & ( dom ( [:b:] . (( [:b:] . (x,y)),z))) = ( dom a) by CARD_3: 9;

      hence thesis by A2, FUNCT_1: 2;

    end;

    theorem :: PRVECT_1:19

    

     Th19: for b be BinOps of a, f be Element of ( product a) st for i holds (f . i) is_a_unity_wrt (b . i) holds f is_a_unity_wrt [:b:]

    proof

      let b be BinOps of a, f be Element of ( product a) such that

       A1: for i holds (f . i) is_a_unity_wrt (b . i);

      now

        let x be Element of ( product a);

         A3:

        now

          let y be object;

          assume y in ( dom a);

          then

          reconsider i = y as Element of ( dom a);

          (( [:b:] . (f,x)) . i) = ((b . i) . ((f . i),(x . i))) & (f . i) is_a_unity_wrt (b . i) by A1, Def8;

          hence (( [:b:] . (f,x)) . y) = (x . y) by BINOP_1: 3;

        end;

        ( dom ( [:b:] . (f,x))) = ( dom a) by CARD_3: 9;

        hence ( [:b:] . (f,x)) = x by A3, CARD_3: 9;

         A4:

        now

          let y be object;

          assume y in ( dom a);

          then

          reconsider i = y as Element of ( dom a);

          (( [:b:] . (x,f)) . i) = ((b . i) . ((x . i),(f . i))) & (f . i) is_a_unity_wrt (b . i) by A1, Def8;

          hence (( [:b:] . (x,f)) . y) = (x . y) by BINOP_1: 3;

        end;

        ( dom ( [:b:] . (x,f))) = ( dom a) by CARD_3: 9;

        hence ( [:b:] . (x,f)) = x by A4, CARD_3: 9;

      end;

      hence thesis by BINOP_1: 3;

    end;

    theorem :: PRVECT_1:20

    

     Th20: for b be BinOps of a, u be UnOps of a st for i holds (u . i) is_an_inverseOp_wrt (b . i) & (b . i) is having_a_unity holds ( Frege u) is_an_inverseOp_wrt [:b:]

    proof

      let b be BinOps of a, u be UnOps of a such that

       A1: for i holds (u . i) is_an_inverseOp_wrt (b . i) & (b . i) is having_a_unity;

      defpred P[ object, object] means ex i st $1 = i & $2 = ( the_unity_wrt (b . i));

      

       A2: for x be object st x in ( dom a) holds ex y be object st P[x, y]

      proof

        let x be object;

        assume x in ( dom a);

        then

        reconsider i = x as Element of ( dom a);

        take ( the_unity_wrt (b . i));

        thus thesis;

      end;

      consider f be Function such that

       A3: ( dom f) = ( dom a) & for x be object st x in ( dom a) holds P[x, (f . x)] from CLASSES1:sch 1( A2);

      now

        let x be object;

        assume x in ( dom a);

        then ex i st x = i & (f . x) = ( the_unity_wrt (b . i)) by A3;

        hence (f . x) in (a . x);

      end;

      then

      reconsider f as Element of ( product a) by A3, CARD_3: 9;

      let x be Element of ( product a);

       A5:

      now

        let y be object;

        assume y in ( dom a);

        then

        reconsider i = y as Element of ( dom a);

        

         A6: ((( Frege u) . x) . i) = ((u . i) . (x . i)) & (u . i) is_an_inverseOp_wrt (b . i) by A1, Th15;

        (ex j be Element of ( dom a) st i = j & (f . i) = ( the_unity_wrt (b . j))) & (( [:b:] . (x,(( Frege u) . x))) . i) = ((b . i) . ((x . i),((( Frege u) . x) . i))) by A3, Def8;

        hence (( [:b:] . (x,(( Frege u) . x))) . y) = (f . y) by A6;

      end;

      now

        let i;

        (ex j be Element of ( dom a) st i = j & (f . i) = ( the_unity_wrt (b . j))) & (b . i) is having_a_unity by A1, A3;

        hence (f . i) is_a_unity_wrt (b . i) by SETWISEO: 14;

      end;

      then f is_a_unity_wrt [:b:] by Th19;

      then

       A7: f = ( the_unity_wrt [:b:]) by BINOP_1:def 8;

       A8:

      now

        let y be object;

        assume y in ( dom a);

        then

        reconsider i = y as Element of ( dom a);

        

         A9: ((( Frege u) . x) . i) = ((u . i) . (x . i)) & (u . i) is_an_inverseOp_wrt (b . i) by A1, Th15;

        (ex j be Element of ( dom a) st i = j & (f . i) = ( the_unity_wrt (b . j))) & (( [:b:] . ((( Frege u) . x),x)) . i) = ((b . i) . (((( Frege u) . x) . i),(x . i))) by A3, Def8;

        hence (( [:b:] . ((( Frege u) . x),x)) . y) = (f . y) by A9;

      end;

      ( dom ( [:b:] . (x,(( Frege u) . x)))) = ( dom a) by CARD_3: 9;

      hence ( [:b:] . (x,(( Frege u) . x))) = ( the_unity_wrt [:b:]) by A7, A5, CARD_3: 9;

      ( dom ( [:b:] . ((( Frege u) . x),x))) = ( dom a) by CARD_3: 9;

      hence ( [:b:] . ((( Frege u) . x),x)) = ( the_unity_wrt [:b:]) by A7, A8, CARD_3: 9;

    end;

    begin

    definition

      let F be Relation;

      :: PRVECT_1:def9

      attr F is non-empty-addLoopStr-yielding means

      : DefAA: x in ( rng F) implies x is non empty addLoopStr;

      :: PRVECT_1:def10

      attr F is AbGroup-yielding means

      : Def9: x in ( rng F) implies x is AbGroup;

    end

    registration

      cluster AbGroup-yielding -> non-empty-addLoopStr-yielding for Relation;

      coherence ;

    end

    registration

      cluster non-empty-addLoopStr-yielding -> non-Empty 1-sorted-yielding for Relation;

      coherence

      proof

        let R be Relation;

        assume

         A1: R is non-empty-addLoopStr-yielding;

        then

         a2: for x be object st x in ( rng R) holds x is 1-sorted;

        for S be 1-sorted st S in ( rng R) holds S is non empty by A1;

        hence thesis by a2, WAYBEL_3:def 7, PRALG_1:def 11;

      end;

    end

    registration

      cluster non empty AbGroup-yielding for FinSequence;

      existence

      proof

        set A = the AbGroup;

        take <*A*>;

        thus <*A*> is non empty;

        let x;

        assume that

         A1: x in ( rng <*A*>) and

         A2: not x is AbGroup;

        x in {A} by A1, FINSEQ_1: 38;

        hence contradiction by A2, TARSKI:def 1;

      end;

    end

    definition

      mode Group-Sequence is non empty AbGroup-yielding FinSequence;

    end

    definition

      let g be non empty non-empty-addLoopStr-yielding FinSequence;

      let i be Element of ( dom g);

      :: original: .

      redefine

      func g . i -> non empty addLoopStr ;

      coherence

      proof

        (g . i) in ( rng g) by FUNCT_1:def 3;

        hence thesis by DefAA;

      end;

    end

    definition

      let g be Group-Sequence;

      let i be Element of ( dom g);

      :: original: .

      redefine

      func g . i -> AbGroup ;

      coherence

      proof

        (g . i) in ( rng g) by FUNCT_1:def 3;

        hence thesis by Def9;

      end;

    end

    notation

      let g be non empty non-Empty 1-sorted-yielding FinSequence;

      synonym carr g for Carrier g;

    end

    registration

      let f be 1-sorted-yielding FinSequence;

      cluster ( Carrier f) -> FinSequence-like;

      coherence

      proof

        consider n be Nat such that

         A1: ( dom f) = ( Seg n) by FINSEQ_1:def 2;

        ex n be Nat st ( dom ( Carrier f)) = ( Seg n) by A1, PRALG_1:def 14;

        hence thesis by FINSEQ_1:def 2;

      end;

    end

    registration

      let f be non empty 1-sorted-yielding Function;

      cluster ( Carrier f) -> non empty;

      coherence

      proof

        ( dom f) = ( dom ( Carrier f)) by PRALG_1:def 14;

        hence thesis;

      end;

    end

    registration

      let f be non-Empty 1-sorted-yielding Function;

      cluster ( Carrier f) -> non-empty;

      coherence

      proof

        

         A0: ( dom f) = ( dom ( Carrier f)) by PRALG_1:def 14;

        for x be object st x in ( dom ( Carrier f)) holds (( Carrier f) . x) is non empty

        proof

          let x be object;

          assume

           A1: x in ( dom ( Carrier f));

          then

           A5: (f . x) in ( rng f) by A0, FUNCT_1: 3;

          then

          reconsider S = (f . x) as 1-sorted by PRALG_1:def 11;

          

           A6: S is non empty by A5, WAYBEL_3:def 7;

          consider R be 1-sorted such that

           A2: R = (f . x) and

           A3: (( Carrier f) . x) = the carrier of R by PRALG_1:def 14, A0, A1;

          thus thesis by A3, A2, A6;

        end;

        hence thesis;

      end;

    end

    definition

      let g be non empty non-Empty 1-sorted-yielding FinSequence;

      :: original: carr

      redefine

      :: PRVECT_1:def11

      func carr g -> Domain-Sequence means

      : Def10: ( len it ) = ( len g) & for j be Element of ( dom g) holds (it . j) = the carrier of (g . j);

      coherence ;

      compatibility

      proof

        let f be Domain-Sequence;

        thus f = ( carr g) implies ( len f) = ( len g) & for j be Element of ( dom g) holds (f . j) = the carrier of (g . j)

        proof

          assume

           a0: f = ( carr g);

          then ( dom f) = ( dom g) & for j be set st j in ( dom g) holds ex R be 1-sorted st R = (g . j) & (f . j) = the carrier of R by PRALG_1:def 14;

          for j be Element of ( dom g) holds (f . j) = the carrier of (g . j)

          proof

            let j be Element of ( dom g);

            consider R be 1-sorted such that

             A2: R = (g . j) & (f . j) = the carrier of R by a0, PRALG_1:def 14;

            thus thesis by A2;

          end;

          hence thesis by a0, FINSEQ_3: 29, PRALG_1:def 14;

        end;

        assume

         B1: ( len f) = ( len g) & for j be Element of ( dom g) holds (f . j) = the carrier of (g . j);

        for j be set st j in ( dom g) holds ex R be 1-sorted st R = (g . j) & (f . j) = the carrier of R

        proof

          let j be set;

          assume

           B3: j in ( dom g);

          then

          reconsider R = (g . j) as 1-sorted by PRALG_1:def 12;

          take R;

          thus thesis by B1, B3;

        end;

        hence thesis by B1, PRALG_1:def 14, FINSEQ_3: 29;

      end;

    end

    reserve g for Group-Sequence,

i for Element of ( dom ( carr g));

    definition

      let g be non empty non-empty-addLoopStr-yielding FinSequence;

      let i be Element of ( dom ( carr g));

      :: original: .

      redefine

      func g . i -> non empty addLoopStr ;

      coherence

      proof

        ( dom g) = ( Seg ( len g)) & ( Seg ( len ( carr g))) = ( dom ( carr g)) by FINSEQ_1:def 3;

        then

        reconsider i9 = i as Element of ( dom g) by Def10;

        (g . i9) is non empty addLoopStr;

        hence thesis;

      end;

    end

    definition

      let g, i;

      :: original: .

      redefine

      func g . i -> AbGroup ;

      coherence

      proof

        ( dom g) = ( Seg ( len g)) & ( Seg ( len ( carr g))) = ( dom ( carr g)) by FINSEQ_1:def 3;

        then

        reconsider i9 = i as Element of ( dom g) by Def10;

        (g . i9) is AbGroup;

        hence thesis;

      end;

    end

    definition

      let g be non-empty-addLoopStr-yielding non empty FinSequence;

      :: PRVECT_1:def12

      func addop g -> BinOps of ( carr g) means

      : Def11: ( len it ) = ( len ( carr g)) & for i be Element of ( dom ( carr g)) holds (it . i) = the addF of (g . i);

      existence

      proof

        deffunc F( Element of ( dom ( carr g))) = the addF of (g . $1);

        consider p be non empty FinSequence such that

         A1: ( len p) = ( len ( carr g)) & for i be Element of ( dom ( carr g)) holds (p . i) = F(i) from NEFinSeqLambda;

        now

          let i be Element of ( dom ( carr g));

          ( len g) = ( len ( carr g)) by Def10;

          then

          reconsider j = i as Element of ( dom g) by FINSEQ_3: 29;

          (p . i) = the addF of (g . i) & the carrier of (g . j) = (( carr g) . j) by A1, Def10;

          hence (p . i) is BinOp of (( carr g) . i);

        end;

        then

        reconsider p9 = p as BinOps of ( carr g) by A1, Th11;

        take p9;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let f,h be BinOps of ( carr g);

        assume that

         A2: ( len f) = ( len ( carr g)) and

         A3: for i be Element of ( dom ( carr g)) holds (f . i) = the addF of (g . i) and

         A4: ( len h) = ( len ( carr g)) and

         A5: for i be Element of ( dom ( carr g)) holds (h . i) = the addF of (g . i);

        reconsider f9 = f, h9 = h as FinSequence;

         A6:

        now

          let i be Nat;

          assume i in ( dom f9);

          then

          reconsider i9 = i as Element of ( dom ( carr g)) by A2, FINSEQ_3: 29;

          (f9 . i) = the addF of (g . i9) by A3;

          hence (f9 . i) = (h9 . i) by A5;

        end;

        ( dom f9) = ( Seg ( len f9)) & ( dom h9) = ( Seg ( len h9)) by FINSEQ_1:def 3;

        hence thesis by A2, A4, A6;

      end;

    end

    definition

      let g be non-empty-addLoopStr-yielding non empty FinSequence;

      :: PRVECT_1:def13

      func complop g -> UnOps of ( carr g) means

      : Def12: ( len it ) = ( len ( carr g)) & for i be Element of ( dom ( carr g)) holds (it . i) = ( comp (g . i));

      existence

      proof

        deffunc F( Element of ( dom ( carr g))) = ( comp (g . $1));

        consider p be non empty FinSequence such that

         A7: ( len p) = ( len ( carr g)) & for i be Element of ( dom ( carr g)) holds (p . i) = F(i) from NEFinSeqLambda;

        now

          let i be Element of ( dom ( carr g));

          ( len g) = ( len ( carr g)) by Def10;

          then

          reconsider j = i as Element of ( dom g) by FINSEQ_3: 29;

          (p . i) = ( comp (g . i)) & the carrier of (g . j) = (( carr g) . j) by A7, Def10;

          hence (p . i) is UnOp of (( carr g) . i);

        end;

        then

        reconsider p9 = p as UnOps of ( carr g) by A7, Th12;

        take p9;

        thus thesis by A7;

      end;

      uniqueness

      proof

        let f,h be UnOps of ( carr g);

        assume that

         A8: ( len f) = ( len ( carr g)) and

         A9: for i be Element of ( dom ( carr g)) holds (f . i) = ( comp (g . i)) and

         A10: ( len h) = ( len ( carr g)) and

         A11: for i be Element of ( dom ( carr g)) holds (h . i) = ( comp (g . i));

        reconsider f9 = f, h9 = h as FinSequence;

         A12:

        now

          let i be Nat;

          assume i in ( dom f9);

          then

          reconsider i9 = i as Element of ( dom ( carr g)) by A8, FINSEQ_3: 29;

          (f . i) = ( comp (g . i9)) by A9;

          hence (f . i) = (h . i) by A11;

        end;

        ( dom f9) = ( Seg ( len f9)) & ( dom h9) = ( Seg ( len h9)) by FINSEQ_1:def 3;

        hence thesis by A8, A10, A12;

      end;

      :: PRVECT_1:def14

      func zeros g -> Element of ( product ( carr g)) means

      : Def13: for i be Element of ( dom ( carr g)) holds (it . i) = ( 0. (g . i));

      existence

      proof

        deffunc F( Element of ( dom ( carr g))) = ( 0. (g . $1));

        

         A13: ( dom ( carr g)) = ( Seg ( len ( carr g))) by FINSEQ_1:def 3;

        consider p be non empty FinSequence such that

         A14: ( len p) = ( len ( carr g)) & for i be Element of ( dom ( carr g)) holds (p . i) = F(i) from NEFinSeqLambda;

        

         A15: ( dom g) = ( Seg ( len g)) by FINSEQ_1:def 3;

         A16:

        now

          let i be object;

          assume i in ( dom ( carr g));

          then

          reconsider x = i as Element of ( dom ( carr g));

          reconsider x9 = x as Element of ( dom g) by A15, A13, Def10;

          (p . x) = ( 0. (g . x)) & (( carr g) . x9) = the carrier of (g . x9) by A14, Def10;

          hence (p . i) in (( carr g) . i);

        end;

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

        then

        reconsider t = p as Element of ( product ( carr g)) by A14, FINSEQ_1:def 3, A16, CARD_3: 9;

        take t;

        thus thesis by A14;

      end;

      uniqueness

      proof

        let f,h be Element of ( product ( carr g));

        assume that

         A17: for i be Element of ( dom ( carr g)) holds (f . i) = ( 0. (g . i)) and

         A18: for i be Element of ( dom ( carr g)) holds (h . i) = ( 0. (g . i));

        reconsider f9 = f, h9 = h as Function;

         A19:

        now

          let x be object;

          assume x in ( dom ( carr g));

          then

          reconsider i = x as Element of ( dom ( carr g));

          

          thus (f9 . x) = ( 0. (g . i)) by A17

          .= (h9 . x) by A18;

        end;

        ( dom f9) = ( dom ( carr g)) & ( dom h9) = ( dom ( carr g)) by CARD_3: 9;

        hence thesis by A19;

      end;

    end

    definition

      let G be non-empty-addLoopStr-yielding non empty FinSequence;

      :: PRVECT_1:def15

      func product G -> strict non empty addLoopStr equals addLoopStr (# ( product ( carr G)), [:( addop G):], ( zeros G) #);

      coherence ;

    end

    registration

      let G be Group-Sequence;

      cluster ( product G) -> add-associative right_zeroed right_complementable non empty Abelian;

      coherence

      proof

        reconsider GS = addLoopStr (# ( product ( carr G)), [:( addop G):], ( zeros G) #) as non empty addLoopStr;

         A1:

        now

          let i be Element of ( dom ( carr G));

          ( dom G) = ( Seg ( len G)) by FINSEQ_1:def 3

          .= ( Seg ( len ( carr G))) by Def10

          .= ( dom ( carr G)) by FINSEQ_1:def 3;

          hence (( carr G) . i) = car(.) by Def10;

        end;

        now

          let i be Element of ( dom ( carr G));

          (( addop G) . i) = ad(.) & (( carr G) . i) = car(.) by A1, Def11;

          hence (( addop G) . i) is associative by FVSUM_1: 2;

        end;

        then

         A2: [:( addop G):] is associative by Th18;

        now

          let i be Element of ( dom ( carr G));

          

           A3: (( carr G) . i) = car(.) by A1;

          (( addop G) . i) = ad(.) & (( zeros G) . i) = zr(.) by Def11, Def13;

          hence (( zeros G) . i) is_a_unity_wrt (( addop G) . i) by A3, Th1;

        end;

        then

         A4: ( zeros G) is_a_unity_wrt [:( addop G):] by Th19;

        

         A5: GS is right_complementable

        proof

          let x be Element of GS;

          reconsider y = (( Frege ( complop G)) . x) as Element of GS by FUNCT_2: 5;

          take y;

          now

            let i be Element of ( dom ( carr G));

            

             A6: (( addop G) . i) = ad(.) & (( complop G) . i) = cc(.) by Def11, Def12;

             zr(.) is_a_unity_wrt ad(.) & (( carr G) . i) = car(.) by A1, Th1;

            hence (( complop G) . i) is_an_inverseOp_wrt (( addop G) . i) & (( addop G) . i) is having_a_unity by A6, Th2, SETWISEO:def 2;

          end;

          then ( Frege ( complop G)) is_an_inverseOp_wrt [:( addop G):] by Th20;

          then (x + y) = ( the_unity_wrt [:( addop G):]);

          hence thesis by A4, BINOP_1:def 8;

        end;

        now

          let i be Element of ( dom ( carr G));

          (( addop G) . i) = ad(.) & (( carr G) . i) = car(.) by A1, Def11;

          hence (( addop G) . i) is commutative by FVSUM_1: 1;

        end;

        then ( 0. GS) = ( zeros G) & [:( addop G):] is commutative by Th17;

        hence thesis by A2, A4, A5, BINOP_1: 3;

      end;

    end