zmodlat1.miz



    begin

    theorem :: ZMODLAT1:1

    

     LMEQ: for D,E be non empty set, n,m be Nat, M be Matrix of n, m, D st for i,j be Nat st [i, j] in ( Indices M) holds (M * (i,j)) in E holds M is Matrix of n, m, E

    proof

      let D,E be non empty set, n,m be Nat, M be Matrix of n, m, D;

      assume for i,j be Nat st [i, j] in ( Indices M) holds (M * (i,j)) in E;

      then

      reconsider G = M as Matrix of E by ZMATRLIN: 5;

      per cases ;

        suppose not n > 0 ;

        then

         X1: n = 0 ;

        then G = {} by MATRIX_0: 22;

        hence thesis by X1, MATRIX_0: 13;

      end;

        suppose

         X1: n > 0 ;

        then ( len G) = n & ( width G) = m by MATRIX_0: 23;

        hence thesis by X1, MATRIX_0: 20;

      end;

    end;

    definition

      let F be 1-sorted;

      struct ( ModuleStr over F) LatticeStr over F (# the carrier -> set,

the addF -> BinOp of the carrier,

the ZeroF -> Element of the carrier,

the lmult -> Function of [:the carrier of F, the carrier:], the carrier,

the scalar -> Function of [: the carrier, the carrier:], the carrier of F_Real #)

       attr strict strict;

    end

    registration

      let F be 1-sorted;

      cluster strict non empty for LatticeStr over F;

      correctness

      proof

        set D = the non empty set, Z = the Element of D, a = the BinOp of D, m = the Function of [:the carrier of F, D:], D, s = the Function of [:D, D:], the carrier of F_Real ;

        take LatticeStr (# D, a, Z, m, s #);

        thus thesis;

      end;

    end

    registration

      let F be 1-sorted;

      let D be non empty set, Z be Element of D, a be BinOp of D, m be Function of [:the carrier of F, D:], D, s be Function of [:D, D:], the carrier of F_Real ;

      cluster LatticeStr (# D, a, Z, m, s #) -> non empty;

      coherence ;

    end

    definition

      let X be non empty LatticeStr over INT.Ring ;

      let x,y be Vector of X;

      :: ZMODLAT1:def1

      func <;x,y;> -> Element of F_Real equals (the scalar of X . [x, y]);

      correctness ;

    end

    definition

      let X be non empty LatticeStr over INT.Ring ;

      let x be Vector of X;

      :: ZMODLAT1:def2

      func ||.x.|| -> Element of F_Real equals <;x, x;>;

      correctness ;

    end

    definition

      let IT be non empty LatticeStr over INT.Ring ;

      :: ZMODLAT1:def3

      attr IT is Z_Lattice-like means

      : defZLattice: (for x be Vector of IT st for y be Vector of IT holds <;x, y;> = 0 holds x = ( 0. IT)) & (for x,y be Vector of IT holds <;x, y;> = <;y, x;>) & (for x,y,z be Vector of IT, a be Element of INT.Ring holds <;(x + y), z;> = ( <;x, z;> + <;y, z;>) & <;(a * x), y;> = (a * <;x, y;>));

    end

    definition

      let V be Z_Module, sc be Function of [:the carrier of V, the carrier of V:], the carrier of F_Real ;

      :: ZMODLAT1:def4

      func GenLat (V,sc) -> non empty LatticeStr over INT.Ring equals LatticeStr (# the carrier of V, the addF of V, ( 0. V), the lmult of V, sc #);

      coherence ;

    end

    

     ZMtoZL1: for V be Z_Module, sc be Function of [:the carrier of V, the carrier of V:], the carrier of F_Real holds ( GenLat (V,sc)) is Abelian add-associative right_zeroed right_complementable scalar-distributive vector-distributive scalar-associative scalar-unital

    proof

      let V be Z_Module, sc be Function of [:the carrier of V, the carrier of V:], the carrier of F_Real ;

      set L = ( GenLat (V,sc));

      

       A1: for x,y be Vector of L holds for x9,y9 be Vector of V st x = x9 & y = y9 holds (x + y) = (x9 + y9) & for a be Element of INT.Ring holds (a * x) = (a * x9);

      thus for v,w be Vector of L holds (v + w) = (w + v)

      proof

        let v,w be Vector of L;

        reconsider v9 = v, w9 = w as Vector of V;

        

        thus (v + w) = (w9 + v9) by A1

        .= (w + v);

      end;

      thus for u,v,w be Vector of L holds ((u + v) + w) = (u + (v + w))

      proof

        let u,v,w be Vector of L;

        reconsider u9 = u, v9 = v, w9 = w as Vector of V;

        

        thus ((u + v) + w) = ((u9 + v9) + w9)

        .= (u9 + (v9 + w9)) by RLVECT_1:def 3

        .= (u + (v + w));

      end;

      thus for v be Vector of L holds (v + ( 0. L)) = v

      proof

        let v be Vector of L;

        reconsider v9 = v as Vector of V;

        

        thus (v + ( 0. L)) = (v9 + ( 0. V))

        .= v;

      end;

      thus L is right_complementable

      proof

        let v be Vector of L;

        reconsider v9 = v as Vector of V;

        consider w9 be Vector of V such that

         A2: (v9 + w9) = ( 0. V) by ALGSTR_0:def 11;

        reconsider w = w9 as Vector of L;

        take w;

        thus thesis by A2;

      end;

      thus for a,b be Element of INT.Ring , v be Vector of L holds ((a + b) * v) = ((a * v) + (b * v))

      proof

        let a,b be Element of INT.Ring , v be Vector of L;

        reconsider v9 = v as Vector of V;

        

        thus ((a + b) * v) = ((a + b) * v9)

        .= ((a * v9) + (b * v9)) by VECTSP_1:def 15

        .= ((a * v) + (b * v));

      end;

      thus for a be Element of INT.Ring , v,w be Vector of L holds (a * (v + w)) = ((a * v) + (a * w))

      proof

        let a be Element of INT.Ring , v,w be Vector of L;

        reconsider v9 = v, w9 = w as Vector of V;

        

        thus (a * (v + w)) = (a * (v9 + w9))

        .= ((a * v9) + (a * w9)) by VECTSP_1:def 14

        .= ((a * v) + (a * w));

      end;

      thus for a,b be Element of INT.Ring , v be Vector of L holds ((a * b) * v) = (a * (b * v))

      proof

        let a,b be Element of INT.Ring , v be Vector of L;

        reconsider v9 = v as Vector of V;

        

        thus ((a * b) * v) = ((a * b) * v9)

        .= (a * (b * v9)) by VECTSP_1:def 16

        .= (a * (b * v));

      end;

      thus for v be Vector of L holds (( 1. INT.Ring ) * v) = v

      proof

        let v be Vector of L;

        reconsider v9 = v as Vector of V;

        

        thus (( 1. INT.Ring ) * v) = (( 1. INT.Ring ) * v9)

        .= v by VECTSP_1:def 17;

      end;

    end;

    registration

      cluster vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed right_complementable strict for non empty LatticeStr over INT.Ring ;

      correctness

      proof

        set V0 = the Z_Module;

        reconsider nilfunc = ( [:the carrier of ( (0). V0), the carrier of ( (0). V0):] --> 0 ) as Function of [:the carrier of ( (0). V0), the carrier of ( (0). V0):], the carrier of F_Real by FUNCOP_1: 45;

        set X0 = ( GenLat (( (0). V0),nilfunc));

        take X0;

        thus X0 is vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed right_complementable strict by ZMtoZL1;

      end;

    end

    registration

      let V be Z_Module;

      let sc be Function of [:the carrier of V, the carrier of V:], the carrier of F_Real ;

      cluster ( GenLat (V,sc)) -> Abelian add-associative right_zeroed right_complementable scalar-distributive vector-distributive scalar-associative scalar-unital;

      correctness by ZMtoZL1;

    end

    theorem :: ZMODLAT1:2

    

     LmZMtoZL1: for V be Z_Module, sc be Function of [:the carrier of V, the carrier of V:], the carrier of F_Real holds ( GenLat (V,sc)) is Submodule of V

    proof

      let V be Z_Module, sc be Function of [:the carrier of V, the carrier of V:], the carrier of F_Real ;

      set L = ( GenLat (V,sc));

      

       A2: ( 0. L) = ( 0. V);

      

       A3: the addF of L = (the addF of V || the carrier of L);

      the lmult of L = (the lmult of V | [:the carrier of INT.Ring , the carrier of L:]);

      hence thesis by A2, A3, VECTSP_4:def 2;

    end;

    theorem :: ZMODLAT1:3

    for V be Z_Module, sc be Function of [:the carrier of V, the carrier of V:], the carrier of F_Real holds V is Submodule of ( GenLat (V,sc))

    proof

      let V be Z_Module, sc be Function of [:the carrier of V, the carrier of V:], the carrier of F_Real ;

      set L = ( GenLat (V,sc));

      

       A2: ( 0. V) = ( 0. L);

      

       A3: the addF of V = (the addF of L || the carrier of V);

      the lmult of V = (the lmult of L | [:the carrier of INT.Ring , the carrier of V:]);

      hence thesis by A2, A3, VECTSP_4:def 2;

    end;

    

     ZMtoZL2: for V be free Z_Module, sc be Function of [:the carrier of V, the carrier of V:], the carrier of F_Real holds ( GenLat (V,sc)) is free

    proof

      let V be free Z_Module, sc be Function of [:the carrier of V, the carrier of V:], the carrier of F_Real ;

      set L = ( GenLat (V,sc));

      consider A be Subset of V such that

       AX2: A is base by VECTSP_7:def 4;

      reconsider AA = A as Subset of L;

      

       A4: L is Submodule of V by LmZMtoZL1;

      

       A5: AA is linearly-independent by AX2, A4, VECTSP_7:def 3, ZMODUL03: 16;

      ( Lin AA) = ( Lin A) by A4, ZMODUL03: 20

      .= ( (Omega). L) by AX2, VECTSP_7:def 3;

      hence thesis by A5, VECTSP_7:def 3, VECTSP_7:def 4;

    end;

    registration

      cluster free for Abelian add-associative right_zeroed right_complementable scalar-distributive vector-distributive scalar-associative scalar-unital non empty LatticeStr over INT.Ring ;

      correctness

      proof

        set V0 = the free Z_Module;

        reconsider nilfunc = ( [:the carrier of ( (0). V0), the carrier of ( (0). V0):] --> 0 ) as Function of [:the carrier of ( (0). V0), the carrier of ( (0). V0):], the carrier of F_Real by FUNCOP_1: 45;

        set X0 = ( GenLat (( (0). V0),nilfunc));

        reconsider X0 as Abelian add-associative right_zeroed right_complementable scalar-distributive vector-distributive scalar-associative scalar-unital non empty LatticeStr over INT.Ring ;

        take X0;

        thus X0 is free by ZMtoZL2;

      end;

    end

    registration

      let V be free Z_Module;

      let sc be Function of [:the carrier of V, the carrier of V:], the carrier of F_Real ;

      cluster ( GenLat (V,sc)) -> free;

      correctness by ZMtoZL2;

    end

    registration

      cluster torsion-free for Abelian add-associative right_zeroed right_complementable scalar-distributive vector-distributive scalar-associative scalar-unital non empty LatticeStr over INT.Ring ;

      correctness

      proof

        set V0 = the free Z_Module;

        reconsider nilfunc = ( [:the carrier of ( (0). V0), the carrier of ( (0). V0):] --> 0 ) as Function of [:the carrier of ( (0). V0), the carrier of ( (0). V0):], the carrier of F_Real by FUNCOP_1: 45;

        set X0 = ( GenLat (( (0). V0),nilfunc));

        reconsider X0 as Abelian add-associative right_zeroed right_complementable scalar-distributive vector-distributive scalar-associative scalar-unital non empty LatticeStr over INT.Ring ;

        take X0;

        thus X0 is torsion-free;

      end;

    end

    theorem :: ZMODLAT1:4

    

     ZMtoZL3: for V be finite-rank free Z_Module, sc be Function of [:the carrier of V, the carrier of V:], the carrier of F_Real holds ( GenLat (V,sc)) is finite-rank

    proof

      let V be finite-rank free Z_Module, sc be Function of [:the carrier of V, the carrier of V:], the carrier of F_Real ;

      set L = ( GenLat (V,sc));

      L is Submodule of V by LmZMtoZL1;

      hence thesis;

    end;

    registration

      cluster finite-rank for free Abelian add-associative right_zeroed right_complementable scalar-distributive vector-distributive scalar-associative scalar-unital non empty LatticeStr over INT.Ring ;

      correctness

      proof

        set V0 = the finite-rank free Z_Module;

        reconsider nilfunc = ( [:the carrier of ( (0). V0), the carrier of ( (0). V0):] --> 0 ) as Function of [:the carrier of ( (0). V0), the carrier of ( (0). V0):], the carrier of F_Real by FUNCOP_1: 45;

        set X0 = ( GenLat (( (0). V0),nilfunc));

        reconsider X0 as Abelian add-associative right_zeroed right_complementable scalar-distributive vector-distributive scalar-associative scalar-unital non empty LatticeStr over INT.Ring ;

        reconsider X0 as free Abelian add-associative right_zeroed right_complementable scalar-distributive vector-distributive scalar-associative scalar-unital non empty LatticeStr over INT.Ring ;

        take X0;

        thus X0 is finite-rank by ZMtoZL3;

      end;

    end

    registration

      let V be finite-rank free Z_Module;

      let sc be Function of [:the carrier of V, the carrier of V:], the carrier of F_Real ;

      cluster ( GenLat (V,sc)) -> finite-rank;

      correctness by ZMtoZL3;

    end

    theorem :: ZMODLAT1:5

    

     ThTrivialLat1: for V be finite-rank free Z_Module, f be Function of [:the carrier of ( (0). V), the carrier of ( (0). V):], the carrier of F_Real st f = ( [:the carrier of ( (0). V), the carrier of ( (0). V):] --> ( 0. F_Real )) holds ( GenLat (( (0). V),f)) is Z_Lattice-like

    proof

      let V be finite-rank free Z_Module, f be Function of [:the carrier of ( (0). V), the carrier of ( (0). V):], the carrier of F_Real such that

       P1: f = ( [:the carrier of ( (0). V), the carrier of ( (0). V):] --> ( 0. F_Real ));

      set X = ( GenLat (( (0). V),f));

      reconsider X as Abelian add-associative right_zeroed right_complementable scalar-distributive vector-distributive scalar-associative scalar-unital non empty LatticeStr over INT.Ring ;

      reconsider X as free Abelian add-associative right_zeroed right_complementable scalar-distributive vector-distributive scalar-associative scalar-unital non empty LatticeStr over INT.Ring ;

      reconsider X as finite-rank free Abelian add-associative right_zeroed right_complementable scalar-distributive vector-distributive scalar-associative scalar-unital non empty LatticeStr over INT.Ring ;

      

       P2: for x be Vector of X st for y be Vector of X holds <;x, y;> = 0 holds x = ( 0. X)

      proof

        let x be Vector of X such that for y be Vector of X holds <;x, y;> = 0 ;

        x in the carrier of ( (0). V);

        then x in {( 0. V)} by VECTSP_4:def 3;

        

        hence x = ( 0. V) by TARSKI:def 1

        .= ( 0. X) by ZMODUL01: 26;

      end;

      for x,y,z be Vector of X, a be Element of INT.Ring holds <;x, y;> = <;y, x;> & <;(x + y), z;> = ( <;x, z;> + <;y, z;>) & <;(a * x), y;> = (a * <;x, y;>)

      proof

        let x,y,z be Vector of X;

        let a be Element of INT.Ring ;

        

         A1: the carrier of ( (0). V) = {( 0. V)} by VECTSP_4:def 3;

        then

         A3: ( 0. V) in the carrier of ( (0). V) by TARSKI:def 1;

        thus <;x, y;> = <;y, x;>

        proof

          x = ( 0. V) & y = ( 0. V) by A1, TARSKI:def 1;

          hence thesis;

        end;

        

         A4: (f . [( 0. V), ( 0. V)]) = 0 by A3, P1, FUNCOP_1: 7, ZFMISC_1: 87;

        thus <;(x + y), z;> = ( <;x, z;> + <;y, z;>)

        proof

          reconsider u = x, v = y, w = z as Vector of ( (0). V);

          

           B2: w = ( 0. V) by A1, TARSKI:def 1;

          u = ( 0. V) & v = ( 0. V) by A1, TARSKI:def 1;

          hence thesis by A1, A4, B2, TARSKI:def 1;

        end;

        thus <;(a * x), y;> = (a * <;x, y;>)

        proof

          reconsider u = x, v = y as Vector of ( (0). V);

          u = ( 0. V) & v = ( 0. V) by A1, TARSKI:def 1;

          hence thesis by A1, A4, TARSKI:def 1;

        end;

      end;

      hence thesis by P2;

    end;

    registration

      cluster Z_Lattice-like for non empty LatticeStr over INT.Ring ;

      existence

      proof

        set V0 = the finite-rank free Z_Module;

        reconsider nilfunc = ( [:the carrier of ( (0). V0), the carrier of ( (0). V0):] --> ( 0. F_Real )) as Function of [:the carrier of ( (0). V0), the carrier of ( (0). V0):], the carrier of F_Real ;

        set X0 = ( GenLat (( (0). V0),nilfunc));

        reconsider X0 as finite-rank free Abelian add-associative right_zeroed right_complementable scalar-distributive vector-distributive scalar-associative scalar-unital non empty LatticeStr over INT.Ring ;

        take X0;

        thus thesis by ThTrivialLat1;

      end;

    end

    registration

      cluster Z_Lattice-like for finite-rank free Abelian add-associative right_zeroed right_complementable scalar-distributive vector-distributive scalar-associative scalar-unital non empty LatticeStr over INT.Ring ;

      existence

      proof

        set V0 = the finite-rank free Z_Module;

        reconsider nilfunc = ( [:the carrier of ( (0). V0), the carrier of ( (0). V0):] --> 0 ) as Function of [:the carrier of ( (0). V0), the carrier of ( (0). V0):], the carrier of F_Real by FUNCOP_1: 45;

        set X0 = ( GenLat (( (0). V0),nilfunc));

        reconsider X0 as finite-rank free Abelian add-associative right_zeroed right_complementable scalar-distributive vector-distributive scalar-associative scalar-unital non empty LatticeStr over INT.Ring ;

        take X0;

        thus thesis by ThTrivialLat1;

      end;

    end

    registration

      cluster strict for finite-rank free Z_Lattice-like Abelian add-associative right_zeroed right_complementable scalar-distributive vector-distributive scalar-associative scalar-unital non empty LatticeStr over INT.Ring ;

      existence

      proof

        set V0 = the finite-rank free Z_Module;

        reconsider nilfunc = ( [:the carrier of ( (0). V0), the carrier of ( (0). V0):] --> 0 ) as Function of [:the carrier of ( (0). V0), the carrier of ( (0). V0):], the carrier of F_Real by FUNCOP_1: 45;

        set X0 = ( GenLat (( (0). V0),nilfunc));

        reconsider X0 as finite-rank free Abelian add-associative right_zeroed right_complementable scalar-distributive vector-distributive scalar-associative scalar-unital non empty LatticeStr over INT.Ring ;

        reconsider X0 as Z_Lattice-like finite-rank free Abelian add-associative right_zeroed right_complementable scalar-distributive vector-distributive scalar-associative scalar-unital non empty LatticeStr over INT.Ring by ThTrivialLat1;

        take X0;

        thus X0 is strict;

      end;

    end

    definition

      mode Z_Lattice is finite-rank free Z_Lattice-like Abelian add-associative right_zeroed right_complementable scalar-distributive vector-distributive scalar-associative scalar-unital non empty LatticeStr over INT.Ring ;

    end

    theorem :: ZMODLAT1:6

    

     ThNonTrivialLat1: for V be non trivial torsion-free Z_Module, Z be Submodule of V, v be non zero Vector of V, f be Function of [:the carrier of Z, the carrier of Z:], the carrier of F_Real st Z = ( Lin {v}) & (for v1,v2 be Vector of Z, a,b be Element of INT.Ring st v1 = (a * v) & v2 = (b * v) holds (f . (v1,v2)) = (a * b)) holds ( GenLat (Z,f)) is Z_Lattice-like

    proof

      let V be non trivial torsion-free Z_Module, Z be Submodule of V, v be non zero Vector of V, f be Function of [:the carrier of Z, the carrier of Z:], the carrier of F_Real such that

       A1: Z = ( Lin {v}) and

       A2: (for v1,v2 be Vector of Z, a,b be Element of INT.Ring st v1 = (a * v) & v2 = (b * v) holds (f . (v1,v2)) = (a * b));

      set L = ( GenLat (Z,f));

      reconsider L as finite-rank free Abelian add-associative right_zeroed right_complementable scalar-distributive vector-distributive scalar-associative scalar-unital non empty LatticeStr over INT.Ring by A1;

      L is Z_Lattice-like

      proof

        thus for x be Vector of L st for y be Vector of L holds <;x, y;> = 0 holds x = ( 0. L)

        proof

          let x be Vector of L such that

           C1: for y be Vector of L holds <;x, y;> = 0 ;

          assume x <> ( 0. L);

          then

           C2: x <> ( 0. V) by ZMODUL01: 26;

          x in ( Lin {v}) by A1;

          then

          consider ix be Element of INT.Ring such that

           C3: x = (ix * v) by ZMODUL06: 19;

          reconsider xx = x as Vector of Z;

          

           C4: ix <> 0 by C2, C3, ZMODUL01: 1;

           <;x, x;> = (f . (x,x))

          .= (ix * ix) by A2, C3;

          hence contradiction by C1, C4;

        end;

        thus for x,y be Vector of L holds <;x, y;> = <;y, x;>

        proof

          let x,y be Vector of L;

          

           C1: x in ( Lin {v}) & y in ( Lin {v}) by A1;

          then

          consider ix be Element of INT.Ring such that

           C2: x = (ix * v) by ZMODUL06: 19;

          consider iy be Element of INT.Ring such that

           C3: y = (iy * v) by C1, ZMODUL06: 19;

          

          thus <;x, y;> = (f . (x,y))

          .= (ix * iy) by A2, C2, C3

          .= (f . (y,x)) by A2, C2, C3

          .= <;y, x;>;

        end;

        thus for x,y,z be Vector of L, a be Element of INT.Ring holds <;(x + y), z;> = ( <;x, z;> + <;y, z;>) & <;(a * x), y;> = (a * <;x, y;>)

        proof

          let x,y,z be Vector of L, a be Element of INT.Ring ;

          

           C1: x in ( Lin {v}) & y in ( Lin {v}) & z in ( Lin {v}) by A1;

          then

          consider ix be Element of INT.Ring such that

           C2: x = (ix * v) by ZMODUL06: 19;

          consider iy be Element of INT.Ring such that

           C3: y = (iy * v) by C1, ZMODUL06: 19;

          consider iz be Element of INT.Ring such that

           C4: z = (iz * v) by C1, ZMODUL06: 19;

          (ix * v) in ( Lin {v}) by ZMODUL06: 21;

          then

          reconsider iixv = (ix * v) as Vector of Z by A1;

          reconsider ixv = (ix * v) as Vector of V;

          (iy * v) in ( Lin {v}) by ZMODUL06: 21;

          then

          reconsider iiyv = (iy * v) as Vector of Z by A1;

          reconsider iyv = (iy * v) as Vector of V;

          

           C5: (x + y) = (iixv + iiyv) by C2, C3

          .= (ixv + iyv) by ZMODUL01: 28

          .= ((ix + iy) * v) by VECTSP_1:def 15;

          

           C6: (a * x) = (a * iixv) by C2

          .= (a * ixv) by ZMODUL01: 29

          .= ((a * ix) * v) by VECTSP_1:def 16;

          

          thus <;(x + y), z;> = (f . ((x + y),z))

          .= ((ix + iy) * iz) by A2, C4, C5

          .= ((ix * iz) + (iy * iz))

          .= ((f . (x,z)) + (iy * iz)) by A2, C2, C4

          .= ((f . [x, z]) + (f . (y,z))) by A2, C3, C4

          .= ( <;x, z;> + <;y, z;>);

          

          thus <;(a * x), y;> = (f . ((a * x),y))

          .= ((a * ix) * iy) by A2, C3, C6

          .= (a * (ix * iy))

          .= (a * (f . (x,y))) by A2, C2, C3

          .= (a * <;x, y;>);

        end;

      end;

      hence thesis;

    end;

    registration

      cluster non trivial for Z_Lattice;

      correctness

      proof

        set V = the non trivial torsion-free Z_Module;

        set v = the non zero Vector of V;

        set Z = ( Lin {v});

        defpred P[ object, object] means ex a,b be Element of INT.Ring st $1 = [(a * v), (b * v)] & $2 = (a * b);

        

         A1: for x be Element of [:the carrier of Z, the carrier of Z:] holds ex y be Element of the carrier of F_Real st P[x, y]

        proof

          let x be Element of [:the carrier of Z, the carrier of Z:];

          consider x1,x2 be object such that

           B1: x1 in the carrier of Z & x2 in the carrier of Z & x = [x1, x2] by ZFMISC_1:def 2;

          reconsider x1, x2 as Vector of Z by B1;

          x1 in ( Lin {v});

          then

          consider i1 be Element of INT.Ring such that

           B2: x1 = (i1 * v) by ZMODUL06: 19;

          x2 in ( Lin {v});

          then

          consider i2 be Element of INT.Ring such that

           B3: x2 = (i2 * v) by ZMODUL06: 19;

          reconsider i12 = (i1 * i2) as Element of INT ;

           INT c= the carrier of F_Real by NUMBERS: 5, XBOOLE_0:def 8;

          then

          reconsider i12 as Element of the carrier of F_Real ;

          take i12;

          thus thesis by B1, B2, B3;

        end;

        consider f be Function of [:the carrier of Z, the carrier of Z:], the carrier of F_Real such that

         A2: for x be Element of [:the carrier of Z, the carrier of Z:] holds P[x, (f . x)] from FUNCT_2:sch 3( A1);

        

         A3: for v1,v2 be Vector of Z, a,b be Element of INT.Ring st v1 = (a * v) & v2 = (b * v) holds (f . (v1,v2)) = (a * b)

        proof

          let v1,v2 be Vector of Z, a,b be Element of INT.Ring such that

           B0: v1 = (a * v) & v2 = (b * v);

          consider a0,b0 be Element of INT.Ring such that

           B1: [v1, v2] = [(a0 * v), (b0 * v)] & (f . [v1, v2]) = (a0 * b0) by A2;

          

           B2: v <> ( 0. V);

          v1 = (a0 * v) by B1, XTUPLE_0: 1;

          then

           B3: a = a0 by B0, B2, ZMODUL01: 11;

          v2 = (b0 * v) by B1, XTUPLE_0: 1;

          hence thesis by B0, B1, B2, B3, ZMODUL01: 11;

        end;

        set L = ( GenLat (Z,f));

        reconsider L as finite-rank free Abelian add-associative right_zeroed right_complementable scalar-distributive vector-distributive scalar-associative scalar-unital non empty LatticeStr over INT.Ring ;

        reconsider L as strict Z_Lattice by A3, ThNonTrivialLat1;

        take L;

        L is non trivial

        proof

          assume

           B1: L is trivial;

          v in ( Lin {v}) by ZMODUL06: 20;

          then

           B2: v = ( 0. L) by B1;

          v <> ( 0. V);

          hence contradiction by B2, ZMODUL01: 26;

        end;

        hence thesis;

      end;

    end

    registration

      let V be torsion-free Z_Module;

      cluster ( Z_MQ_VectSp V) -> scalar-distributive vector-distributive scalar-associative scalar-unital add-associative right_zeroed right_complementable Abelian;

      correctness ;

    end

    theorem :: ZMODLAT1:7

    

     ThSc1: for L be Z_Lattice, v,u be Vector of L holds <;v, ( - u);> = ( - <;v, u;>) & <;( - v), u;> = ( - <;v, u;>)

    proof

      let L be Z_Lattice, v,u be Vector of L;

      

      thus <;v, ( - u);> = <;v, (( - ( 1. INT.Ring )) * u);> by ZMODUL01: 2

      .= <;(( - ( 1. INT.Ring )) * u), v;> by defZLattice

      .= (( - 1) * <;u, v;>) by defZLattice

      .= ( - <;u, v;>)

      .= ( - <;v, u;>) by defZLattice;

      

      thus <;( - v), u;> = <;(( - ( 1. INT.Ring )) * v), u;> by ZMODUL01: 2

      .= (( - ( 1. INT.Ring )) * <;v, u;>) by defZLattice

      .= ( - <;v, u;>);

    end;

    theorem :: ZMODLAT1:8

    

     ThSc2: for L be Z_Lattice, v,u,w be Vector of L holds <;v, (u + w);> = ( <;v, u;> + <;v, w;>)

    proof

      let L be Z_Lattice, v,u,w be Vector of L;

      

      thus <;v, (u + w);> = <;(u + w), v;> by defZLattice

      .= ( <;u, v;> + <;w, v;>) by defZLattice

      .= ( <;v, u;> + <;w, v;>) by defZLattice

      .= ( <;v, u;> + <;v, w;>) by defZLattice;

    end;

    theorem :: ZMODLAT1:9

    

     ThSc3: for L be Z_Lattice, v,u be Vector of L, a be Element of INT.Ring holds <;v, (a * u);> = (a * <;v, u;>)

    proof

      let L be Z_Lattice, v,u be Vector of L, a be Element of INT.Ring ;

      

      thus <;v, (a * u);> = <;(a * u), v;> by defZLattice

      .= (a * <;u, v;>) by defZLattice

      .= (a * <;v, u;>) by defZLattice;

    end;

    theorem :: ZMODLAT1:10

    

     ThSc4: for L be Z_Lattice, v,u,w be Vector of L, a,b be Element of INT.Ring holds <;((a * v) + (b * u)), w;> = ((a * <;v, w;>) + (b * <;u, w;>)) & <;v, ((a * u) + (b * w));> = ((a * <;v, u;>) + (b * <;v, w;>))

    proof

      let L be Z_Lattice, v,u,w be Vector of L, a,b be Element of INT.Ring ;

      

      thus <;((a * v) + (b * u)), w;> = ( <;(a * v), w;> + <;(b * u), w;>) by defZLattice

      .= ((a * <;v, w;>) + <;(b * u), w;>) by defZLattice

      .= ((a * <;v, w;>) + (b * <;u, w;>)) by defZLattice;

      

      thus <;v, ((a * u) + (b * w));> = ( <;v, (a * u);> + <;v, (b * w);>) by ThSc2

      .= ((a * <;v, u;>) + <;v, (b * w);>) by ThSc3

      .= ((a * <;v, u;>) + (b * <;v, w;>)) by ThSc3;

    end;

    theorem :: ZMODLAT1:11

    

     ThSc5: for L be Z_Lattice, v,u,w be Vector of L holds <;(v - u), w;> = ( <;v, w;> - <;u, w;>) & <;v, (u - w);> = ( <;v, u;> - <;v, w;>)

    proof

      let L be Z_Lattice, v,u,w be Vector of L;

      

      thus <;(v - u), w;> = <;(v + (( - ( 1. INT.Ring )) * u)), w;> by ZMODUL01: 2

      .= ( <;v, w;> + <;(( - ( 1. INT.Ring )) * u), w;>) by defZLattice

      .= ( <;v, w;> + (( - ( 1. INT.Ring )) * <;u, w;>)) by defZLattice

      .= ( <;v, w;> - <;u, w;>);

      

      thus <;v, (u - w);> = <;v, (u + (( - ( 1. INT.Ring )) * w));> by ZMODUL01: 2

      .= ( <;v, u;> + <;v, (( - ( 1. INT.Ring )) * w);>) by ThSc2

      .= ( <;v, u;> + (( - ( 1. INT.Ring )) * <;v, w;>)) by ThSc3

      .= ( <;v, u;> - <;v, w;>);

    end;

    theorem :: ZMODLAT1:12

    

     ThSc6: for L be Z_Lattice, v be Vector of L holds <;v, ( 0. L);> = 0 & <;( 0. L), v;> = 0

    proof

      let L be Z_Lattice, v be Vector of L;

      

      thus <;v, ( 0. L);> = <;v, (v - v);> by RLVECT_1: 15

      .= ( <;v, v;> - <;v, v;>) by ThSc5

      .= 0 ;

      

      thus <;( 0. L), v;> = <;(v - v), v;> by RLVECT_1: 15

      .= ( <;v, v;> - <;v, v;>) by ThSc5

      .= 0 ;

    end;

    definition

      let IT be Z_Lattice;

      :: ZMODLAT1:def5

      attr IT is INTegral means

      : defIntegral: for v,u be Vector of IT holds <;v, u;> in INT ;

    end

    registration

      cluster INTegral for Z_Lattice;

      correctness

      proof

        set V0 = the finite-rank free Z_Module;

        reconsider nilfunc = ( [:the carrier of ( (0). V0), the carrier of ( (0). V0):] --> 0 ) as Function of [:the carrier of ( (0). V0), the carrier of ( (0). V0):], the carrier of F_Real by FUNCOP_1: 45;

        set X0 = ( GenLat (( (0). V0),nilfunc));

        reconsider X0 as finite-rank free Abelian add-associative right_zeroed right_complementable scalar-distributive vector-distributive scalar-associative scalar-unital non empty LatticeStr over INT.Ring ;

        reconsider X0 as Z_Lattice by ThTrivialLat1;

        take X0;

        thus thesis by INT_1:def 2;

      end;

    end

    registration

      let L be INTegral Z_Lattice;

      let v,u be Vector of L;

      cluster <;v, u;> -> integer;

      correctness by defIntegral, INT_1:def 2;

    end

    registration

      let L be INTegral Z_Lattice;

      let v be Vector of L;

      cluster ||.v.|| -> integer;

      correctness ;

    end

    theorem :: ZMODLAT1:13

    

     ThIntLat1B: for L be Z_Lattice, I be finite Subset of L, u be Vector of L st for v be Vector of L st v in I holds <;v, u;> in INT holds for v be Vector of L st v in ( Lin I) holds <;v, u;> in INT

    proof

      let L be Z_Lattice, I be finite Subset of L, u be Vector of L;

      assume

       AS: for v be Vector of L st v in I holds <;v, u;> in INT ;

      defpred P[ Nat] means for I be finite Subset of L st ( card I) = $1 & for v be Vector of L st v in I holds <;v, u;> in INT holds for v be Vector of L st v in ( Lin I) holds <;v, u;> in INT ;

      

       P1: P[ 0 ]

      proof

        let I be finite Subset of L;

        assume ( card I) = 0 & for v be Vector of L st v in I holds <;v, u;> in INT ;

        then I = ( {} the carrier of L);

        then

         A2: ( Lin I) = ( (0). L) by ZMODUL02: 67;

        let v be Vector of L;

        assume v in ( Lin I);

        then v in {( 0. L)} by A2, VECTSP_4:def 3;

        then v = ( 0. L) by TARSKI:def 1;

        then <;v, u;> = 0 by ThSc6;

        hence <;v, u;> in INT ;

      end;

      

       P2: for n be Nat st P[n] holds P[(n + 1)]

      proof

        let n be Nat;

        assume

         A0: P[n];

        thus P[(n + 1)]

        proof

          let I be finite Subset of L;

          assume

           A1: ( card I) = (n + 1) & for v be Vector of L st v in I holds <;v, u;> in INT ;

          then I <> {} ;

          then

          consider v be object such that

           A3: v in I by XBOOLE_0:def 1;

          reconsider v as Vector of L by A3;

          ((I \ {v}) \/ {v}) = (I \/ {v}) by XBOOLE_1: 39

          .= I by A3, ZFMISC_1: 40;

          then

           A4: ( Lin I) = (( Lin (I \ {v})) + ( Lin {v})) by ZMODUL02: 72;

          

           A5: ( card (I \ {v})) = (( card I) - ( card {v})) by A3, CARD_2: 44, ZFMISC_1: 31

          .= (( card I) - 1) by CARD_1: 30

          .= n by A1;

          reconsider J = (I \ {v}) as finite Subset of L;

          

           B8: for x be Vector of L st x in J holds <;x, u;> in INT

          proof

            let x be Vector of L;

            assume x in J;

            then x in I by XBOOLE_1: 36, TARSKI:def 3;

            hence <;x, u;> in INT by A1;

          end;

          thus for x be Vector of L st x in ( Lin I) holds <;x, u;> in INT

          proof

            let x be Vector of L;

            assume x in ( Lin I);

            then

            consider xu1,xu2 be Vector of L such that

             A10: xu1 in ( Lin (I \ {v})) & xu2 in ( Lin {v}) & x = (xu1 + xu2) by A4, ZMODUL01: 92;

            consider ixu2 be Element of INT.Ring such that

             A12: xu2 = (ixu2 * v) by A10, ZMODUL06: 19;

            

             B11: x = ((( 1. INT.Ring ) * xu1) + (ixu2 * v)) by A10, A12, VECTSP_1:def 17;

            set i1 = ( 1. INT.Ring );

            

             B13: <;x, u;> = ((i1 * <;xu1, u;>) + (ixu2 * <;v, u;>)) by B11, ThSc4;

            

             B14: <;xu1, u;> in INT by A0, A5, B8, A10;

             <;v, u;> in INT by A1, A3;

            hence <;x, u;> in INT by B13, B14, INT_1:def 2;

          end;

        end;

      end;

      

       X1: for n be Nat holds P[n] from NAT_1:sch 2( P1, P2);

      ( card I) is Nat;

      hence thesis by X1, AS;

    end;

    theorem :: ZMODLAT1:14

    

     ThIntLat1A: for L be Z_Lattice, I be Basis of L st for v,u be Vector of L st v in I & u in I holds <;v, u;> in INT holds for v,u be Vector of L holds <;v, u;> in INT

    proof

      let L be Z_Lattice;

      defpred P[ Nat] means for I be finite Subset of L st ( card I) = $1 & for v,u be Vector of L st v in I & u in I holds <;v, u;> in INT holds for v,u be Vector of L st v in ( Lin I) & u in ( Lin I) holds <;v, u;> in INT ;

      

       P1: P[ 0 ]

      proof

        let I be finite Subset of L;

        assume ( card I) = 0 & for v,u be Vector of L st v in I & u in I holds <;v, u;> in INT ;

        then I = ( {} the carrier of L);

        then

         A2: ( Lin I) = ( (0). L) by ZMODUL02: 67;

        let v,u be Vector of L;

        assume v in ( Lin I) & u in ( Lin I);

        then v in {( 0. L)} & u in {( 0. L)} by A2, VECTSP_4:def 3;

        then v = ( 0. L) & u = ( 0. L) by TARSKI:def 1;

        then <;v, u;> = 0 by ThSc6;

        hence <;v, u;> in INT ;

      end;

      

       P2: for n be Nat st P[n] holds P[(n + 1)]

      proof

        let n be Nat;

        assume

         A0: P[n];

        thus P[(n + 1)]

        proof

          let I be finite Subset of L;

          assume

           A1: ( card I) = (n + 1) & for v,u be Vector of L st v in I & u in I holds <;v, u;> in INT ;

          then I <> {} ;

          then

          consider v be object such that

           A3: v in I by XBOOLE_0:def 1;

          reconsider v as Vector of L by A3;

          ((I \ {v}) \/ {v}) = (I \/ {v}) by XBOOLE_1: 39

          .= I by A3, ZFMISC_1: 40;

          then

           A4: ( Lin I) = (( Lin (I \ {v})) + ( Lin {v})) by ZMODUL02: 72;

          

           A5: ( card (I \ {v})) = (( card I) - ( card {v})) by A3, CARD_2: 44, ZFMISC_1: 31

          .= (( card I) - 1) by CARD_1: 30

          .= n by A1;

          reconsider J = (I \ {v}) as finite Subset of L;

          

           B8: for x,y be Vector of L st x in J & y in J holds <;x, y;> in INT

          proof

            let x,y be Vector of L;

            assume x in J & y in J;

            then x in I & y in I by XBOOLE_1: 36, TARSKI:def 3;

            hence <;x, y;> in INT by A1;

          end;

          

           A6X: for x be Vector of L st x in J holds <;x, v;> in INT

          proof

            let x be Vector of L;

            assume x in J;

            then x in I & v in I by A3, XBOOLE_1: 36, TARSKI:def 3;

            hence <;x, v;> in INT by A1;

          end;

          thus for x,y be Vector of L st x in ( Lin I) & y in ( Lin I) holds <;x, y;> in INT

          proof

            let x,y be Vector of L;

            assume

             A9: x in ( Lin I) & y in ( Lin I);

            then

            consider xu1,xu2 be Vector of L such that

             A10: xu1 in ( Lin (I \ {v})) & xu2 in ( Lin {v}) & x = (xu1 + xu2) by A4, ZMODUL01: 92;

            consider yu1,yu2 be Vector of L such that

             A11: yu1 in ( Lin (I \ {v})) & yu2 in ( Lin {v}) & y = (yu1 + yu2) by A9, A4, ZMODUL01: 92;

            consider ixu2 be Element of INT.Ring such that

             A12: xu2 = (ixu2 * v) by A10, ZMODUL06: 19;

            consider iyu2 be Element of INT.Ring such that

             A13: yu2 = (iyu2 * v) by A11, ZMODUL06: 19;

            

             B11: x = ((( 1. INT.Ring ) * xu1) + (ixu2 * v)) by A10, A12, VECTSP_1:def 17;

            set i1 = ( 1. INT.Ring );

            

             B13: <;x, y;> = ( <;((i1 * xu1) + (ixu2 * v)), yu1;> + <;((i1 * xu1) + (ixu2 * v)), (iyu2 * v);>) by A11, A13, B11, ThSc2

            .= (((i1 * <;xu1, yu1;>) + (ixu2 * <;v, yu1;>)) + <;((i1 * xu1) + (ixu2 * v)), (iyu2 * v);>) by ThSc4

            .= (((i1 * <;xu1, yu1;>) + (ixu2 * <;v, yu1;>)) + ((i1 * <;xu1, (iyu2 * v);>) + (ixu2 * <;v, (iyu2 * v);>))) by ThSc4

            .= ((( <;xu1, yu1;> + (ixu2 * <;v, yu1;>)) + <;xu1, (iyu2 * v);>) + (ixu2 * <;v, (iyu2 * v);>))

            .= ((( <;xu1, yu1;> + (ixu2 * <;v, yu1;>)) + <;xu1, (iyu2 * v);>) + (ixu2 * (iyu2 * <;v, v;>))) by ThSc3

            .= ((( <;xu1, yu1;> + (ixu2 * <;v, yu1;>)) + (iyu2 * <;xu1, v;>)) + ((ixu2 * iyu2) * <;v, v;>)) by ThSc3;

            

             B14: <;xu1, yu1;> in INT by A0, A5, B8, A10, A11;

             <;yu1, v;> in INT by A11, A6X, ThIntLat1B;

            then

             B15: <;v, yu1;> in INT by defZLattice;

            

             B16: <;xu1, v;> in INT by A10, A6X, ThIntLat1B;

             <;v, v;> in INT by A3, A1;

            hence <;x, y;> in INT by B13, B14, B15, B16, INT_1:def 2;

          end;

        end;

      end;

      

       X1: for n be Nat holds P[n] from NAT_1:sch 2( P1, P2);

      let I be Basis of L;

      assume

       X2: for v,u be Vector of L st v in I & u in I holds <;v, u;> in INT ;

      

       X3: I is linearly-independent & ( Lin I) = the ModuleStr of L by VECTSP_7:def 3;

      

       X4: ( card I) is Nat;

      let v,u be Vector of L;

      v in ( Lin I) & u in ( Lin I) by X3;

      hence <;v, u;> in INT by X1, X2, X4;

    end;

    theorem :: ZMODLAT1:15

    for L be Z_Lattice, I be Basis of L st for v,u be Vector of L st v in I & u in I holds <;v, u;> in INT holds L is INTegral by ThIntLat1A;

    definition

      let IT be Z_Lattice;

      :: ZMODLAT1:def6

      attr IT is positive-definite means

      : defPositive: for v be Vector of IT st v <> ( 0. IT) holds ||.v.|| > 0 ;

    end

    registration

      cluster non trivial INTegral positive-definite for Z_Lattice;

      correctness

      proof

        set V = the non trivial torsion-free Z_Module;

        set v = the non zero Vector of V;

        set Z = ( Lin {v});

        defpred P[ object, object] means ex a,b be Element of INT.Ring st $1 = [(a * v), (b * v)] & $2 = (a * b);

        

         A1: for x be Element of [:the carrier of Z, the carrier of Z:] holds ex y be Element of the carrier of F_Real st P[x, y]

        proof

          let x be Element of [:the carrier of Z, the carrier of Z:];

          consider x1,x2 be object such that

           B1: x1 in the carrier of Z & x2 in the carrier of Z & x = [x1, x2] by ZFMISC_1:def 2;

          reconsider x1, x2 as Vector of Z by B1;

          x1 in ( Lin {v});

          then

          consider i1 be Element of INT.Ring such that

           B2: x1 = (i1 * v) by ZMODUL06: 19;

          x2 in ( Lin {v});

          then

          consider i2 be Element of INT.Ring such that

           B3: x2 = (i2 * v) by ZMODUL06: 19;

          reconsider i12 = (i1 * i2) as Element of INT ;

           INT c= the carrier of F_Real by NUMBERS: 5, XBOOLE_0:def 8;

          then

          reconsider i12 as Element of F_Real ;

          take i12;

          thus thesis by B1, B2, B3;

        end;

        consider f be Function of [:the carrier of Z, the carrier of Z:], the carrier of F_Real such that

         A2: for x be Element of [:the carrier of Z, the carrier of Z:] holds P[x, (f . x)] from FUNCT_2:sch 3( A1);

        

         A3: for a,b be Element of INT.Ring holds (f . [(a * v), (b * v)]) = (a * b)

        proof

          let a,b be Element of INT.Ring ;

          (a * v) in ( Lin {v}) & (b * v) in ( Lin {v}) by ZMODUL06: 21;

          then [(a * v), (b * v)] in [:the carrier of Z, the carrier of Z:] by ZFMISC_1: 87;

          then

          consider a0,b0 be Element of INT.Ring such that

           B1: [(a * v), (b * v)] = [(a0 * v), (b0 * v)] & (f . [(a * v), (b * v)]) = (a0 * b0) by A2;

          

           B2: v <> ( 0. V);

          (a * v) = (a0 * v) by B1, XTUPLE_0: 1;

          then

           B3: a = a0 by B2, ZMODUL01: 11;

          (b * v) = (b0 * v) by B1, XTUPLE_0: 1;

          hence thesis by B1, B2, B3, ZMODUL01: 11;

        end;

        set L = ( GenLat (Z,f));

        reconsider L as finite-rank free Abelian add-associative right_zeroed right_complementable scalar-distributive vector-distributive scalar-associative scalar-unital non empty LatticeStr over INT.Ring ;

        L is Z_Lattice-like

        proof

          thus for x be Vector of L st for y be Vector of L holds <;x, y;> = 0 holds x = ( 0. L)

          proof

            let x be Vector of L such that

             C1: for y be Vector of L holds <;x, y;> = 0 ;

            assume x <> ( 0. L);

            then

             C2: x <> ( 0. V) by ZMODUL01: 26;

            x in ( Lin {v});

            then

            consider ix be Element of INT.Ring such that

             C3: x = (ix * v) by ZMODUL06: 19;

            

             C4: ix <> 0 by C2, C3, ZMODUL01: 1;

             <;x, x;> = (ix * ix) by A3, C3;

            hence contradiction by C1, C4;

          end;

          thus for x,y be Vector of L holds <;x, y;> = <;y, x;>

          proof

            let x,y be Vector of L;

            

             C1: x in ( Lin {v}) & y in ( Lin {v});

            then

            consider ix be Element of INT.Ring such that

             C2: x = (ix * v) by ZMODUL06: 19;

            consider iy be Element of INT.Ring such that

             C3: y = (iy * v) by C1, ZMODUL06: 19;

            

            thus <;x, y;> = (ix * iy) by A3, C2, C3

            .= <;y, x;> by A3, C2, C3;

          end;

          thus for x,y,z be Vector of L, a be Element of INT.Ring holds <;(x + y), z;> = ( <;x, z;> + <;y, z;>) & <;(a * x), y;> = (a * <;x, y;>)

          proof

            let x,y,z be Vector of L, a be Element of INT.Ring ;

            

             C1: x in ( Lin {v}) & y in ( Lin {v}) & z in ( Lin {v});

            then

            consider ix be Element of INT.Ring such that

             C2: x = (ix * v) by ZMODUL06: 19;

            consider iy be Element of INT.Ring such that

             C3: y = (iy * v) by C1, ZMODUL06: 19;

            consider iz be Element of INT.Ring such that

             C4: z = (iz * v) by C1, ZMODUL06: 19;

            (ix * v) in ( Lin {v}) by ZMODUL06: 21;

            then

            reconsider iixv = (ix * v) as Vector of Z;

            reconsider ixv = (ix * v) as Vector of V;

            (iy * v) in ( Lin {v}) by ZMODUL06: 21;

            then

            reconsider iiyv = (iy * v) as Vector of Z;

            reconsider iyv = (iy * v) as Vector of V;

            

             C5: (x + y) = (iixv + iiyv) by C2, C3

            .= (ixv + iyv) by ZMODUL01: 28

            .= ((ix + iy) * v) by VECTSP_1:def 15;

            

             C6: (a * x) = (a * iixv) by C2

            .= (a * ixv) by ZMODUL01: 29

            .= ((a * ix) * v) by VECTSP_1:def 16;

            

            thus <;(x + y), z;> = ((ix + iy) * iz) by A3, C4, C5

            .= ((ix * iz) + (iy * iz))

            .= ((f . [x, z]) + (iy * iz)) by A3, C2, C4

            .= ( <;x, z;> + <;y, z;>) by A3, C3, C4;

            

            thus <;(a * x), y;> = ((a * ix) * iy) by A3, C3, C6

            .= (a * (ix * iy))

            .= (a * <;x, y;>) by A3, C2, C3;

          end;

        end;

        then

        reconsider L as Z_Lattice;

        

         A4: for u be Vector of L st u <> ( 0. L) holds ||.u.|| > 0

        proof

          let u be Vector of L such that

           B1: u <> ( 0. L);

          

           B2: u <> ( 0. V) by B1, ZMODUL01: 26;

          u in ( Lin {v});

          then

          consider iu be Element of INT.Ring such that

           B4: u = (iu * v) by ZMODUL06: 19;

          

           B5: iu <> 0 by B2, B4, ZMODUL01: 1;

           ||.u.|| = (iu * iu) by A3, B4;

          hence thesis by B5, XREAL_1: 63;

        end;

        take L;

        

         A5: L is non trivial

        proof

          assume

           B1: L is trivial;

          v in ( Lin {v}) by ZMODUL06: 20;

          then

           B2: v = ( 0. L) by B1;

          v <> ( 0. V);

          hence contradiction by B2, ZMODUL01: 26;

        end;

        for w,u be Vector of L holds <;w, u;> in INT

        proof

          let w,u be Vector of L;

          w in ( Lin {v});

          then

          consider iw be Element of INT.Ring such that

           B1: w = (iw * v) by ZMODUL06: 19;

          u in ( Lin {v});

          then

          consider iu be Element of INT.Ring such that

           B2: u = (iu * v) by ZMODUL06: 19;

           <;w, u;> = (iw * iu) by A3, B1, B2;

          hence thesis;

        end;

        hence thesis by A4, A5;

      end;

    end

    theorem :: ZMODLAT1:16

    for L be positive-definite Z_Lattice, v be Vector of L holds ||.v.|| = 0 iff v = ( 0. L) by ThSc6, defPositive;

    theorem :: ZMODLAT1:17

    for L be positive-definite Z_Lattice, v be Vector of L holds ||.v.|| >= 0

    proof

      let L be positive-definite Z_Lattice, v be Vector of L;

      per cases ;

        suppose v = ( 0. L);

        hence thesis by ThSc6;

      end;

        suppose v <> ( 0. L);

        hence thesis by defPositive;

      end;

    end;

    definition

      let IT be INTegral Z_Lattice;

      :: ZMODLAT1:def7

      attr IT is even means for v be Vector of IT holds ||.v.|| is even;

    end

    registration

      cluster even for INTegral Z_Lattice;

      correctness

      proof

        set V0 = the finite-rank free Z_Module;

        reconsider nilfunc = ( [:the carrier of ( (0). V0), the carrier of ( (0). V0):] --> 0 ) as Function of [:the carrier of ( (0). V0), the carrier of ( (0). V0):], the carrier of F_Real by FUNCOP_1: 45;

        set X0 = ( GenLat (( (0). V0),nilfunc));

        reconsider X0 as finite-rank free Abelian add-associative right_zeroed right_complementable scalar-distributive vector-distributive scalar-associative scalar-unital non empty LatticeStr over INT.Ring ;

        reconsider X0 as Z_Lattice by ThTrivialLat1;

        X0 is INTegral by INT_1:def 2;

        then

        reconsider X0 as INTegral Z_Lattice;

        take X0;

        thus thesis by FUNCOP_1: 7;

      end;

    end

    notation

      let L be Z_Lattice;

      synonym dim (L) for rank (L);

    end

    definition

      let L be Z_Lattice;

      let v,u be Vector of L;

      :: ZMODLAT1:def8

      pred v,u are_orthogonal means <;v, u;> = 0 ;

      symmetry by defZLattice;

    end

    theorem :: ZMODLAT1:18

    for L be Z_Lattice, v,u be Vector of L holds (v,u) are_orthogonal implies (v,( - u)) are_orthogonal & (( - v),u) are_orthogonal & (( - v),( - u)) are_orthogonal

    proof

      let L be Z_Lattice, v,u be Vector of L;

      assume

       A1: (v,u) are_orthogonal ;

       <;v, ( - u);> = ( - <;v, u;>) by ThSc1

      .= 0 by A1;

      hence (v,( - u)) are_orthogonal ;

      

       A2: <;( - v), u;> = ( - <;v, u;>) by ThSc1

      .= 0 by A1;

      hence (( - v),u) are_orthogonal ;

       <;( - v), ( - u);> = ( - <;( - v), u;>) by ThSc1

      .= 0 by A2;

      hence (( - v),( - u)) are_orthogonal ;

    end;

    theorem :: ZMODLAT1:19

    for L be Z_Lattice, v,u be Vector of L holds (v,u) are_orthogonal implies ||.(v + u).|| = ( ||.v.|| + ||.u.||)

    proof

      let L be Z_Lattice, v,u be Vector of L;

      assume

       A1: (v,u) are_orthogonal ;

      

      thus ||.(v + u).|| = ( <;v, (v + u);> + <;u, (v + u);>) by defZLattice

      .= (( <;v, v;> + <;v, u;>) + <;u, (v + u);>) by ThSc2

      .= (( <;v, v;> + 0 ) + ( <;u, v;> + <;u, u;>)) by A1, ThSc2

      .= ( <;v, v;> + ( 0 + <;u, u;>)) by A1, defZLattice

      .= ( ||.v.|| + ||.u.||);

    end;

    theorem :: ZMODLAT1:20

    for L be Z_Lattice, v,u be Vector of L holds (v,u) are_orthogonal implies ||.(v - u).|| = ( ||.v.|| + ||.u.||)

    proof

      let L be Z_Lattice, v,u be Vector of L;

      assume

       A1: (v,u) are_orthogonal ;

      

      thus ||.(v - u).|| = ( <;v, (v - u);> - <;u, (v - u);>) by ThSc5

      .= (( <;v, v;> - <;v, u;>) - <;u, (v - u);>) by ThSc5

      .= (( <;v, v;> - 0 ) - ( <;u, v;> - <;u, u;>)) by A1, ThSc5

      .= ( <;v, v;> - ( 0 - <;u, u;>)) by A1, defZLattice

      .= ( ||.v.|| + ||.u.||);

    end;

    definition

      let L be Z_Lattice;

      :: ZMODLAT1:def9

      mode Z_Sublattice of L -> Z_Lattice means

      : defSublattice: the carrier of it c= the carrier of L & ( 0. it ) = ( 0. L) & the addF of it = (the addF of L || the carrier of it ) & the lmult of it = (the lmult of L | [:the carrier of INT.Ring , the carrier of it :]) & the scalar of it = (the scalar of L || the carrier of it );

      existence

      proof

        take L;

        thus thesis;

      end;

    end

    theorem :: ZMODLAT1:21

    

     ThSL1: for L be Z_Lattice, L1 be Z_Sublattice of L holds L1 is Submodule of L

    proof

      let L be Z_Lattice, L1 be Z_Sublattice of L;

      

       A1: the carrier of L1 c= the carrier of L by defSublattice;

      

       A2: the addF of L1 = (the addF of L || the carrier of L1) by defSublattice;

      

       A3: ( 0. L1) = ( 0. L) by defSublattice;

      the lmult of L1 = (the lmult of L | [:the carrier of INT.Ring , the carrier of L1:]) by defSublattice;

      hence thesis by A1, A2, A3, VECTSP_4:def 2;

    end;

    theorem :: ZMODLAT1:22

    for x be object, L be Z_Lattice, L1,L2 be Z_Sublattice of L holds x in L1 & L1 is Z_Sublattice of L2 implies x in L2

    proof

      let x be object, L be Z_Lattice, L1,L2 be Z_Sublattice of L;

      assume

       AS: x in L1 & L1 is Z_Sublattice of L2;

      then

       A1: L1 is Submodule of L2 by ThSL1;

      L1 is Submodule of L & L2 is Submodule of L by ThSL1;

      hence thesis by AS, A1, ZMODUL01: 23;

    end;

    theorem :: ZMODLAT1:23

    for x be object, L be Z_Lattice, L1 be Z_Sublattice of L holds x in L1 implies x in L

    proof

      let x be object, L be Z_Lattice, L1 be Z_Sublattice of L;

      

       A1: L1 is Submodule of L by ThSL1;

      assume x in L1;

      hence thesis by A1, ZMODUL01: 24;

    end;

    theorem :: ZMODLAT1:24

    

     ThSL4: for L be Z_Lattice, L1 be Z_Sublattice of L, w be Vector of L1 holds w is Vector of L

    proof

      let L be Z_Lattice, L1 be Z_Sublattice of L, w be Vector of L1;

      L1 is Submodule of L by ThSL1;

      hence thesis by ZMODUL01: 25;

    end;

    theorem :: ZMODLAT1:25

    for L be Z_Lattice, L1,L2 be Z_Sublattice of L holds ( 0. L1) = ( 0. L2)

    proof

      let L be Z_Lattice, L1,L2 be Z_Sublattice of L;

      

      thus ( 0. L1) = ( 0. L) by defSublattice

      .= ( 0. L2) by defSublattice;

    end;

    theorem :: ZMODLAT1:26

    for L be Z_Lattice, L1 be Z_Sublattice of L, v1,v2 be Vector of L, w1,w2 be Vector of L1 holds w1 = v1 & w2 = v2 implies (w1 + w2) = (v1 + v2)

    proof

      let L be Z_Lattice, L1 be Z_Sublattice of L, v1,v2 be Vector of L, w1,w2 be Vector of L1;

      assume

       AS: w1 = v1 & w2 = v2;

      L1 is Submodule of L by ThSL1;

      hence thesis by AS, ZMODUL01: 28;

    end;

    theorem :: ZMODLAT1:27

    for L be Z_Lattice, L1 be Z_Sublattice of L, v be Vector of L, w be Vector of L1, a be Element of INT.Ring holds w = v implies (a * w) = (a * v)

    proof

      let L be Z_Lattice, L1 be Z_Sublattice of L, v be Vector of L, w be Vector of L1, a be Element of INT.Ring ;

      assume

       AS: w = v;

      L1 is Submodule of L by ThSL1;

      hence thesis by AS, ZMODUL01: 29;

    end;

    theorem :: ZMODLAT1:28

    for L be Z_Lattice, L1 be Z_Sublattice of L, v be Vector of L, w be Vector of L1 holds w = v implies ( - w) = ( - v)

    proof

      let L be Z_Lattice, L1 be Z_Sublattice of L, v be Vector of L, w be Vector of L1;

      assume

       AS: w = v;

      L1 is Submodule of L by ThSL1;

      hence thesis by AS, ZMODUL01: 30;

    end;

    theorem :: ZMODLAT1:29

    for L be Z_Lattice, L1 be Z_Sublattice of L, v1,v2 be Vector of L, w1,w2 be Vector of L1 holds w1 = v1 & w2 = v2 implies (w1 - w2) = (v1 - v2)

    proof

      let L be Z_Lattice, L1 be Z_Sublattice of L, v1,v2 be Vector of L, w1,w2 be Vector of L1;

      assume

       AS: w1 = v1 & w2 = v2;

      L1 is Submodule of L by ThSL1;

      hence thesis by AS, ZMODUL01: 31;

    end;

    theorem :: ZMODLAT1:30

    for L be Z_Lattice, L1 be Z_Sublattice of L holds ( 0. L) in L1

    proof

      let L be Z_Lattice, L1 be Z_Sublattice of L;

      L1 is Submodule of L by ThSL1;

      hence thesis by ZMODUL01: 33;

    end;

    theorem :: ZMODLAT1:31

    for L be Z_Lattice, L1,L2 be Z_Sublattice of L holds ( 0. L1) in L2

    proof

      let L be Z_Lattice, L1,L2 be Z_Sublattice of L;

      L1 is Submodule of L & L2 is Submodule of L by ThSL1;

      hence thesis by ZMODUL01: 34;

    end;

    theorem :: ZMODLAT1:32

    for L be Z_Lattice, L1 be Z_Sublattice of L holds ( 0. L1) in L

    proof

      let L be Z_Lattice, L1 be Z_Sublattice of L;

      L1 is Submodule of L by ThSL1;

      hence thesis by ZMODUL01: 35;

    end;

    theorem :: ZMODLAT1:33

    for L be Z_Lattice, L1 be Z_Sublattice of L, v1,v2 be Vector of L holds v1 in L1 & v2 in L1 implies (v1 + v2) in L1

    proof

      let L be Z_Lattice, L1 be Z_Sublattice of L, v1,v2 be Vector of L;

      assume

       AS: v1 in L1 & v2 in L1;

      L1 is Submodule of L by ThSL1;

      hence thesis by AS, ZMODUL01: 36;

    end;

    theorem :: ZMODLAT1:34

    for L be Z_Lattice, L1 be Z_Sublattice of L, v be Vector of L, a be Element of INT.Ring holds v in L1 implies (a * v) in L1

    proof

      let L be Z_Lattice, L1 be Z_Sublattice of L, v be Vector of L, a be Element of INT.Ring ;

      assume

       AS: v in L1;

      L1 is Submodule of L by ThSL1;

      hence thesis by AS, ZMODUL01: 37;

    end;

    theorem :: ZMODLAT1:35

    for L be Z_Lattice, L1 be Z_Sublattice of L, v be Vector of L holds v in L1 implies ( - v) in L1

    proof

      let L be Z_Lattice, L1 be Z_Sublattice of L, v be Vector of L;

      assume

       AS: v in L1;

      L1 is Submodule of L by ThSL1;

      hence thesis by AS, ZMODUL01: 38;

    end;

    theorem :: ZMODLAT1:36

    for L be Z_Lattice, L1 be Z_Sublattice of L, v1,v2 be Vector of L holds v1 in L1 & v2 in L1 implies (v1 - v2) in L1

    proof

      let L be Z_Lattice, L1 be Z_Sublattice of L, v1,v2 be Vector of L;

      assume

       AS: v1 in L1 & v2 in L1;

      L1 is Submodule of L by ThSL1;

      hence thesis by AS, ZMODUL01: 39;

    end;

    theorem :: ZMODLAT1:37

    for L be positive-definite Z_Lattice, A be non empty set, ze be Element of A, ad be BinOp of A, mu be Function of [:the carrier of INT.Ring , A:], A, sc be Function of [:A, A:], the carrier of F_Real st A is linearly-closed Subset of L & ze = ( 0. L) & ad = (the addF of L || A) & mu = (the lmult of L | [:the carrier of INT.Ring , A:]) & sc = (the scalar of L || A) holds LatticeStr (# A, ad, ze, mu, sc #) is Z_Sublattice of L

    proof

      let L be positive-definite Z_Lattice, A be non empty set, ze be Element of A, ad be BinOp of A, mu be Function of [:the carrier of INT.Ring , A:], A, sc be Function of [:A, A:], the carrier of F_Real such that

       A1: A is linearly-closed Subset of L & ze = ( 0. L) & ad = (the addF of L || A) & mu = (the lmult of L | [:the carrier of INT.Ring , A:]) & sc = (the scalar of L || A);

      set L1 = LatticeStr (# A, ad, ze, mu, sc #);

      set V1 = ModuleStr (# A, ad, ze, mu #);

      reconsider V1 as Submodule of L by A1, ZMODUL01: 40;

      

       AY3: A = the carrier of V1 & ze = ( 0. V1) & ad = the addF of V1 & mu = the lmult of V1;

      reconsider scc = sc as Function of [:the carrier of V1, the carrier of V1:], the carrier of F_Real ;

      

       AA: L1 = ( GenLat (V1,scc));

      then

       A3: L1 is Submodule of V1 by LmZMtoZL1;

      reconsider L1 as Abelian add-associative right_zeroed right_complementable scalar-distributive vector-distributive scalar-associative scalar-unital non empty LatticeStr over INT.Ring by AA;

      reconsider L1 as free Abelian add-associative right_zeroed right_complementable scalar-distributive vector-distributive scalar-associative scalar-unital non empty LatticeStr over INT.Ring by AA;

      

       AX3: L1 is Submodule of L by A3, ZMODUL01: 42;

      L1 is Z_Lattice-like

      proof

        thus for x be Vector of L1 st for y be Vector of L1 holds <;x, y;> = 0 holds x = ( 0. L1)

        proof

          let x be Vector of L1 such that

           B1: for y be Vector of L1 holds <;x, y;> = 0 ;

          reconsider xx = x as Vector of L by AY3, ZMODUL01: 25;

          assume x <> ( 0. L1);

          then ||.xx.|| <> 0 by A1, defPositive;

          then <;x, x;> <> 0 by A1, FUNCT_1: 49;

          hence contradiction by B1;

        end;

        thus for x,y be Vector of L1 holds <;x, y;> = <;y, x;>

        proof

          let x,y be Vector of L1;

          reconsider xx = x, yy = y as Vector of L by AY3, ZMODUL01: 25;

          

          thus <;x, y;> = <;xx, yy;> by A1, FUNCT_1: 49

          .= <;yy, xx;> by defZLattice

          .= <;y, x;> by A1, FUNCT_1: 49;

        end;

        thus for x,y,z be Vector of L1, a be Element of INT.Ring holds <;(x + y), z;> = ( <;x, z;> + <;y, z;>) & <;(a * x), y;> = (a * <;x, y;>)

        proof

          let x,y,z be Vector of L1, a be Element of INT.Ring ;

          reconsider xx = x, yy = y, zz = z as Vector of L by AY3, ZMODUL01: 25;

          (xx + yy) = (x + y) by AX3, ZMODUL01: 28;

          

          hence <;(x + y), z;> = <;(xx + yy), zz;> by A1, FUNCT_1: 49

          .= ( <;xx, zz;> + <;yy, zz;>) by defZLattice

          .= ( <;x, z;> + <;yy, zz;>) by A1, FUNCT_1: 49

          .= ( <;x, z;> + <;y, z;>) by A1, FUNCT_1: 49;

          (a * xx) = (a * x) by AX3, ZMODUL01: 29;

          

          hence <;(a * x), y;> = <;(a * xx), yy;> by A1, FUNCT_1: 49

          .= (a * <;xx, yy;>) by defZLattice

          .= (a * <;x, y;>) by A1, FUNCT_1: 49;

        end;

      end;

      hence thesis by A1, defSublattice, AA;

    end;

    theorem :: ZMODLAT1:38

    

     ThSL18: for L be Z_Lattice, L1 be Z_Sublattice of L, w1,w2 be Vector of L1, v1,v2 be Vector of L st w1 = v1 & w2 = v2 holds <;w1, w2;> = <;v1, v2;>

    proof

      let L be Z_Lattice, L1 be Z_Sublattice of L, w1,w2 be Vector of L1, v1,v2 be Vector of L such that

       B1: w1 = v1 & w2 = v2;

      

       B2: [w1, w2] in [:the carrier of L1, the carrier of L1:];

      

      thus <;w1, w2;> = ((the scalar of L || the carrier of L1) . (w1,w2)) by defSublattice

      .= <;v1, v2;> by B1, B2, FUNCT_1: 49;

    end;

    registration

      let L be INTegral Z_Lattice;

      cluster -> INTegral for Z_Sublattice of L;

      correctness

      proof

        let L1 be Z_Sublattice of L;

        thus for w1,w2 be Vector of L1 holds <;w1, w2;> in INT

        proof

          let w1,w2 be Vector of L1;

          reconsider v1 = w1, v2 = w2 as Vector of L by ThSL4;

           <;w1, w2;> = <;v1, v2;> by ThSL18;

          hence thesis by defIntegral;

        end;

      end;

    end

    registration

      let L be positive-definite Z_Lattice;

      cluster -> positive-definite for Z_Sublattice of L;

      correctness

      proof

        let L1 be Z_Sublattice of L;

        thus for w be Vector of L1 st w <> ( 0. L1) holds ||.w.|| > 0

        proof

          let w be Vector of L1 such that

           A1: w <> ( 0. L1);

          reconsider v = w as Vector of L by ThSL4;

          v <> ( 0. L) by A1, defSublattice;

          then ||.v.|| > 0 by defPositive;

          hence thesis by ThSL18;

        end;

      end;

    end

    definition

      let V,W be ModuleStr over INT.Ring ;

      mode FrForm of V,W is Function of [:the carrier of V, the carrier of W:], the carrier of F_Real ;

    end

    definition

      let V,W be ModuleStr over INT.Ring ;

      :: ZMODLAT1:def10

      func NulFrForm (V,W) -> FrForm of V, W equals ( [:the carrier of V, the carrier of W:] --> ( 0. F_Real ));

      coherence ;

    end

    definition

      let V,W be non empty ModuleStr over INT.Ring ;

      let f,g be FrForm of V, W;

      :: ZMODLAT1:def11

      func f + g -> FrForm of V, W means

      : Def2: for v be Vector of V, w be Vector of W holds (it . (v,w)) = ((f . (v,w)) + (g . (v,w)));

      existence

      proof

        set K = F_Real ;

        set X = the carrier of V, Y = the carrier of W, Z = the carrier of F_Real ;

        deffunc F( Element of X, Element of Y) = ((f . ($1,$2)) + (g . ($1,$2)));

        consider ff be Function of [:X, Y:], Z such that

         A1: for x be Element of X, y be Element of Y holds (ff . (x,y)) = F(x,y) from BINOP_1:sch 4;

        reconsider ff as FrForm of V, W;

        take ff;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let F,G be FrForm of V, W such that

         A2: for v be Vector of V, w be Vector of W holds (F . (v,w)) = ((f . (v,w)) + (g . (v,w))) and

         A3: for v be Vector of V, w be Vector of W holds (G . (v,w)) = ((f . (v,w)) + (g . (v,w)));

        now

          let v be Vector of V, w be Vector of W;

          

          thus (F . (v,w)) = ((f . (v,w)) + (g . (v,w))) by A2

          .= (G . (v,w)) by A3;

        end;

        hence thesis;

      end;

    end

    definition

      let V,W be non empty ModuleStr over INT.Ring ;

      let f be FrForm of V, W;

      let a be Element of F_Real ;

      :: ZMODLAT1:def12

      func a * f -> FrForm of V, W means

      : Def3: for v be Vector of V, w be Vector of W holds (it . (v,w)) = (a * (f . (v,w)));

      existence

      proof

        set K = F_Real ;

        set X = the carrier of V, Y = the carrier of W, Z = the carrier of F_Real ;

        deffunc F( Element of X, Element of Y) = (( In (a,the carrier of F_Real )) * (f . ($1,$2)));

        consider ff be Function of [:X, Y:], Z such that

         A1: for x be Element of X, y be Element of Y holds (ff . (x,y)) = F(x,y) from BINOP_1:sch 4;

        reconsider ff as FrForm of V, W;

        take ff;

        thus for v be Vector of V, w be Vector of W holds (ff . (v,w)) = (a * (f . (v,w))) by A1;

      end;

      uniqueness

      proof

        let F,G be FrForm of V, W such that

         A2: for v be Vector of V, w be Vector of W holds (F . (v,w)) = (a * (f . (v,w))) and

         A3: for v be Vector of V, w be Vector of W holds (G . (v,w)) = (a * (f . (v,w)));

        now

          let v be Vector of V, w be Vector of W;

          

          thus (F . (v,w)) = (a * (f . (v,w))) by A2

          .= (G . (v,w)) by A3;

        end;

        hence thesis;

      end;

    end

    definition

      let V,W be non empty ModuleStr over INT.Ring ;

      let f be FrForm of V, W;

      :: ZMODLAT1:def13

      func - f -> FrForm of V, W means

      : Def4: for v be Vector of V, w be Vector of W holds (it . (v,w)) = ( - (f . (v,w)));

      existence

      proof

        set K = F_Real ;

        set X = the carrier of V, Y = the carrier of W, Z = the carrier of K;

        deffunc F( Element of X, Element of Y) = ( - (f . ($1,$2)));

        consider ff be Function of [:X, Y:], Z such that

         A1: for x be Element of X, y be Element of Y holds (ff . (x,y)) = F(x,y) from BINOP_1:sch 4;

        reconsider ff as FrForm of V, W;

        take ff;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let F,G be FrForm of V, W such that

         A2: for v be Vector of V, w be Vector of W holds (F . (v,w)) = ( - (f . (v,w))) and

         A3: for v be Vector of V, w be Vector of W holds (G . (v,w)) = ( - (f . (v,w)));

        now

          let v be Vector of V, w be Vector of W;

          

          thus (F . (v,w)) = ( - (f . (v,w))) by A2

          .= (G . (v,w)) by A3;

        end;

        hence thesis;

      end;

    end

    definition

      let V,W be non empty ModuleStr over INT.Ring ;

      let f be FrForm of V, W;

      :: original: -

      redefine

      :: ZMODLAT1:def14

      func - f equals (( - ( 1. F_Real )) * f);

      compatibility

      proof

        let g be FrForm of V, W;

        thus g = ( - f) implies g = (( - ( 1. F_Real )) * f)

        proof

          assume

           A1: g = ( - f);

          now

            let v be Vector of V, w be Vector of W;

            

            thus (g . (v,w)) = ( - (f . (v,w))) by A1, Def4

            .= (( - ( 1. F_Real )) * (f . (v,w)))

            .= ((( - ( 1. F_Real )) * f) . (v,w)) by Def3;

          end;

          hence thesis;

        end;

        assume

         A2: g = (( - ( 1. F_Real )) * f);

        now

          let v be Vector of V, w be Vector of W;

          

          thus (g . (v,w)) = (( - ( 1. F_Real )) * (f . (v,w))) by A2, Def3

          .= ( - (f . (v,w)))

          .= (( - f) . (v,w)) by Def4;

        end;

        hence thesis;

      end;

    end

    definition

      let V,W be non empty ModuleStr over INT.Ring ;

      let f,g be FrForm of V, W;

      :: ZMODLAT1:def15

      func f - g -> FrForm of V, W equals (f + ( - g));

      correctness ;

    end

    definition

      let V,W be non empty ModuleStr over INT.Ring ;

      let f,g be FrForm of V, W;

      :: original: -

      redefine

      :: ZMODLAT1:def16

      func f - g means

      : Def7: for v be Vector of V, w be Vector of W holds (it . (v,w)) = ((f . (v,w)) - (g . (v,w)));

      compatibility

      proof

        let h be FrForm of V, W;

        thus h = (f - g) implies for v be Vector of V, w be Vector of W holds (h . (v,w)) = ((f . (v,w)) - (g . (v,w)))

        proof

          assume

           A1: h = (f - g);

          let v be Vector of V, w be Vector of W;

          

          thus (h . (v,w)) = ((f . (v,w)) + (( - g) . (v,w))) by A1, Def2

          .= ((f . (v,w)) - (g . (v,w))) by Def4;

        end;

        assume

         A2: for v be Vector of V, w be Vector of W holds (h . (v,w)) = ((f . (v,w)) - (g . (v,w)));

        now

          let v be Vector of V, w be Vector of W;

          

          thus (h . (v,w)) = ((f . (v,w)) - (g . (v,w))) by A2

          .= ((f . (v,w)) + (( - g) . (v,w))) by Def4

          .= ((f - g) . (v,w)) by Def2;

        end;

        hence thesis;

      end;

    end

    definition

      let V,W be non empty ModuleStr over INT.Ring ;

      let f,g be FrForm of V, W;

      :: original: +

      redefine

      func f + g;

      commutativity

      proof

        let f,g be FrForm of V, W;

        now

          let v be Vector of V, w be Vector of W;

          

          thus ((f + g) . (v,w)) = ((f . (v,w)) + (g . (v,w))) by Def2

          .= ((g + f) . (v,w)) by Def2;

        end;

        hence (f + g) = (g + f);

      end;

    end

    theorem :: ZMODLAT1:39

    for V,W be non empty ModuleStr over INT.Ring , f be FrForm of V, W holds (f + ( NulFrForm (V,W))) = f

    proof

      let V,W be non empty ModuleStr over INT.Ring , f be FrForm of V, W;

      set g = ( NulFrForm (V,W));

      now

        let v be Vector of V, w be Vector of W;

        

        thus ((f + g) . (v,w)) = ((f . (v,w)) + (g . (v,w))) by Def2

        .= ((f . (v,w)) + ( 0. INT.Ring )) by FUNCOP_1: 70

        .= (f . (v,w));

      end;

      hence thesis;

    end;

    theorem :: ZMODLAT1:40

    for V,W be non empty ModuleStr over INT.Ring , f,g,h be FrForm of V, W holds ((f + g) + h) = (f + (g + h))

    proof

      let V,W be non empty ModuleStr over INT.Ring , f,g,h be FrForm of V, W;

      now

        let v be Vector of V, w be Vector of W;

        

        thus (((f + g) + h) . (v,w)) = (((f + g) . (v,w)) + (h . (v,w))) by Def2

        .= (((f . (v,w)) + (g . (v,w))) + (h . (v,w))) by Def2

        .= ((f . (v,w)) + ((g . (v,w)) + (h . (v,w))))

        .= ((f . (v,w)) + ((g + h) . (v,w))) by Def2

        .= ((f + (g + h)) . (v,w)) by Def2;

      end;

      hence thesis;

    end;

    theorem :: ZMODLAT1:41

    for V,W be non empty ModuleStr over INT.Ring , f be FrForm of V, W holds (f - f) = ( NulFrForm (V,W))

    proof

      let V,W be non empty ModuleStr over INT.Ring , f be FrForm of V, W;

      now

        let v be Vector of V, w be Vector of W;

        

        thus ((f - f) . (v,w)) = ((f . (v,w)) - (f . (v,w))) by Def7

        .= (( NulFrForm (V,W)) . (v,w)) by FUNCOP_1: 70;

      end;

      hence thesis;

    end;

    theorem :: ZMODLAT1:42

    for V,W be non empty ModuleStr over INT.Ring , a be Element of F_Real , f,g be FrForm of V, W holds (a * (f + g)) = ((a * f) + (a * g))

    proof

      let V,W be non empty ModuleStr over INT.Ring , r be Element of F_Real , f,g be FrForm of V, W;

      now

        let v be Vector of V, w be Vector of W;

        

        thus ((r * (f + g)) . (v,w)) = (r * ((f + g) . (v,w))) by Def3

        .= (r * ((f . (v,w)) + (g . (v,w)))) by Def2

        .= ((r * (f . (v,w))) + (r * (g . (v,w))))

        .= (((r * f) . (v,w)) + (r * (g . (v,w)))) by Def3

        .= (((r * f) . (v,w)) + ((r * g) . (v,w))) by Def3

        .= (((r * f) + (r * g)) . (v,w)) by Def2;

      end;

      hence thesis;

    end;

    theorem :: ZMODLAT1:43

    for V,W be non empty ModuleStr over INT.Ring , a,b be Element of F_Real , f be FrForm of V, W holds ((a + b) * f) = ((a * f) + (b * f))

    proof

      let V,W be non empty ModuleStr over INT.Ring , r,s be Element of F_Real , f be FrForm of V, W;

      now

        let v be Vector of V, w be Vector of W;

        

        thus (((r + s) * f) . (v,w)) = ((r + s) * (f . (v,w))) by Def3

        .= ((r * (f . (v,w))) + (s * (f . (v,w))))

        .= (((r * f) . (v,w)) + (s * (f . (v,w)))) by Def3

        .= (((r * f) . (v,w)) + ((s * f) . (v,w))) by Def3

        .= (((r * f) + (s * f)) . (v,w)) by Def2;

      end;

      hence thesis;

    end;

    theorem :: ZMODLAT1:44

    for V,W be non empty ModuleStr over INT.Ring , a,b be Element of F_Real , f be FrForm of V, W holds ((a * b) * f) = (a * (b * f))

    proof

      let V,W be non empty ModuleStr over INT.Ring , r,s be Element of F_Real , f be FrForm of V, W;

      now

        let v be Vector of V, w be Vector of W;

        

        thus (((r * s) * f) . (v,w)) = ((r * s) * (f . (v,w))) by Def3

        .= (r * (s * (f . (v,w))))

        .= (r * ((s * f) . (v,w))) by Def3

        .= ((r * (s * f)) . (v,w)) by Def3;

      end;

      hence thesis;

    end;

    theorem :: ZMODLAT1:45

    for V,W be non empty ModuleStr over INT.Ring , f be FrForm of V, W holds (( 1. F_Real ) * f) = f

    proof

      let V,W be non empty ModuleStr over INT.Ring , f be FrForm of V, W;

      now

        let v be Vector of V, w be Vector of W;

        

        thus ((( 1. F_Real ) * f) . (v,w)) = (( 1. F_Real ) * (f . (v,w))) by Def3

        .= (f . (v,w));

      end;

      hence thesis;

    end;

    definition

      let V be ModuleStr over INT.Ring ;

      mode FrFunctional of V is Function of the carrier of V, the carrier of F_Real ;

    end

    definition

      let V be non empty ModuleStr over INT.Ring ;

      let f,g be FrFunctional of V;

      :: ZMODLAT1:def17

      func f + g -> FrFunctional of V means

      : HDef3: for x be Element of V holds (it . x) = ((f . x) + (g . x));

      existence

      proof

        deffunc G( Element of V) = ((f . $1) + (g . $1));

        consider F be Function of the carrier of V, the carrier of F_Real such that

         A1: for x be Element of V holds (F . x) = G(x) from FUNCT_2:sch 4;

        reconsider F as FrFunctional of V;

        take F;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let a,b be FrFunctional of V such that

         A2: for x be Element of V holds (a . x) = ((f . x) + (g . x)) and

         A3: for x be Element of V holds (b . x) = ((f . x) + (g . x));

        now

          let x be Element of V;

          

          thus (a . x) = ((f . x) + (g . x)) by A2

          .= (b . x) by A3;

        end;

        hence a = b by FUNCT_2: 63;

      end;

    end

    definition

      let V be non empty ModuleStr over INT.Ring ;

      let f be FrFunctional of V;

      :: ZMODLAT1:def18

      func - f -> FrFunctional of V means

      : HDef4: for x be Element of V holds (it . x) = ( - (f . x));

      existence

      proof

        deffunc G( Element of V) = ( - (f . $1));

        consider F be Function of the carrier of V, the carrier of F_Real such that

         A1: for x be Element of V holds (F . x) = G(x) from FUNCT_2:sch 4;

        reconsider F as FrFunctional of V;

        take F;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let a,b be FrFunctional of V such that

         A2: for x be Element of V holds (a . x) = ( - (f . x)) and

         A3: for x be Element of V holds (b . x) = ( - (f . x));

        now

          let x be Element of V;

          

          thus (a . x) = ( - (f . x)) by A2

          .= (b . x) by A3;

        end;

        hence a = b by FUNCT_2: 63;

      end;

    end

    definition

      let V be non empty ModuleStr over INT.Ring ;

      let f,g be FrFunctional of V;

      :: ZMODLAT1:def19

      func f - g -> FrFunctional of V equals (f + ( - g));

      coherence ;

    end

    definition

      let V be non empty ModuleStr over INT.Ring ;

      let v be Element of F_Real ;

      let f be FrFunctional of V;

      :: ZMODLAT1:def20

      func v * f -> FrFunctional of V means

      : HDef6: for x be Element of V holds (it . x) = (v * (f . x));

      existence

      proof

        deffunc G( Element of V) = (v * (f . $1));

        consider F be Function of the carrier of V, the carrier of F_Real such that

         A1: for x be Element of V holds (F . x) = G(x) from FUNCT_2:sch 4;

        reconsider F as FrFunctional of V;

        take F;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let a,b be FrFunctional of V such that

         A2: for x be Element of V holds (a . x) = (v * (f . x)) and

         A3: for x be Element of V holds (b . x) = (v * (f . x));

        now

          let x be Element of V;

          

          thus (a . x) = (v * (f . x)) by A2

          .= (b . x) by A3;

        end;

        hence thesis by FUNCT_2: 63;

      end;

    end

    definition

      let V be ModuleStr over INT.Ring ;

      :: ZMODLAT1:def21

      func 0FrFunctional (V) -> FrFunctional of V equals (( [#] V) --> ( 0. F_Real ));

      coherence ;

    end

    definition

      let V be non empty ModuleStr over INT.Ring ;

      let F be FrFunctional of V;

      :: ZMODLAT1:def22

      attr F is homogeneous means

      : HDef8: for x be Vector of V, r be Scalar of V holds (F . (r * x)) = (r * (F . x));

    end

    definition

      let V be non empty ModuleStr over INT.Ring ;

      let F be FrFunctional of V;

      :: ZMODLAT1:def23

      attr F is 0-preserving means (F . ( 0. V)) = ( 0. F_Real );

    end

    registration

      let V be Z_Module;

      cluster homogeneous -> 0-preserving for FrFunctional of V;

      coherence

      proof

        let F be FrFunctional of V;

        assume

         A1: F is homogeneous;

        

        thus (F . ( 0. V)) = (F . (( 0. INT.Ring ) * ( 0. V))) by ZMODUL01: 1

        .= (( 0. INT.Ring ) * (F . ( 0. V))) by A1

        .= ( 0. F_Real );

      end;

    end

    registration

      let V be non empty ModuleStr over INT.Ring ;

      cluster ( 0FrFunctional V) -> additive;

      coherence

      proof

        let x,y be Vector of V;

        

         A1: (( 0FrFunctional V) . x) = ( 0. F_Real ) & (( 0FrFunctional V) . y) = ( 0. F_Real ) by FUNCOP_1: 7;

        thus (( 0FrFunctional V) . (x + y)) = ((( 0FrFunctional V) . x) + (( 0FrFunctional V) . y)) by A1, FUNCOP_1: 7;

      end;

    end

    registration

      let V be non empty ModuleStr over INT.Ring ;

      cluster ( 0FrFunctional V) -> homogeneous;

      coherence

      proof

        let x be Vector of V;

        let r be Scalar of V;

        

         A1: (( 0FrFunctional V) . x) = ( 0. F_Real ) by FUNCOP_1: 7;

        thus (( 0FrFunctional V) . (r * x)) = (r * (( 0FrFunctional V) . x)) by A1, FUNCOP_1: 7;

      end;

    end

    registration

      let V be non empty ModuleStr over INT.Ring ;

      cluster ( 0FrFunctional V) -> 0-preserving;

      coherence by FUNCOP_1: 7;

    end

    registration

      let V be non empty ModuleStr over INT.Ring ;

      cluster additive homogeneous 0-preserving for FrFunctional of V;

      existence

      proof

        take ( 0FrFunctional V);

        thus thesis;

      end;

    end

    theorem :: ZMODLAT1:46

    for V be non empty ModuleStr over INT.Ring , f,g be FrFunctional of V holds (f + g) = (g + f)

    proof

      let V be non empty ModuleStr over INT.Ring ;

      let f,g be FrFunctional of V;

      now

        let x be Element of V;

        

        thus ((f + g) . x) = ((f . x) + (g . x)) by HDef3

        .= ((g + f) . x) by HDef3;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: ZMODLAT1:47

    for V be non empty ModuleStr over INT.Ring , f,g,h be FrFunctional of V holds ((f + g) + h) = (f + (g + h))

    proof

      let V be non empty ModuleStr over INT.Ring ;

      let f,g,h be FrFunctional of V;

      now

        let x be Element of V;

        

        thus (((f + g) + h) . x) = (((f + g) . x) + (h . x)) by HDef3

        .= (((f . x) + (g . x)) + (h . x)) by HDef3

        .= ((f . x) + ((g . x) + (h . x)))

        .= ((f . x) + ((g + h) . x)) by HDef3

        .= ((f + (g + h)) . x) by HDef3;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: ZMODLAT1:48

    for V be non empty ModuleStr over INT.Ring , x be Element of V holds (( 0FrFunctional V) . x) = ( 0. F_Real ) by FUNCOP_1: 7;

    theorem :: ZMODLAT1:49

    for V be non empty ModuleStr over INT.Ring , f be FrFunctional of V holds (f + ( 0FrFunctional V)) = f

    proof

      let V be non empty ModuleStr over INT.Ring ;

      let f be FrFunctional of V;

      now

        let x be Element of V;

        

        thus ((f + ( 0FrFunctional V)) . x) = ((f . x) + (( 0FrFunctional V) . x)) by HDef3

        .= ((f . x) + ( 0. F_Real )) by FUNCOP_1: 7

        .= (f . x);

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: ZMODLAT1:50

    for V be non empty ModuleStr over INT.Ring , f be FrFunctional of V holds (f - f) = ( 0FrFunctional V)

    proof

      let V be non empty ModuleStr over INT.Ring ;

      let f be FrFunctional of V;

      now

        let x be Element of V;

        

        thus ((f - f) . x) = ((f . x) + (( - f) . x)) by HDef3

        .= ((f . x) + ( - (f . x))) by HDef4

        .= (( 0FrFunctional V) . x) by FUNCOP_1: 7;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: ZMODLAT1:51

    for V be non empty ModuleStr over INT.Ring , r be Element of F_Real , f,g be FrFunctional of V holds (r * (f + g)) = ((r * f) + (r * g))

    proof

      let V be non empty ModuleStr over INT.Ring ;

      let r be Element of F_Real ;

      let f,g be FrFunctional of V;

      now

        let x be Element of V;

        

        thus ((r * (f + g)) . x) = (r * ((f + g) . x)) by HDef6

        .= (r * ((f . x) + (g . x))) by HDef3

        .= ((r * (f . x)) + (r * (g . x)))

        .= (((r * f) . x) + (r * (g . x))) by HDef6

        .= (((r * f) . x) + ((r * g) . x)) by HDef6

        .= (((r * f) + (r * g)) . x) by HDef3;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: ZMODLAT1:52

    for V be non empty ModuleStr over INT.Ring , r,s be Element of F_Real , f be FrFunctional of V holds ((r + s) * f) = ((r * f) + (s * f))

    proof

      let V be non empty ModuleStr over INT.Ring ;

      let r,s be Element of F_Real ;

      let f be FrFunctional of V;

      now

        let x be Element of V;

        

        thus (((r + s) * f) . x) = ((r + s) * (f . x)) by HDef6

        .= ((r * (f . x)) + (s * (f . x)))

        .= (((r * f) . x) + (s * (f . x))) by HDef6

        .= (((r * f) . x) + ((s * f) . x)) by HDef6

        .= (((r * f) + (s * f)) . x) by HDef3;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: ZMODLAT1:53

    for V be non empty ModuleStr over INT.Ring , r,s be Element of F_Real , f be FrFunctional of V holds ((r * s) * f) = (r * (s * f))

    proof

      let V be non empty ModuleStr over INT.Ring ;

      let r,s be Element of F_Real ;

      let f be FrFunctional of V;

      now

        let x be Element of V;

        

        thus (((r * s) * f) . x) = ((r * s) * (f . x)) by HDef6

        .= (r * (s * (f . x)))

        .= (r * ((s * f) . x)) by HDef6

        .= ((r * (s * f)) . x) by HDef6;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: ZMODLAT1:54

    for V be non empty ModuleStr over INT.Ring , f be FrFunctional of V holds (( 1. F_Real ) * f) = f

    proof

      let V be non empty ModuleStr over INT.Ring ;

      let f be FrFunctional of V;

      now

        let x be Element of V;

        

        thus ((( 1. F_Real ) * f) . x) = (( 1. F_Real ) * (f . x)) by HDef6

        .= (f . x);

      end;

      hence thesis by FUNCT_2: 63;

    end;

    registration

      let V be non empty ModuleStr over INT.Ring ;

      let f,g be additive FrFunctional of V;

      cluster (f + g) -> additive;

      coherence

      proof

        let x,y be Vector of V;

        

        thus ((f + g) . (x + y)) = ((f . (x + y)) + (g . (x + y))) by HDef3

        .= (((f . x) + (f . y)) + (g . (x + y))) by VECTSP_1:def 20

        .= (((f . x) + (f . y)) + ((g . x) + (g . y))) by VECTSP_1:def 20

        .= (((f . x) + (g . x)) + ((f . y) + (g . y)))

        .= (((f + g) . x) + ((f . y) + (g . y))) by HDef3

        .= (((f + g) . x) + ((f + g) . y)) by HDef3;

      end;

    end

    registration

      let V be non empty ModuleStr over INT.Ring ;

      let f be additive FrFunctional of V;

      cluster ( - f) -> additive;

      coherence

      proof

        let x,y be Vector of V;

        

        thus (( - f) . (x + y)) = ( - (f . (x + y))) by HDef4

        .= ( - ((f . x) + (f . y))) by VECTSP_1:def 20

        .= (( - (f . x)) + ( - (f . y)))

        .= ((( - f) . x) + ( - (f . y))) by HDef4

        .= ((( - f) . x) + (( - f) . y)) by HDef4;

      end;

    end

    registration

      let V be non empty ModuleStr over INT.Ring ;

      let v be Element of F_Real ;

      let f be additive FrFunctional of V;

      cluster (v * f) -> additive;

      coherence

      proof

        let x,y be Vector of V;

        

        thus ((v * f) . (x + y)) = (v * (f . (x + y))) by HDef6

        .= (v * ((f . x) + (f . y))) by VECTSP_1:def 20

        .= ((v * (f . x)) + (v * (f . y)))

        .= (((v * f) . x) + (v * (f . y))) by HDef6

        .= (((v * f) . x) + ((v * f) . y)) by HDef6;

      end;

    end

    registration

      let V be non empty ModuleStr over INT.Ring ;

      let f,g be homogeneous FrFunctional of V;

      cluster (f + g) -> homogeneous;

      coherence

      proof

        let x be Vector of V;

        let r be Scalar of V;

        

        thus ((f + g) . (r * x)) = ((f . (r * x)) + (g . (r * x))) by HDef3

        .= ((r * (f . x)) + (g . (r * x))) by HDef8

        .= ((r * (f . x)) + (r * (g . x))) by HDef8

        .= (r * ((f . x) + (g . x)))

        .= (r * ((f + g) . x)) by HDef3;

      end;

    end

    registration

      let V be non empty ModuleStr over INT.Ring ;

      let f be homogeneous FrFunctional of V;

      cluster ( - f) -> homogeneous;

      coherence

      proof

        let x be Vector of V;

        let r be Scalar of V;

        

        thus (( - f) . (r * x)) = ( - (f . (r * x))) by HDef4

        .= ( - (r * (f . x))) by HDef8

        .= (r * ( - (f . x)))

        .= (r * (( - f) . x)) by HDef4;

      end;

    end

    registration

      let V be non empty ModuleStr over INT.Ring ;

      let v be Element of F_Real ;

      let f be homogeneous FrFunctional of V;

      cluster (v * f) -> homogeneous;

      coherence

      proof

        let x be Vector of V;

        let r be Scalar of V;

        

        thus ((v * f) . (r * x)) = (v * (f . (r * x))) by HDef6

        .= (v * (r * (f . x))) by HDef8

        .= (r * (v * (f . x)))

        .= (r * ((v * f) . x)) by HDef6;

      end;

    end

    definition

      let V,W be non empty ModuleStr over INT.Ring ;

      let f be FrForm of V, W, v be Vector of V;

      :: ZMODLAT1:def24

      func FrFunctionalFAF (f,v) -> FrFunctional of W equals (( curry f) . v);

      correctness ;

    end

    definition

      let V,W be non empty ModuleStr over INT.Ring ;

      let f be FrForm of V, W, w be Vector of W;

      :: ZMODLAT1:def25

      func FrFunctionalSAF (f,w) -> FrFunctional of V equals (( curry' f) . w);

      correctness ;

    end

    theorem :: ZMODLAT1:55

    

     HTh8: for V,W be non empty ModuleStr over INT.Ring , f be FrForm of V, W, v be Vector of V holds ( dom ( FrFunctionalFAF (f,v))) = the carrier of W & ( rng ( FrFunctionalFAF (f,v))) c= the carrier of F_Real & for w be Vector of W holds (( FrFunctionalFAF (f,v)) . w) = (f . (v,w))

    proof

      let V,W be non empty ModuleStr over INT.Ring ;

      let f be FrForm of V, W, v be Vector of V;

      set F = ( FrFunctionalFAF (f,v));

      ( dom f) = [:the carrier of V, the carrier of W:] by FUNCT_2:def 1;

      then

       A1: ex g be Function st (( curry f) . v) = g & ( dom g) = the carrier of W & ( rng g) c= ( rng f) & for y be object st y in the carrier of W holds (g . y) = (f . (v,y)) by FUNCT_5: 29;

      hence ( dom F) = the carrier of W & ( rng F) c= the carrier of F_Real ;

      let y be Vector of W;

      thus thesis by A1;

    end;

    theorem :: ZMODLAT1:56

    

     HTh9: for V,W be non empty ModuleStr over INT.Ring , f be FrForm of V, W, w be Vector of W holds ( dom ( FrFunctionalSAF (f,w))) = the carrier of V & ( rng ( FrFunctionalSAF (f,w))) c= the carrier of F_Real & for v be Vector of V holds (( FrFunctionalSAF (f,w)) . v) = (f . (v,w))

    proof

      let V,W be non empty ModuleStr over INT.Ring , f be FrForm of V, W, w be Vector of W;

      set F = ( FrFunctionalSAF (f,w));

      ( dom f) = [:the carrier of V, the carrier of W:] by FUNCT_2:def 1;

      then

       A1: ex g be Function st (( curry' f) . w) = g & ( dom g) = the carrier of V & ( rng g) c= ( rng f) & for y be object st y in the carrier of V holds (g . y) = (f . (y,w)) by FUNCT_5: 32;

      hence ( dom F) = the carrier of V & ( rng F) c= the carrier of F_Real ;

      let v be Vector of V;

      thus thesis by A1;

    end;

    theorem :: ZMODLAT1:57

    for V be non empty ModuleStr over INT.Ring , x be Element of V holds (( 0FrFunctional V) . x) = ( 0. F_Real ) by FUNCOP_1: 7;

    theorem :: ZMODLAT1:58

    

     HTh10: for V,W be non empty ModuleStr over INT.Ring , v be Vector of V holds ( FrFunctionalFAF (( NulFrForm (V,W)),v)) = ( 0FrFunctional W)

    proof

      let V,W be non empty ModuleStr over INT.Ring , v be Vector of V;

      set N = ( NulFrForm (V,W));

      now

        let y be Vector of W;

        

        thus (( FrFunctionalFAF (N,v)) . y) = (N . (v,y)) by HTh8

        .= ( 0. F_Real ) by FUNCOP_1: 70

        .= (( 0FrFunctional W) . y) by FUNCOP_1: 7;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: ZMODLAT1:59

    

     HTh11: for V,W be non empty ModuleStr over INT.Ring , w be Vector of W holds ( FrFunctionalSAF (( NulFrForm (V,W)),w)) = ( 0FrFunctional V)

    proof

      let V,W be non empty ModuleStr over INT.Ring , y be Vector of W;

      set N = ( NulFrForm (V,W));

      now

        let v be Vector of V;

        

        thus (( FrFunctionalSAF (N,y)) . v) = (N . (v,y)) by HTh9

        .= ( 0. INT.Ring ) by FUNCOP_1: 70

        .= (( 0FrFunctional V) . v) by FUNCOP_1: 7;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: ZMODLAT1:60

    

     HTh12: for V,W be non empty ModuleStr over INT.Ring , f,g be FrForm of V, W, w be Vector of W holds ( FrFunctionalSAF ((f + g),w)) = (( FrFunctionalSAF (f,w)) + ( FrFunctionalSAF (g,w)))

    proof

      let V,W be non empty ModuleStr over INT.Ring , f,g be FrForm of V, W, w be Vector of W;

      now

        let v be Vector of V;

        

        thus (( FrFunctionalSAF ((f + g),w)) . v) = ((f + g) . (v,w)) by HTh9

        .= ((f . (v,w)) + (g . (v,w))) by Def2

        .= ((( FrFunctionalSAF (f,w)) . v) + (g . (v,w))) by HTh9

        .= ((( FrFunctionalSAF (f,w)) . v) + (( FrFunctionalSAF (g,w)) . v)) by HTh9

        .= ((( FrFunctionalSAF (f,w)) + ( FrFunctionalSAF (g,w))) . v) by HDef3;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: ZMODLAT1:61

    

     HTh13: for V,W be non empty ModuleStr over INT.Ring , f,g be FrForm of V, W, v be Vector of V holds ( FrFunctionalFAF ((f + g),v)) = (( FrFunctionalFAF (f,v)) + ( FrFunctionalFAF (g,v)))

    proof

      let V,W be non empty ModuleStr over INT.Ring , f,g be FrForm of V, W, w be Vector of V;

      now

        let v be Vector of W;

        

        thus (( FrFunctionalFAF ((f + g),w)) . v) = ((f + g) . (w,v)) by HTh8

        .= ((f . (w,v)) + (g . (w,v))) by Def2

        .= ((( FrFunctionalFAF (f,w)) . v) + (g . (w,v))) by HTh8

        .= ((( FrFunctionalFAF (f,w)) . v) + (( FrFunctionalFAF (g,w)) . v)) by HTh8

        .= ((( FrFunctionalFAF (f,w)) + ( FrFunctionalFAF (g,w))) . v) by HDef3;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: ZMODLAT1:62

    

     HTh14: for V,W be non empty ModuleStr over INT.Ring , f be FrForm of V, W, a be Element of F_Real , w be Vector of W holds ( FrFunctionalSAF ((a * f),w)) = (a * ( FrFunctionalSAF (f,w)))

    proof

      let V,W be non empty ModuleStr over INT.Ring , f be FrForm of V, W, a be Element of F_Real , w be Vector of W;

      now

        let v be Vector of V;

        

        thus (( FrFunctionalSAF ((a * f),w)) . v) = ((a * f) . (v,w)) by HTh9

        .= (a * (f . (v,w))) by Def3

        .= (a * (( FrFunctionalSAF (f,w)) . v)) by HTh9

        .= ((a * ( FrFunctionalSAF (f,w))) . v) by HDef6;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: ZMODLAT1:63

    

     HTh15: for V,W be non empty ModuleStr over INT.Ring , f be FrForm of V, W, a be Element of F_Real , v be Vector of V holds ( FrFunctionalFAF ((a * f),v)) = (a * ( FrFunctionalFAF (f,v)))

    proof

      let V,W be non empty ModuleStr over INT.Ring , f be FrForm of V, W, a be Element of F_Real , w be Vector of V;

      now

        let v be Vector of W;

        

        thus (( FrFunctionalFAF ((a * f),w)) . v) = ((a * f) . (w,v)) by HTh8

        .= (a * (f . (w,v))) by Def3

        .= (a * (( FrFunctionalFAF (f,w)) . v)) by HTh8

        .= ((a * ( FrFunctionalFAF (f,w))) . v) by HDef6;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: ZMODLAT1:64

    for V,W be non empty ModuleStr over INT.Ring , f be FrForm of V, W, w be Vector of W holds ( FrFunctionalSAF (( - f),w)) = ( - ( FrFunctionalSAF (f,w)))

    proof

      let V,W be non empty ModuleStr over INT.Ring , f be FrForm of V, W, w be Vector of W;

      now

        let v be Vector of V;

        

        thus (( FrFunctionalSAF (( - f),w)) . v) = (( - f) . (v,w)) by HTh9

        .= ( - (f . (v,w))) by Def4

        .= ( - (( FrFunctionalSAF (f,w)) . v)) by HTh9

        .= (( - ( FrFunctionalSAF (f,w))) . v) by HDef4;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: ZMODLAT1:65

    for V,W be non empty ModuleStr over INT.Ring , f be FrForm of V, W, v be Vector of V holds ( FrFunctionalFAF (( - f),v)) = ( - ( FrFunctionalFAF (f,v)))

    proof

      let V,W be non empty ModuleStr over INT.Ring , f be FrForm of V, W, w be Vector of V;

      now

        let v be Vector of W;

        

        thus (( FrFunctionalFAF (( - f),w)) . v) = (( - f) . (w,v)) by HTh8

        .= ( - (f . (w,v))) by Def4

        .= ( - (( FrFunctionalFAF (f,w)) . v)) by HTh8

        .= (( - ( FrFunctionalFAF (f,w))) . v) by HDef4;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: ZMODLAT1:66

    for V,W be non empty ModuleStr over INT.Ring , f,g be FrForm of V, W, w be Vector of W holds ( FrFunctionalSAF ((f - g),w)) = (( FrFunctionalSAF (f,w)) - ( FrFunctionalSAF (g,w)))

    proof

      let V,W be non empty ModuleStr over INT.Ring , f,g be FrForm of V, W, w be Vector of W;

      now

        let v be Vector of V;

        

        thus (( FrFunctionalSAF ((f - g),w)) . v) = ((f - g) . (v,w)) by HTh9

        .= ((f . (v,w)) - (g . (v,w))) by Def7

        .= ((( FrFunctionalSAF (f,w)) . v) - (g . (v,w))) by HTh9

        .= ((( FrFunctionalSAF (f,w)) . v) - (( FrFunctionalSAF (g,w)) . v)) by HTh9

        .= ((( FrFunctionalSAF (f,w)) . v) + (( - ( FrFunctionalSAF (g,w))) . v)) by HDef4

        .= ((( FrFunctionalSAF (f,w)) - ( FrFunctionalSAF (g,w))) . v) by HDef3;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: ZMODLAT1:67

    for V,W be non empty ModuleStr over INT.Ring , f,g be FrForm of V, W, v be Vector of V holds ( FrFunctionalFAF ((f - g),v)) = (( FrFunctionalFAF (f,v)) - ( FrFunctionalFAF (g,v)))

    proof

      let V,W be non empty ModuleStr over INT.Ring , f,g be FrForm of V, W, w be Vector of V;

      now

        let v be Vector of W;

        

        thus (( FrFunctionalFAF ((f - g),w)) . v) = ((f - g) . (w,v)) by HTh8

        .= ((f . (w,v)) - (g . (w,v))) by Def7

        .= ((( FrFunctionalFAF (f,w)) . v) - (g . (w,v))) by HTh8

        .= ((( FrFunctionalFAF (f,w)) . v) - (( FrFunctionalFAF (g,w)) . v)) by HTh8

        .= ((( FrFunctionalFAF (f,w)) . v) + (( - ( FrFunctionalFAF (g,w))) . v)) by HDef4

        .= ((( FrFunctionalFAF (f,w)) - ( FrFunctionalFAF (g,w))) . v) by HDef3;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    definition

      let V,W be non empty ModuleStr over INT.Ring ;

      let f be FrFunctional of V;

      let g be FrFunctional of W;

      :: ZMODLAT1:def26

      func FrFormFunctional (f,g) -> FrForm of V, W means

      : HDef10: for v be Vector of V, w be Vector of W holds (it . (v,w)) = ((f . v) * (g . w));

      existence

      proof

        deffunc F( Vector of V, Vector of W) = ((f . $1) * (g . $2));

        set c1 = the carrier of V, c2 = the carrier of W, k = the carrier of F_Real ;

        consider i be Function of [:c1, c2:], k such that

         A1: for x be Element of c1, y be Element of c2 holds (i . (x,y)) = F(x,y) from BINOP_1:sch 4;

        reconsider i as FrForm of V, W;

        take i;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let F1,F2 be FrForm of V, W such that

         A2: for v be Vector of V, y be Vector of W holds (F1 . (v,y)) = ((f . v) * (g . y)) and

         A3: for v be Vector of V, y be Vector of W holds (F2 . (v,y)) = ((f . v) * (g . y));

        now

          let v be Vector of V, y be Vector of W;

          

          thus (F1 . (v,y)) = ((f . v) * (g . y)) by A2

          .= (F2 . (v,y)) by A3;

        end;

        hence thesis;

      end;

    end

    theorem :: ZMODLAT1:68

    

     HTh20: for V,W be non empty ModuleStr over INT.Ring , f be FrFunctional of V, v be Vector of V, w be Vector of W holds (( FrFormFunctional (f,( 0FrFunctional W))) . (v,w)) = ( 0. INT.Ring )

    proof

      let V,W be non empty ModuleStr over INT.Ring ;

      let f be FrFunctional of V, v be Vector of V, y be Vector of W;

      set 0F = ( 0FrFunctional W), F = ( FrFormFunctional (f,0F));

      

      thus (F . (v,y)) = ((f . v) * (0F . y)) by HDef10

      .= ((f . v) * ( 0. INT.Ring )) by FUNCOP_1: 7

      .= ( 0. INT.Ring );

    end;

    theorem :: ZMODLAT1:69

    

     HTh21: for V,W be non empty ModuleStr over INT.Ring , g be FrFunctional of W, v be Vector of V, w be Vector of W holds (( FrFormFunctional (( 0FrFunctional V),g)) . (v,w)) = ( 0. INT.Ring )

    proof

      let V,W be non empty ModuleStr over INT.Ring ;

      let h be FrFunctional of W, v be Vector of V, y be Vector of W;

      set 0F = ( 0FrFunctional V), F = ( FrFormFunctional (0F,h));

      

      thus (F . (v,y)) = ((0F . v) * (h . y)) by HDef10

      .= (( 0. INT.Ring ) * (h . y)) by FUNCOP_1: 7

      .= ( 0. INT.Ring );

    end;

    theorem :: ZMODLAT1:70

    for V,W be non empty ModuleStr over INT.Ring , f be FrFunctional of V holds ( FrFormFunctional (f,( 0FrFunctional W))) = ( NulFrForm (V,W))

    proof

      let V,W be non empty ModuleStr over INT.Ring , f be FrFunctional of V;

      now

        let v be Vector of V, y be Vector of W;

        

        thus (( FrFormFunctional (f,( 0FrFunctional W))) . (v,y)) = ( 0. INT.Ring ) by HTh20

        .= (( NulFrForm (V,W)) . (v,y)) by FUNCOP_1: 70;

      end;

      hence thesis;

    end;

    theorem :: ZMODLAT1:71

    for V,W be non empty ModuleStr over INT.Ring , g be FrFunctional of W holds ( FrFormFunctional (( 0FrFunctional V),g)) = ( NulFrForm (V,W))

    proof

      let V,W be non empty ModuleStr over INT.Ring , h be FrFunctional of W;

      now

        let v be Vector of V, y be Vector of W;

        

        thus (( FrFormFunctional (( 0FrFunctional V),h)) . (v,y)) = ( 0. INT.Ring ) by HTh21

        .= (( NulFrForm (V,W)) . (v,y)) by FUNCOP_1: 70;

      end;

      hence thesis;

    end;

    theorem :: ZMODLAT1:72

    

     HTh24: for V,W be non empty ModuleStr over INT.Ring , f be FrFunctional of V, g be FrFunctional of W, v be Vector of V holds ( FrFunctionalFAF (( FrFormFunctional (f,g)),v)) = ((f . v) * g)

    proof

      let V,W be non empty ModuleStr over INT.Ring ;

      let f be FrFunctional of V, h be FrFunctional of W, v be Vector of V;

      set F = ( FrFormFunctional (f,h)), FF = ( FrFunctionalFAF (F,v));

      now

        let y be Vector of W;

        

        thus (FF . y) = (F . (v,y)) by HTh8

        .= ((f . v) * (h . y)) by HDef10

        .= (((f . v) * h) . y) by HDef6;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: ZMODLAT1:73

    

     HTh25: for V,W be non empty ModuleStr over INT.Ring , f be FrFunctional of V, g be FrFunctional of W, w be Vector of W holds ( FrFunctionalSAF (( FrFormFunctional (f,g)),w)) = ((g . w) * f)

    proof

      let V,W be non empty ModuleStr over INT.Ring ;

      let f be FrFunctional of V, h be FrFunctional of W, y be Vector of W;

      set F = ( FrFormFunctional (f,h)), FF = ( FrFunctionalSAF (F,y));

      now

        let v be Vector of V;

        

        thus (FF . v) = (F . (v,y)) by HTh9

        .= ((f . v) * (h . y)) by HDef10

        .= (((h . y) * f) . v) by HDef6;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    begin

    definition

      let V,W be non empty ModuleStr over INT.Ring ;

      let f be FrForm of V, W;

      :: ZMODLAT1:def27

      attr f is additiveFAF means

      : HDef11: for v be Vector of V holds ( FrFunctionalFAF (f,v)) is additive;

      :: ZMODLAT1:def28

      attr f is additiveSAF means

      : HDef12: for w be Vector of W holds ( FrFunctionalSAF (f,w)) is additive;

    end

    definition

      let V,W be non empty ModuleStr over INT.Ring ;

      let f be FrForm of V, W;

      :: ZMODLAT1:def29

      attr f is homogeneousFAF means

      : HDef13: for v be Vector of V holds ( FrFunctionalFAF (f,v)) is homogeneous;

      :: ZMODLAT1:def30

      attr f is homogeneousSAF means

      : HDef14: for w be Vector of W holds ( FrFunctionalSAF (f,w)) is homogeneous;

    end

    registration

      let V,W be non empty ModuleStr over INT.Ring ;

      cluster ( NulFrForm (V,W)) -> additiveFAF;

      coherence

      proof

        let v be Vector of V;

        ( FrFunctionalFAF (( NulFrForm (V,W)),v)) = ( 0FrFunctional W) by HTh10;

        hence thesis;

      end;

      cluster ( NulFrForm (V,W)) -> additiveSAF;

      coherence

      proof

        let y be Vector of W;

        ( FrFunctionalSAF (( NulFrForm (V,W)),y)) = ( 0FrFunctional V) by HTh11;

        hence thesis;

      end;

    end

    registration

      let V,W be non empty ModuleStr over INT.Ring ;

      cluster additiveFAF additiveSAF for FrForm of V, W;

      existence

      proof

        take ( NulFrForm (V,W));

        thus thesis;

      end;

    end

    registration

      let V,W be non empty ModuleStr over INT.Ring ;

      cluster ( NulFrForm (V,W)) -> homogeneousFAF;

      coherence

      proof

        let v be Vector of V;

        ( FrFunctionalFAF (( NulFrForm (V,W)),v)) = ( 0FrFunctional W) by HTh10;

        hence thesis;

      end;

      cluster ( NulFrForm (V,W)) -> homogeneousSAF;

      coherence

      proof

        let y be Vector of W;

        ( FrFunctionalSAF (( NulFrForm (V,W)),y)) = ( 0FrFunctional V) by HTh11;

        hence thesis;

      end;

    end

    registration

      let V,W be non empty ModuleStr over INT.Ring ;

      cluster additiveFAF homogeneousFAF additiveSAF homogeneousSAF for FrForm of V, W;

      existence

      proof

        take ( NulFrForm (V,W));

        thus thesis;

      end;

    end

    definition

      let V,W be non empty ModuleStr over INT.Ring ;

      mode bilinear-FrForm of V,W is additiveSAF homogeneousSAF additiveFAF homogeneousFAF FrForm of V, W;

    end

    registration

      let V,W be non empty ModuleStr over INT.Ring ;

      let f be additiveFAF FrForm of V, W, v be Vector of V;

      cluster ( FrFunctionalFAF (f,v)) -> additive;

      coherence by HDef11;

    end

    registration

      let V,W be non empty ModuleStr over INT.Ring ;

      let f be additiveSAF FrForm of V, W, w be Vector of W;

      cluster ( FrFunctionalSAF (f,w)) -> additive;

      coherence by HDef12;

    end

    registration

      let V,W be non empty ModuleStr over INT.Ring ;

      let f be homogeneousFAF FrForm of V, W, v be Vector of V;

      cluster ( FrFunctionalFAF (f,v)) -> homogeneous;

      coherence by HDef13;

    end

    registration

      let V,W be non empty ModuleStr over INT.Ring ;

      let f be homogeneousSAF FrForm of V, W, w be Vector of W;

      cluster ( FrFunctionalSAF (f,w)) -> homogeneous;

      coherence by HDef14;

    end

    registration

      let V,W be non empty ModuleStr over INT.Ring ;

      let f be FrFunctional of V, g be additive FrFunctional of W;

      cluster ( FrFormFunctional (f,g)) -> additiveFAF;

      coherence

      proof

        let v be Vector of V;

        set fg = ( FrFormFunctional (f,g)), F = ( FrFunctionalFAF (fg,v));

        let y,y9 be Vector of W;

        

         A1: F = ((f . v) * g) by HTh24;

        

        hence (F . (y + y9)) = ((f . v) * (g . (y + y9))) by HDef6

        .= ((f . v) * ((g . y) + (g . y9))) by VECTSP_1:def 20

        .= (((f . v) * (g . y)) + ((f . v) * (g . y9)))

        .= (((f . v) * (g . y)) + (F . y9)) by A1, HDef6

        .= ((F . y) + (F . y9)) by A1, HDef6;

      end;

    end

    registration

      let V,W be non empty ModuleStr over INT.Ring ;

      let f be additive FrFunctional of V, g be FrFunctional of W;

      cluster ( FrFormFunctional (f,g)) -> additiveSAF;

      coherence

      proof

        let y be Vector of W;

        set fg = ( FrFormFunctional (f,g)), F = ( FrFunctionalSAF (fg,y));

        F = ((g . y) * f) by HTh25;

        hence thesis;

      end;

    end

    registration

      let V,W be non empty ModuleStr over INT.Ring ;

      let f be FrFunctional of V, g be homogeneous FrFunctional of W;

      cluster ( FrFormFunctional (f,g)) -> homogeneousFAF;

      coherence

      proof

        let v be Vector of V;

        set fg = ( FrFormFunctional (f,g)), F = ( FrFunctionalFAF (fg,v));

        let y be Vector of W, r be Scalar of W;

        

         A1: F = ((f . v) * g) by HTh24;

        

        hence (F . (r * y)) = ((f . v) * (g . (r * y))) by HDef6

        .= ((f . v) * (r * (g . y))) by HDef8

        .= (r * ((f . v) * (g . y)))

        .= (r * (F . y)) by A1, HDef6;

      end;

    end

    registration

      let V,W be non empty ModuleStr over INT.Ring ;

      let f be homogeneous FrFunctional of V, g be FrFunctional of W;

      cluster ( FrFormFunctional (f,g)) -> homogeneousSAF;

      coherence

      proof

        let y be Vector of W;

        set fg = ( FrFormFunctional (f,g));

        set F = ( FrFunctionalSAF (fg,y));

        let v be Vector of V, r be Scalar of V;

        

         A1: F = ((g . y) * f) by HTh25;

        

        hence (F . (r * v)) = ((g . y) * (f . (r * v))) by HDef6

        .= ((g . y) * (r * (f . v))) by HDef8

        .= (r * ((g . y) * (f . v)))

        .= (r * (F . v)) by A1, HDef6;

      end;

    end

    registration

      let V be non trivial ModuleStr over INT.Ring , W be non empty ModuleStr over INT.Ring ;

      let f be FrFunctional of V, g be FrFunctional of W;

      cluster ( FrFormFunctional (f,g)) -> non trivial;

      coherence

      proof

        set fg = ( FrFormFunctional (f,g));

        set w = the Vector of W;

        consider v be Vector of V such that

         A1: v <> ( 0. V) by STRUCT_0:def 18;

        

         A2: [( 0. V), ( 0. W)] <> [v, w] by A1, XTUPLE_0: 1;

        ( dom fg) = [:the carrier of V, the carrier of W:] by FUNCT_2:def 1;

        then

         A3: [ [( 0. V), ( 0. W)], (fg . (( 0. V),( 0. W)))] in fg & [ [v, w], (fg . (v,w))] in fg by FUNCT_1: 1;

        assume

         A4: fg is trivial;

        per cases by A4, ZFMISC_1: 131;

          suppose fg = {} ;

          hence contradiction;

        end;

          suppose ex x be object st fg = {x};

          then

          consider x be object such that

           A5: fg = {x};

           [ [( 0. V), ( 0. W)], (fg . (( 0. V),( 0. W)))] = x & x = [ [v, w], (fg . (v,w))] by A3, A5, TARSKI:def 1;

          hence contradiction by A2, XTUPLE_0: 1;

        end;

      end;

    end

    registration

      let V be non empty ModuleStr over INT.Ring , W be non trivial ModuleStr over INT.Ring ;

      let f be FrFunctional of V, g be FrFunctional of W;

      cluster ( FrFormFunctional (f,g)) -> non trivial;

      coherence

      proof

        set fg = ( FrFormFunctional (f,g));

        set v = the Vector of V;

        consider w be Vector of W such that

         A1: w <> ( 0. W) by STRUCT_0:def 18;

        

         A2: [( 0. V), ( 0. W)] <> [v, w] by A1, XTUPLE_0: 1;

        ( dom fg) = [:the carrier of V, the carrier of W:] by FUNCT_2:def 1;

        then

         A3: [ [( 0. V), ( 0. W)], (fg . (( 0. V),( 0. W)))] in fg & [ [v, w], (fg . (v,w))] in fg by FUNCT_1: 1;

        assume

         A4: fg is trivial;

        per cases by A4, ZFMISC_1: 131;

          suppose fg = {} ;

          hence contradiction;

        end;

          suppose ex x be object st fg = {x};

          then

          consider x be object such that

           A5: fg = {x};

           [ [( 0. V), ( 0. W)], (fg . (( 0. V),( 0. W)))] = x & x = [ [v, w], (fg . (v,w))] by A3, A5, TARSKI:def 1;

          hence contradiction by A2, XTUPLE_0: 1;

        end;

      end;

    end

    definition

      let V be non empty ModuleStr over INT.Ring ;

      let F be FrFunctional of V;

      :: ZMODLAT1:def31

      attr F is 0-preserving means

      : HDef9: (F . ( 0. V)) = ( 0. F_Real );

    end

    registration

      let V be Z_Module;

      cluster homogeneous -> 0-preserving for FrFunctional of V;

      coherence

      proof

        let F be FrFunctional of V;

        assume

         A1: F is homogeneous;

        

        thus (F . ( 0. V)) = (F . (( 0. INT.Ring ) * ( 0. V))) by VECTSP_1: 14

        .= (( 0. INT.Ring ) * (F . ( 0. V))) by A1

        .= ( 0. F_Real );

      end;

    end

    registration

      let V be non empty ModuleStr over INT.Ring ;

      cluster ( 0FrFunctional V) -> 0-preserving;

      coherence by FUNCOP_1: 7;

    end

    registration

      let V be non empty ModuleStr over INT.Ring ;

      cluster additive homogeneous 0-preserving for FrFunctional of V;

      existence

      proof

        take ( 0FrFunctional V);

        thus thesis;

      end;

    end

    registration

      let V be non trivial free Z_Module;

      cluster additive homogeneous non constant non trivial for FrFunctional of V;

      existence

      proof

        set f = the additive homogeneous non constant non trivial Functional of V;

        reconsider g = f as FrFunctional of V by FUNCT_2: 7, NUMBERS: 15;

        take g;

        for x,y be Vector of V holds (g . (x + y)) = ((g . x) + (g . y))

        proof

          let x,y be Vector of V;

          

          thus (g . (x + y)) = ((f . x) + (f . y)) by VECTSP_1:def 20

          .= ((g . x) + (g . y));

        end;

        hence g is additive;

        for x be Vector of V, r be Element of INT.Ring holds (g . (r * x)) = (r * (g . x))

        proof

          let x be Vector of V, r be Element of INT.Ring ;

          

          thus (g . (r * x)) = (r * (f . x)) by HAHNBAN1:def 8

          .= (r * (g . x));

        end;

        hence g is homogeneous;

        thus g is non constant non trivial;

      end;

    end

    theorem :: ZMODLAT1:74

    

     VS10Th28: for V be non trivial free Z_Module, f be non constant 0-preserving FrFunctional of V holds ex v be Vector of V st v <> ( 0. V) & (f . v) <> ( 0. F_Real )

    proof

      let V be non trivial free Z_Module, f be non constant 0-preserving FrFunctional of V;

      

       A1: (f . ( 0. V)) = ( 0. F_Real ) by HDef9;

      assume

       A2: for v be Vector of V st v <> ( 0. V) holds (f . v) = ( 0. F_Real );

      now

        let x,y be object;

        assume x in ( dom f) & y in ( dom f);

        then

        reconsider v = x, w = y as Vector of V;

        

        thus (f . x) = (f . v)

        .= 0 by A2, A1

        .= (f . w) by A2, A1

        .= (f . y);

      end;

      hence contradiction by FUNCT_1:def 10;

    end;

    registration

      let V,W be non trivial free Z_Module;

      let f be non constant 0-preserving FrFunctional of V, g be non constant 0-preserving FrFunctional of W;

      cluster ( FrFormFunctional (f,g)) -> non constant;

      coherence

      proof

        set fg = ( FrFormFunctional (f,g));

        consider v be Vector of V such that v <> ( 0. V) and

         A1: (f . v) <> ( 0. F_Real ) by VS10Th28;

        consider w be Vector of W such that w <> ( 0. W) and

         A2: (g . w) <> ( 0. F_Real ) by VS10Th28;

        (fg . (v,w)) = ((f . v) * (g . w)) by HDef10;

        then

         A3: ( dom fg) = [:the carrier of V, the carrier of W:] & (fg . (v,w)) <> ( 0. F_Real ) by A1, A2, FUNCT_2:def 1;

        (fg . (( 0. V),( 0. W))) = ((f . ( 0. V)) * (g . ( 0. W))) by HDef10

        .= (( 0. INT.Ring ) * (g . ( 0. W))) by HDef9

        .= ( 0. F_Real );

        hence thesis by A3, BINOP_1: 19;

      end;

    end

    definition

      let V be non empty ModuleStr over INT.Ring ;

      mode linear-FrFunctional of V is additive homogeneous FrFunctional of V;

    end

    registration

      let V,W be non trivial free Z_Module;

      cluster non trivial non constant additiveFAF homogeneousFAF additiveSAF homogeneousSAF for FrForm of V, W;

      existence

      proof

        set f = the non constant non trivial linear-FrFunctional of V, g = the non constant non trivial linear-FrFunctional of W;

        take ( FrFormFunctional (f,g));

        thus thesis;

      end;

    end

    registration

      let V,W be non empty ModuleStr over INT.Ring ;

      let f,g be additiveSAF FrForm of V, W;

      cluster (f + g) -> additiveSAF;

      correctness

      proof

        let w be Vector of W;

        set Ffg = ( FrFunctionalSAF ((f + g),w)), Ff = ( FrFunctionalSAF (f,w));

        set Fg = ( FrFunctionalSAF (g,w));

        let v,y be Vector of V;

        

         A1: Ff is additive;

        

         A2: Fg is additive;

        

        thus (Ffg . (v + y)) = ((Ff + Fg) . (v + y)) by HTh12

        .= ((Ff . (v + y)) + (Fg . (v + y))) by HDef3

        .= (((Ff . v) + (Ff . y)) + (Fg . (v + y))) by A1

        .= (((Ff . v) + (Ff . y)) + ((Fg . v) + (Fg . y))) by A2

        .= ((((Ff . v) + (Fg . v)) + (Ff . y)) + (Fg . y))

        .= ((((Ff + Fg) . v) + (Ff . y)) + (Fg . y)) by HDef3

        .= (((Ff + Fg) . v) + ((Ff . y) + (Fg . y)))

        .= (((Ff + Fg) . v) + ((Ff + Fg) . y)) by HDef3

        .= ((Ffg . v) + ((Ff + Fg) . y)) by HTh12

        .= ((Ffg . v) + (Ffg . y)) by HTh12;

      end;

    end

    registration

      let V,W be non empty ModuleStr over INT.Ring ;

      let f,g be additiveFAF FrForm of V, W;

      cluster (f + g) -> additiveFAF;

      correctness

      proof

        let w be Vector of V;

        set Ffg = ( FrFunctionalFAF ((f + g),w)), Ff = ( FrFunctionalFAF (f,w));

        set Fg = ( FrFunctionalFAF (g,w));

        let v,y be Vector of W;

        

         A1: Ff is additive;

        

         A2: Fg is additive;

        

        thus (Ffg . (v + y)) = ((Ff + Fg) . (v + y)) by HTh13

        .= ((Ff . (v + y)) + (Fg . (v + y))) by HDef3

        .= (((Ff . v) + (Ff . y)) + (Fg . (v + y))) by A1

        .= (((Ff . v) + (Ff . y)) + ((Fg . v) + (Fg . y))) by A2

        .= ((((Ff . v) + (Fg . v)) + (Ff . y)) + (Fg . y))

        .= ((((Ff + Fg) . v) + (Ff . y)) + (Fg . y)) by HDef3

        .= (((Ff + Fg) . v) + ((Ff . y) + (Fg . y)))

        .= (((Ff + Fg) . v) + ((Ff + Fg) . y)) by HDef3

        .= ((Ffg . v) + ((Ff + Fg) . y)) by HTh13

        .= ((Ffg . v) + (Ffg . y)) by HTh13;

      end;

    end

    registration

      let V,W be non empty ModuleStr over INT.Ring ;

      let f be additiveSAF FrForm of V, W;

      let a be Element of F_Real ;

      cluster (a * f) -> additiveSAF;

      correctness

      proof

        let w be Vector of W;

        set Ffg = ( FrFunctionalSAF ((a * f),w)), Ff = ( FrFunctionalSAF (f,w));

        let v,y be Vector of V;

        

         A1: Ff is additive;

        

        thus (Ffg . (v + y)) = ((a * Ff) . (v + y)) by HTh14

        .= (a * (Ff . (v + y))) by HDef6

        .= (a * ((Ff . v) + (Ff . y))) by A1

        .= ((a * (Ff . v)) + (a * (Ff . y)))

        .= (((a * Ff) . v) + (a * (Ff . y))) by HDef6

        .= (((a * Ff) . v) + ((a * Ff) . y)) by HDef6

        .= ((Ffg . v) + ((a * Ff) . y)) by HTh14

        .= ((Ffg . v) + (Ffg . y)) by HTh14;

      end;

    end

    registration

      let V,W be non empty ModuleStr over INT.Ring ;

      let f be additiveFAF FrForm of V, W;

      let a be Element of F_Real ;

      cluster (a * f) -> additiveFAF;

      correctness

      proof

        let w be Vector of V;

        set Ffg = ( FrFunctionalFAF ((a * f),w)), Ff = ( FrFunctionalFAF (f,w));

        let v,y be Vector of W;

        

         A1: Ff is additive;

        

        thus (Ffg . (v + y)) = ((a * Ff) . (v + y)) by HTh15

        .= (a * (Ff . (v + y))) by HDef6

        .= (a * ((Ff . v) + (Ff . y))) by A1

        .= ((a * (Ff . v)) + (a * (Ff . y)))

        .= (((a * Ff) . v) + (a * (Ff . y))) by HDef6

        .= (((a * Ff) . v) + ((a * Ff) . y)) by HDef6

        .= ((Ffg . v) + ((a * Ff) . y)) by HTh15

        .= ((Ffg . v) + (Ffg . y)) by HTh15;

      end;

    end

    registration

      let V,W be non empty ModuleStr over INT.Ring ;

      let f be additiveSAF FrForm of V, W;

      cluster ( - f) -> additiveSAF;

      correctness ;

    end

    registration

      let V,W be non empty ModuleStr over INT.Ring ;

      let f be additiveFAF FrForm of V, W;

      cluster ( - f) -> additiveFAF;

      correctness ;

    end

    registration

      let V,W be non empty ModuleStr over INT.Ring ;

      let f,g be additiveSAF FrForm of V, W;

      cluster (f - g) -> additiveSAF;

      correctness ;

    end

    registration

      let V,W be non empty ModuleStr over INT.Ring ;

      let f,g be additiveFAF FrForm of V, W;

      cluster (f - g) -> additiveFAF;

      correctness ;

    end

    registration

      let V,W be non empty ModuleStr over INT.Ring ;

      let f,g be homogeneousSAF FrForm of V, W;

      cluster (f + g) -> homogeneousSAF;

      correctness

      proof

        let w be Vector of W;

        set Ffg = ( FrFunctionalSAF ((f + g),w)), Ff = ( FrFunctionalSAF (f,w));

        set Fg = ( FrFunctionalSAF (g,w));

        let v be Vector of V, a be Scalar of V;

        

        thus (Ffg . (a * v)) = ((Ff + Fg) . (a * v)) by HTh12

        .= ((Ff . (a * v)) + (Fg . (a * v))) by HDef3

        .= ((a * (Ff . v)) + (Fg . (a * v))) by HDef8

        .= ((a * (Ff . v)) + (a * (Fg . v))) by HDef8

        .= (a * ((Ff . v) + (Fg . v)))

        .= (a * ((Ff + Fg) . v)) by HDef3

        .= (a * (Ffg . v)) by HTh12;

      end;

    end

    registration

      let V,W be non empty ModuleStr over INT.Ring ;

      let f,g be homogeneousFAF FrForm of V, W;

      cluster (f + g) -> homogeneousFAF;

      correctness

      proof

        let w be Vector of V;

        set Ffg = ( FrFunctionalFAF ((f + g),w)), Ff = ( FrFunctionalFAF (f,w));

        set Fg = ( FrFunctionalFAF (g,w));

        let v be Vector of W, a be Scalar of V;

        

        thus (Ffg . (a * v)) = ((Ff + Fg) . (a * v)) by HTh13

        .= ((Ff . (a * v)) + (Fg . (a * v))) by HDef3

        .= ((a * (Ff . v)) + (Fg . (a * v))) by HDef8

        .= ((a * (Ff . v)) + (a * (Fg . v))) by HDef8

        .= (a * ((Ff . v) + (Fg . v)))

        .= (a * ((Ff + Fg) . v)) by HDef3

        .= (a * (Ffg . v)) by HTh13;

      end;

    end

    registration

      let V,W be non empty ModuleStr over INT.Ring ;

      let f be homogeneousSAF FrForm of V, W;

      let a be Element of F_Real ;

      cluster (a * f) -> homogeneousSAF;

      correctness

      proof

        let w be Vector of W;

        set Ffg = ( FrFunctionalSAF ((a * f),w)), Ff = ( FrFunctionalSAF (f,w));

        let v be Vector of V, b be Scalar of V;

        

        thus (Ffg . (b * v)) = ((a * Ff) . (b * v)) by HTh14

        .= (a * (Ff . (b * v))) by HDef6

        .= (a * (b * (Ff . v))) by HDef8

        .= (b * (a * (Ff . v)))

        .= (b * ((a * Ff) . v)) by HDef6

        .= (b * (Ffg . v)) by HTh14;

      end;

    end

    registration

      let V,W be non empty ModuleStr over INT.Ring ;

      let f be homogeneousFAF FrForm of V, W;

      let a be Element of F_Real ;

      cluster (a * f) -> homogeneousFAF;

      correctness

      proof

        let w be Vector of V;

        set Ffg = ( FrFunctionalFAF ((a * f),w)), Ff = ( FrFunctionalFAF (f,w));

        let v be Vector of W, b be Scalar of V;

        

        thus (Ffg . (b * v)) = ((a * Ff) . (b * v)) by HTh15

        .= (a * (Ff . (b * v))) by HDef6

        .= (a * (b * (Ff . v))) by HDef8

        .= (b * (a * (Ff . v)))

        .= (b * ((a * Ff) . v)) by HDef6

        .= (b * (Ffg . v)) by HTh15;

      end;

    end

    registration

      let V,W be non empty ModuleStr over INT.Ring ;

      let f be homogeneousSAF FrForm of V, W;

      cluster ( - f) -> homogeneousSAF;

      correctness ;

    end

    registration

      let V,W be non empty ModuleStr over INT.Ring ;

      let f be homogeneousFAF FrForm of V, W;

      cluster ( - f) -> homogeneousFAF;

      correctness ;

    end

    registration

      let V,W be non empty ModuleStr over INT.Ring ;

      let f,g be homogeneousSAF FrForm of V, W;

      cluster (f - g) -> homogeneousSAF;

      correctness ;

    end

    registration

      let V,W be non empty ModuleStr over INT.Ring ;

      let f,g be homogeneousFAF FrForm of V, W;

      cluster (f - g) -> homogeneousFAF;

      correctness ;

    end

    theorem :: ZMODLAT1:75

    

     HTh26: for V,W be non empty ModuleStr over INT.Ring , v,u be Vector of V, w be Vector of W, f be FrForm of V, W st f is additiveSAF holds (f . ((v + u),w)) = ((f . (v,w)) + (f . (u,w)))

    proof

      let V,W be non empty ModuleStr over INT.Ring ;

      let v,w be Vector of V, y be Vector of W, f be FrForm of V, W;

      set F = ( FrFunctionalSAF (f,y));

      assume f is additiveSAF;

      then

       A1: F is additive;

      

      thus (f . ((v + w),y)) = (F . (v + w)) by HTh9

      .= ((F . v) + (F . w)) by A1

      .= ((f . (v,y)) + (F . w)) by HTh9

      .= ((f . (v,y)) + (f . (w,y))) by HTh9;

    end;

    theorem :: ZMODLAT1:76

    

     HTh27: for V,W be non empty ModuleStr over INT.Ring , v be Vector of V, u,w be Vector of W, f be FrForm of V, W st f is additiveFAF holds (f . (v,(u + w))) = ((f . (v,u)) + (f . (v,w)))

    proof

      let V,W be non empty ModuleStr over INT.Ring ;

      let v be Vector of V, y,z be Vector of W, f be FrForm of V, W;

      set F = ( FrFunctionalFAF (f,v));

      assume f is additiveFAF;

      then

       A1: F is additive;

      

      thus (f . (v,(y + z))) = (F . (y + z)) by HTh8

      .= ((F . y) + (F . z)) by A1

      .= ((f . (v,y)) + (F . z)) by HTh8

      .= ((f . (v,y)) + (f . (v,z))) by HTh8;

    end;

    theorem :: ZMODLAT1:77

    

     HTh28: for V,W be non empty ModuleStr over INT.Ring , v,u be Vector of V, w,t be Vector of W, f be additiveSAF additiveFAF FrForm of V, W holds (f . ((v + u),(w + t))) = (((f . (v,w)) + (f . (v,t))) + ((f . (u,w)) + (f . (u,t))))

    proof

      let V,W be non empty ModuleStr over INT.Ring ;

      let v,w be Vector of V, y,z be Vector of W, f be additiveSAF additiveFAF FrForm of V, W;

      set v1 = (f . (v,y)), v3 = (f . (v,z)), v4 = (f . (w,y)), v5 = (f . (w,z));

      

      thus (f . ((v + w),(y + z))) = ((f . (v,(y + z))) + (f . (w,(y + z)))) by HTh26

      .= ((v1 + v3) + (f . (w,(y + z)))) by HTh27

      .= ((v1 + v3) + (v4 + v5)) by HTh27;

    end;

    theorem :: ZMODLAT1:78

    

     HTh29: for V,W be right_zeroed non empty ModuleStr over INT.Ring , f be additiveFAF FrForm of V, W, v be Vector of V holds (f . (v,( 0. W))) = ( 0. INT.Ring )

    proof

      let V,W be right_zeroed non empty ModuleStr over INT.Ring ;

      let f be additiveFAF FrForm of V, W, v be Vector of V;

      (f . (v,( 0. W))) = (f . (v,(( 0. W) + ( 0. W)))) by RLVECT_1:def 4

      .= ((f . (v,( 0. W))) + (f . (v,( 0. W)))) by HTh27;

      hence thesis;

    end;

    theorem :: ZMODLAT1:79

    

     HTh30: for V,W be right_zeroed non empty ModuleStr over INT.Ring , f be additiveSAF FrForm of V, W, w be Vector of W holds (f . (( 0. V),w)) = ( 0. INT.Ring )

    proof

      let V,W be right_zeroed non empty ModuleStr over INT.Ring ;

      let f be additiveSAF FrForm of V, W, v be Vector of W;

      (f . (( 0. V),v)) = (f . ((( 0. V) + ( 0. V)),v)) by RLVECT_1:def 4

      .= ((f . (( 0. V),v)) + (f . (( 0. V),v))) by HTh26;

      hence thesis;

    end;

    theorem :: ZMODLAT1:80

    

     HTh31: for V,W be non empty ModuleStr over INT.Ring , v be Vector of V, w be Vector of W, a be Element of INT.Ring , f be FrForm of V, W st f is homogeneousSAF holds (f . ((a * v),w)) = (a * (f . (v,w)))

    proof

      let V,W be non empty ModuleStr over INT.Ring ;

      let v be Vector of V, y be Vector of W, r be Element of INT.Ring , f be FrForm of V, W;

      set F = ( FrFunctionalSAF (f,y));

      assume f is homogeneousSAF;

      then

       A1: F is homogeneous;

      

      thus (f . ((r * v),y)) = (F . (r * v)) by HTh9

      .= (r * (F . v)) by A1

      .= (r * (f . (v,y))) by HTh9;

    end;

    theorem :: ZMODLAT1:81

    

     HTh32: for V,W be non empty ModuleStr over INT.Ring , v be Vector of V, w be Vector of W, a be Element of INT.Ring , f be FrForm of V, W st f is homogeneousFAF holds (f . (v,(a * w))) = (a * (f . (v,w)))

    proof

      let V,W be non empty ModuleStr over INT.Ring ;

      let v be Vector of V, y be Vector of W, r be Element of INT.Ring , f be FrForm of V, W;

      set F = ( FrFunctionalFAF (f,v));

      assume f is homogeneousFAF;

      then

       A1: F is homogeneous;

      

      thus (f . (v,(r * y))) = (F . (r * y)) by HTh8

      .= (r * (F . y)) by A1

      .= (r * (f . (v,y))) by HTh8;

    end;

    theorem :: ZMODLAT1:82

    for V,W be add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital non empty ModuleStr over INT.Ring , f be homogeneousSAF FrForm of V, W, w be Vector of W holds (f . (( 0. V),w)) = ( 0. F_Real )

    proof

      let V,W be add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital non empty ModuleStr over INT.Ring ;

      let f be homogeneousSAF FrForm of V, W, v be Vector of W;

      

      thus (f . (( 0. V),v)) = (f . ((( 0. INT.Ring ) * ( 0. V)),v)) by VECTSP10: 1

      .= (( 0. INT.Ring ) * (f . (( 0. V),v))) by HTh31

      .= ( 0. F_Real );

    end;

    theorem :: ZMODLAT1:83

    for V,W be add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital non empty ModuleStr over INT.Ring , f be homogeneousFAF FrForm of V, W, v be Vector of V holds (f . (v,( 0. W))) = ( 0. F_Real )

    proof

      let V,W be add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital non empty ModuleStr over INT.Ring ;

      let f be homogeneousFAF FrForm of V, W, v be Vector of V;

      

      thus (f . (v,( 0. W))) = (f . (v,(( 0. INT.Ring ) * ( 0. W)))) by VECTSP10: 1

      .= (( 0. INT.Ring ) * (f . (v,( 0. W)))) by HTh32

      .= ( 0. F_Real );

    end;

    theorem :: ZMODLAT1:84

    

     HTh35: for V,W be Z_Module, v,u be Vector of V, w be Vector of W, f be additiveSAF homogeneousSAF FrForm of V, W holds (f . ((v - u),w)) = ((f . (v,w)) - (f . (u,w)))

    proof

      let V,W be Z_Module, v,w be Vector of V, y be Vector of W;

      let f be additiveSAF homogeneousSAF FrForm of V, W;

      

      thus (f . ((v - w),y)) = ((f . (v,y)) + (f . (( - w),y))) by HTh26

      .= ((f . (v,y)) + (f . ((( - ( 1. INT.Ring )) * w),y))) by VECTSP_1: 14

      .= ((f . (v,y)) + (( - ( 1. INT.Ring )) * (f . (w,y)))) by HTh31

      .= ((f . (v,y)) - (f . (w,y)));

    end;

    theorem :: ZMODLAT1:85

    

     HTh36: for V,W be Z_Module, v be Vector of V, w,t be Vector of W, f be additiveFAF homogeneousFAF FrForm of V, W holds (f . (v,(w - t))) = ((f . (v,w)) - (f . (v,t)))

    proof

      let V,W be Z_Module, v be Vector of V, y,z be Vector of W, f be additiveFAF homogeneousFAF FrForm of V, W;

      

      thus (f . (v,(y - z))) = ((f . (v,y)) + (f . (v,( - z)))) by HTh27

      .= ((f . (v,y)) + (f . (v,(( - ( 1. INT.Ring )) * z)))) by VECTSP_1: 14

      .= ((f . (v,y)) + (( - ( 1. INT.Ring )) * (f . (v,z)))) by HTh32

      .= ((f . (v,y)) - (f . (v,z)));

    end;

    theorem :: ZMODLAT1:86

    

     HTh37: for V,W be Z_Module, v,u be Vector of V, w,t be Vector of W, f be bilinear-FrForm of V, W holds (f . ((v - u),(w - t))) = (((f . (v,w)) - (f . (v,t))) - ((f . (u,w)) - (f . (u,t))))

    proof

      let V,W be Z_Module;

      let v,w be Vector of V, y,z be Vector of W, f be bilinear-FrForm of V, W;

      set v1 = (f . (v,y)), v3 = (f . (v,z)), v4 = (f . (w,y)), v5 = (f . (w,z));

      

      thus (f . ((v - w),(y - z))) = ((f . (v,(y - z))) - (f . (w,(y - z)))) by HTh35

      .= ((v1 - v3) - (f . (w,(y - z)))) by HTh36

      .= ((v1 - v3) - (v4 - v5)) by HTh36;

    end;

    theorem :: ZMODLAT1:87

    for V,W be add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital non empty ModuleStr over INT.Ring , v,u be Vector of V, w,t be Vector of W, a,b be Element of INT.Ring , f be bilinear-FrForm of V, W holds (f . ((v + (a * u)),(w + (b * t)))) = (((f . (v,w)) + (b * (f . (v,t)))) + ((a * (f . (u,w))) + (a * (b * (f . (u,t))))))

    proof

      let V,W be add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital non empty ModuleStr over INT.Ring , v,w be Vector of V, y,z be Vector of W, a,b be Element of INT.Ring ;

      let f be bilinear-FrForm of V, W;

      set v1 = (f . (v,y)), v3 = (f . (v,z)), v4 = (f . (w,y)), v5 = (f . (w,z));

      

      thus (f . ((v + (a * w)),(y + (b * z)))) = ((v1 + (f . (v,(b * z)))) + ((f . ((a * w),y)) + (f . ((a * w),(b * z))))) by HTh28

      .= ((v1 + (b * v3)) + ((f . ((a * w),y)) + (f . ((a * w),(b * z))))) by HTh32

      .= ((v1 + (b * v3)) + ((a * v4) + (f . ((a * w),(b * z))))) by HTh31

      .= ((v1 + (b * v3)) + ((a * v4) + (a * (f . (w,(b * z)))))) by HTh31

      .= ((v1 + (b * v3)) + ((a * v4) + (a * (b * v5)))) by HTh32;

    end;

    theorem :: ZMODLAT1:88

    for V,W be Z_Module, v,u be Vector of V, w,t be Vector of W, a,b be Element of INT.Ring , f be bilinear-FrForm of V, W holds (f . ((v - (a * u)),(w - (b * t)))) = (((f . (v,w)) - (b * (f . (v,t)))) - ((a * (f . (u,w))) - (a * (b * (f . (u,t))))))

    proof

      let V,W be Z_Module, v,w be Vector of V, y,z be Vector of W, a,b be Element of INT.Ring , f be bilinear-FrForm of V, W;

      set v1 = (f . (v,y)), v3 = (f . (v,z)), v4 = (f . (w,y)), v5 = (f . (w,z));

      

      thus (f . ((v - (a * w)),(y - (b * z)))) = ((v1 - (f . (v,(b * z)))) - ((f . ((a * w),y)) - (f . ((a * w),(b * z))))) by HTh37

      .= ((v1 - (b * v3)) - ((f . ((a * w),y)) - (f . ((a * w),(b * z))))) by HTh32

      .= ((v1 - (b * v3)) - ((a * v4) - (f . ((a * w),(b * z))))) by HTh31

      .= ((v1 - (b * v3)) - ((a * v4) - (a * (f . (w,(b * z)))))) by HTh31

      .= ((v1 - (b * v3)) - ((a * v4) - (a * (b * v5)))) by HTh32;

    end;

    theorem :: ZMODLAT1:89

    for V,W be right_zeroed non empty ModuleStr over INT.Ring , f be FrForm of V, W st f is additiveFAF or f is additiveSAF holds f is constant iff for v be Vector of V, w be Vector of W holds (f . (v,w)) = ( 0. INT.Ring )

    proof

      let V,W be right_zeroed non empty ModuleStr over INT.Ring , f be FrForm of V, W;

      

       A1: ( dom f) = [:the carrier of V, the carrier of W:] by FUNCT_2:def 1;

      assume

       A2: f is additiveFAF or f is additiveSAF;

      hereby

        assume

         A3: f is constant;

        let v be Vector of V, w be Vector of W;

        per cases by A2;

          suppose

           A4: f is additiveFAF;

          

          thus (f . (v,w)) = (f . (v,( 0. W))) by A1, A3, BINOP_1: 19

          .= ( 0. INT.Ring ) by A4, HTh29;

        end;

          suppose

           A5: f is additiveSAF;

          

          thus (f . (v,w)) = (f . (( 0. V),w)) by A1, A3, BINOP_1: 19

          .= ( 0. INT.Ring ) by A5, HTh30;

        end;

      end;

      hereby

        assume

         A6: for v be Vector of V, w be Vector of W holds (f . (v,w)) = ( 0. INT.Ring );

        now

          let x,y be object such that

           A7: x in ( dom f) and

           A8: y in ( dom f);

          consider v be Vector of V, w be Vector of W such that

           A9: x = [v, w] by A7, DOMAIN_1: 1;

          consider s be Vector of V, t be Vector of W such that

           A10: y = [s, t] by A8, DOMAIN_1: 1;

          

          thus (f . x) = (f . (v,w)) by A9

          .= ( 0. INT.Ring ) by A6

          .= (f . (s,t)) by A6

          .= (f . y) by A10;

        end;

        hence f is constant by FUNCT_1:def 10;

      end;

    end;

    begin

    definition

      let V1,V2 be finite-rank free Z_Module;

      let b1 be OrdBasis of V1, b2 be OrdBasis of V2;

      let f be bilinear-FrForm of V1, V2;

      :: ZMODLAT1:def32

      func BilinearM (f,b1,b2) -> Matrix of ( len b1), ( len b2), F_Real means

      : defBilinearM: for i,j be Nat st i in ( dom b1) & j in ( dom b2) holds (it * (i,j)) = (f . ((b1 /. i),(b2 /. j)));

      existence

      proof

        deffunc F( Nat, Nat) = ( In ((f . ((b1 /. $1),(b2 /. $2))),the carrier of F_Real ));

        consider M be Matrix of ( len b1), ( len b2), F_Real such that

         A20: for i,j be Nat st [i, j] in ( Indices M) holds (M * (i,j)) = F(i,j) from MATRIX_0:sch 1;

        take M;

        thus for i,j be Nat st i in ( dom b1) & j in ( dom b2) holds (M * (i,j)) = (f . ((b1 /. i),(b2 /. j)))

        proof

          let i,j be Nat;

          assume

           A21: i in ( dom b1) & j in ( dom b2);

          ( len b1) <> 0

          proof

            assume ( len b1) = 0 ;

            then ( Seg ( len b1)) = {} ;

            hence contradiction by A21, FINSEQ_1:def 3;

          end;

          

          then ( Indices M) = [:( Seg ( len b1)), ( Seg ( len b2)):] by MATRIX_0: 23

          .= [:( dom b1), ( Seg ( len b2)):] by FINSEQ_1:def 3

          .= [:( dom b1), ( dom b2):] by FINSEQ_1:def 3;

          then [i, j] in ( Indices M) by A21, ZFMISC_1: 87;

          then (M * (i,j)) = F(i,j) by A20;

          hence (M * (i,j)) = (f . ((b1 /. i),(b2 /. j)));

        end;

      end;

      uniqueness

      proof

        let M1,M2 be Matrix of ( len b1), ( len b2), F_Real ;

        assume that

         A22: for i,j be Nat st i in ( dom b1) & j in ( dom b2) holds (M1 * (i,j)) = (f . ((b1 /. i),(b2 /. j))) and

         A23: for i,j be Nat st i in ( dom b1) & j in ( dom b2) holds (M2 * (i,j)) = (f . ((b1 /. i),(b2 /. j)));

        now

          let i,j be Nat;

          assume

           A25: [i, j] in ( Indices M1);

          then ( len b1) <> 0 by MATRIX_0: 22;

          

          then ( Indices M1) = [:( Seg ( len b1)), ( Seg ( len b2)):] by MATRIX_0: 23

          .= [:( dom b1), ( Seg ( len b2)):] by FINSEQ_1:def 3

          .= [:( dom b1), ( dom b2):] by FINSEQ_1:def 3;

          then

           A26: i in ( dom b1) & j in ( dom b2) by A25, ZFMISC_1: 87;

          

          thus (M1 * (i,j)) = (f . ((b1 /. i),(b2 /. j))) by A22, A26

          .= (M2 * (i,j)) by A26, A23;

        end;

        hence thesis by MATRIX_0: 27;

      end;

    end

    theorem :: ZMODLAT1:90

    

     LMThMBF1X0: for V be finite-rank free Z_Module, F be linear-FrFunctional of V, y be FinSequence of V, x be FinSequence of INT.Ring , X,Y be FinSequence of F_Real st X = x & ( len y) = ( len x) & ( len X) = ( len Y) & (for k be Nat st k in ( Seg ( len x)) holds (Y . k) = (F . (y /. k))) holds (X "*" Y) = (F . ( Sum ( lmlt (x,y))))

    proof

      let V be finite-rank free Z_Module, F be linear-FrFunctional of V;

      defpred P[ FinSequence of V] means for x be FinSequence of INT.Ring , X,Y be FinSequence of F_Real st X = x & ( len $1) = ( len x) & ( len X) = ( len Y) & (for k be Nat st k in ( Seg ( len x)) holds (Y . k) = (F . ($1 /. k))) holds (X "*" Y) = (F . ( Sum ( lmlt (x,$1))));

      

       A2: for y be FinSequence of V holds for w be Element of V st P[y] holds P[(y ^ <*w*>)]

      proof

        let y be FinSequence of V;

        let w be Element of V such that

         P1: for x be FinSequence of INT.Ring , X,Y be FinSequence of F_Real st X = x & ( len y) = ( len x) & ( len X) = ( len Y) & (for k be Nat st k in ( Seg ( len x)) holds (Y . k) = (F . (y /. k))) holds (X "*" Y) = (F . ( Sum ( lmlt (x,y))));

        thus for x be FinSequence of INT.Ring , X,Y be FinSequence of F_Real st X = x & ( len (y ^ <*w*>)) = ( len x) & ( len X) = ( len Y) & (for k be Nat st k in ( Seg ( len x)) holds (Y . k) = (F . ((y ^ <*w*>) /. k))) holds (X "*" Y) = (F . ( Sum ( lmlt (x,(y ^ <*w*>)))))

        proof

          let x be FinSequence of INT.Ring , X,Y be FinSequence of F_Real ;

          assume that

           R1: X = x and

           R2: ( len (y ^ <*w*>)) = ( len x) and

           R3: ( len X) = ( len Y) and

           R4: for k be Nat st k in ( Seg ( len x)) holds (Y . k) = (F . ((y ^ <*w*>) /. k));

          

           X1: F is additive;

          

           X2: F is homogeneous;

          set n = ( len y);

          set X0 = (X | n);

          set Y0 = (Y | n);

          set x0 = (x | n);

          

           Q0: ( len (y ^ <*w*>)) = (( len y) + ( len <*w*>)) by FINSEQ_1: 22

          .= (n + 1) by FINSEQ_1: 39;

          

           LN4: ( len x0) = n by Q0, R2, FINSEQ_1: 59, NAT_1: 11;

          

           LN5: ( len X0) = n by Q0, R1, R2, FINSEQ_1: 59, NAT_1: 11;

          

           LN6: ( len Y0) = n by Q0, R1, R2, R3, FINSEQ_1: 59, NAT_1: 11;

          

           LN7: (n + 1) in ( Seg (n + 1)) by FINSEQ_1: 4;

          

           Q2: ( len y) = ( len x0) by Q0, R2, FINSEQ_1: 59, NAT_1: 11;

          

           Q3: ( len X0) = ( len Y0) by LN5, Q0, R1, R2, R3, FINSEQ_1: 59, NAT_1: 11;

          for k be Nat st k in ( Seg ( len x0)) holds (Y0 . k) = (F . (y /. k))

          proof

            let k be Nat;

            assume

             Q31: k in ( Seg ( len x0));

            then

             Q34: k in ( dom y) by LN4, FINSEQ_1:def 3;

            

             Q32: ( Seg ( len x0)) c= ( Seg ( len x)) by FINSEQ_3: 18, Q0, R2, LN4;

            then k in ( Seg ( len x)) by Q31;

            then

             Q33: k in ( dom (y ^ <*w*>)) by R2, FINSEQ_1:def 3;

            

             Q35: ((y ^ <*w*>) /. k) = ((y ^ <*w*>) . k) by Q33, PARTFUN1:def 6

            .= (y . k) by FINSEQ_1:def 7, Q34

            .= (y /. k) by Q34, PARTFUN1:def 6;

            

            thus (Y0 . k) = (Y . k) by LN4, Q31, FUNCT_1: 49

            .= (F . (y /. k)) by R4, Q31, Q32, Q35;

          end;

          then

           Q4: (X0 "*" Y0) = (F . ( Sum ( lmlt (x0,y)))) by R1, Q2, Q3, P1;

          

           Q51: (n + 1) in ( dom X) by LN7, Q0, R1, R2, FINSEQ_1:def 3;

          

           Q61: (n + 1) in ( dom Y) by LN7, Q0, R1, R2, R3, FINSEQ_1:def 3;

          

           Q71: (n + 1) in ( dom x) by LN7, Q0, R2, FINSEQ_1:def 3;

          

           Q9: (X /. (n + 1)) = (X . (n + 1)) by Q51, PARTFUN1:def 6

          .= (x /. (n + 1)) by R1, Q71, PARTFUN1:def 6;

          

           Q103: (n + 1) in ( dom (y ^ <*w*>)) by LN7, Q0, FINSEQ_1:def 3;

          

           Q102: ((y ^ <*w*>) /. (n + 1)) = ((y ^ <*w*>) . (n + 1)) by Q103, PARTFUN1:def 6

          .= w by FINSEQ_1: 42;

          (Y /. (n + 1)) = (Y . (n + 1)) by Q61, PARTFUN1:def 6

          .= (F . w) by Q0, Q102, R2, R4, FINSEQ_1: 4;

          then

           Q11: ((X /. (n + 1)) * (Y /. (n + 1))) = (F . ((x /. (n + 1)) * w)) by Q9, X2;

          ( len ( mlt (X,Y))) = (n + 1) by Q0, R1, R2, R3, MATRIX_3: 6;

          then

           Q85: ( dom ( mlt (X,Y))) = ( Seg (n + 1)) by FINSEQ_1:def 3;

          

           Q82: ( len ( mlt (X0,Y0))) = n by LN5, LN6, MATRIX_3: 6;

          ( len (( mlt (X0,Y0)) ^ <*((X /. (n + 1)) * (Y /. (n + 1)))*>)) = (( len ( mlt (X0,Y0))) + ( len <*((X /. (n + 1)) * (Y /. (n + 1)))*>)) by FINSEQ_1: 22

          .= (n + 1) by Q82, FINSEQ_1: 39;

          then

           DM1: ( dom ( mlt (X,Y))) = ( dom (( mlt (X0,Y0)) ^ <*((X /. (n + 1)) * (Y /. (n + 1)))*>)) by Q85, FINSEQ_1:def 3;

          for k be Nat st k in ( dom ( mlt (X,Y))) holds (( mlt (X,Y)) . k) = ((( mlt (X0,Y0)) ^ <*((X /. (n + 1)) * (Y /. (n + 1)))*>) . k)

          proof

            let k be Nat;

            assume

             V1: k in ( dom ( mlt (X,Y)));

            then

             V2: 1 <= k & k <= (n + 1) by Q85, FINSEQ_1: 1;

            set f = (( mlt (X0,Y0)) ^ <*((X /. (n + 1)) * (Y /. (n + 1)))*>);

            per cases ;

              suppose k <= n;

              then

               V3: k in ( Seg n) by V2;

              then

               V4: k in ( dom ( mlt (X0,Y0))) by Q82, FINSEQ_1:def 3;

              

               V5: k in ( dom X0) by LN5, V3, FINSEQ_1:def 3;

              

               V6: k in ( dom Y0) by LN6, V3, FINSEQ_1:def 3;

              (X0 . k) in ( rng X0) by V5, FUNCT_1: 3;

              then

              reconsider X0k = (X0 . k) as Element of F_Real ;

              (Y0 . k) in ( rng Y0) by V6, FUNCT_1: 3;

              then

              reconsider Y0k = (Y0 . k) as Element of F_Real ;

              k in ( dom X) by V1, Q0, Q85, R1, R2, FINSEQ_1:def 3;

              then (X . k) in ( rng X) by FUNCT_1: 3;

              then

              reconsider Xk = (X . k) as Element of F_Real ;

              k in ( dom Y) by V1, Q0, Q85, R1, R2, R3, FINSEQ_1:def 3;

              then (Y . k) in ( rng Y) by FUNCT_1: 3;

              then

              reconsider Yk = (Y . k) as Element of F_Real ;

              (f . k) = (( mlt (X0,Y0)) . k) by V4, FINSEQ_1:def 7

              .= (X0k * Y0k) by V4, FVSUM_1: 60

              .= ((X . k) * (Y0 . k)) by V5, FUNCT_1: 47

              .= (Xk * Yk) by V6, FUNCT_1: 47

              .= (( mlt (X,Y)) . k) by V1, FVSUM_1: 60;

              hence thesis;

            end;

              suppose not k <= n;

              then (n + 1) <= k by NAT_1: 13;

              then

               V8: k = (n + 1) by XXREAL_0: 1, V2;

              ( Seg 1) = ( dom <*((X /. (n + 1)) * (Y /. (n + 1)))*>) by FINSEQ_1: 38;

              then

               V10: 1 in ( dom <*((X /. (n + 1)) * (Y /. (n + 1)))*>);

              

               Q9: (X /. (n + 1)) = (X . (n + 1)) by Q51, PARTFUN1:def 6;

              then

              reconsider Xn = (X . (n + 1)) as Element of F_Real ;

              

               Q10: (Y /. (n + 1)) = (Y . (n + 1)) by Q61, PARTFUN1:def 6;

              then

              reconsider Yn = (Y . (n + 1)) as Element of F_Real ;

              (f . k) = ( <*((X /. (n + 1)) * (Y /. (n + 1)))*> . 1) by Q82, FINSEQ_1:def 7, V8, V10

              .= ((X /. (n + 1)) * (Y /. (n + 1))) by FINSEQ_1: 40

              .= (( mlt (X,Y)) . k) by Q9, Q10, V1, V8, FVSUM_1: 60;

              hence thesis;

            end;

          end;

          then

           Q8: ( mlt (X,Y)) = (( mlt (X0,Y0)) ^ <*((X /. (n + 1)) * (Y /. (n + 1)))*>) by DM1, FINSEQ_1: 13;

          

           QX121: ( dom x) = ( Seg (n + 1)) by Q0, R2, FINSEQ_1:def 3

          .= ( dom (y ^ <*w*>)) by Q0, FINSEQ_1:def 3;

          then

           Q121: ( dom ( lmlt (x,(y ^ <*w*>)))) = ( dom x) by ZMATRLIN: 13;

          ( dom x0) = ( Seg n) by FINSEQ_1:def 3, LN4

          .= ( dom y) by FINSEQ_1:def 3;

          then ( dom ( lmlt (x0,y))) = ( dom x0) by ZMATRLIN: 13;

          then

           Q124: ( dom ( lmlt (x0,y))) = ( Seg n) by LN4, FINSEQ_1:def 3;

          then

           Q125: ( len ( lmlt (x0,y))) = n by FINSEQ_1:def 3;

          ( len (( lmlt (x0,y)) ^ <*((x /. (n + 1)) * w)*>)) = (( len ( lmlt (x0,y))) + ( len <*((x /. (n + 1)) * w)*>)) by FINSEQ_1: 22

          .= (n + 1) by Q125, FINSEQ_1: 39;

          then ( dom (( lmlt (x0,y)) ^ <*((x /. (n + 1)) * w)*>)) = ( Seg (n + 1)) by FINSEQ_1:def 3;

          then

           DM1: ( dom ( lmlt (x,(y ^ <*w*>)))) = ( dom (( lmlt (x0,y)) ^ <*((x /. (n + 1)) * w)*>)) by Q0, Q121, R2, FINSEQ_1:def 3;

          for k be Nat st k in ( dom ( lmlt (x,(y ^ <*w*>)))) holds (( lmlt (x,(y ^ <*w*>))) . k) = ((( lmlt (x0,y)) ^ <*((x /. (n + 1)) * w)*>) . k)

          proof

            let k be Nat;

            assume

             V1: k in ( dom ( lmlt (x,(y ^ <*w*>))));

            then

             V0: k in ( Seg (n + 1)) by Q121, Q0, R2, FINSEQ_1:def 3;

            then

             V2: 1 <= k & k <= (n + 1) by FINSEQ_1: 1;

            set f = (( lmlt (x0,y)) ^ <*((x /. (n + 1)) * w)*>);

            per cases ;

              suppose

               VX3: k <= n;

              then

               V3: k in ( Seg n) by V2;

              

               V5: k in ( dom x0) by V3, LN4, FINSEQ_1:def 3;

              

               V6: k in ( dom y) by V3, FINSEQ_1:def 3;

              ( rng x0) c= the carrier of INT.Ring ;

              then

              reconsider x0k = (x0 . k) as Element of INT.Ring by V5, FUNCT_1: 3;

              (y . k) in ( rng y) by V6, FUNCT_1: 3;

              then

              reconsider y0k = (y . k) as Element of V;

              

               XX2: k in ( dom x) by V1, QX121, ZMATRLIN: 13;

              ( rng x) c= the carrier of INT.Ring ;

              then

              reconsider xk = (x . k) as Element of INT.Ring by XX2, FUNCT_1: 3;

              k in ( dom (y ^ <*w*>)) by V0, Q0, FINSEQ_1:def 3;

              then ((y ^ <*w*>) . k) in ( rng (y ^ <*w*>)) by FUNCT_1: 3;

              then

              reconsider yk = ((y ^ <*w*>) . k) as Element of V;

              

               W: y0k = yk by V6, FINSEQ_1:def 7;

              (f . k) = (( lmlt (x0,y)) . k) by V3, Q124, FINSEQ_1:def 7

              .= (x0k * y0k) by V2, VX3, Q124, FUNCOP_1: 22, FINSEQ_1: 1

              .= (xk * y0k) by V5, FUNCT_1: 47

              .= (( lmlt (x,(y ^ <*w*>))) . k) by W, V1, FUNCOP_1: 22;

              hence thesis;

            end;

              suppose not k <= n;

              then (n + 1) <= k by NAT_1: 13;

              then

               V8: k = (n + 1) by XXREAL_0: 1, V2;

              ( Seg 1) = ( dom <*((x /. (n + 1)) * w)*>) by FINSEQ_1: 38;

              then

               V10: 1 in ( dom <*((x /. (n + 1)) * w)*>);

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

              then

               V11: 1 in ( dom <*w*>);

              

               Q9: (x /. (n + 1)) = (x . (n + 1)) by Q71, PARTFUN1:def 6;

              then

              reconsider xn = (x . (n + 1)) as Element of INT.Ring ;

              ((y ^ <*w*>) /. (n + 1)) = ((y ^ <*w*>) . (n + 1)) by Q103, PARTFUN1:def 6;

              then

              reconsider yn = ((y ^ <*w*>) . (n + 1)) as Element of V;

              

               Q11: ((y ^ <*w*>) . (n + 1)) = ( <*w*> . 1) by V11, FINSEQ_1:def 7

              .= w by FINSEQ_1: 40;

              (f . k) = ( <*((x /. (n + 1)) * w)*> . 1) by Q125, V8, V10, FINSEQ_1:def 7

              .= (xn * w) by Q9, FINSEQ_1: 40

              .= (( lmlt (x,(y ^ <*w*>))) . k) by Q11, V1, V8, FUNCOP_1: 22;

              hence thesis;

            end;

          end;

          then

           Q12: ( lmlt (x,(y ^ <*w*>))) = (( lmlt (x0,y)) ^ <*((x /. (n + 1)) * w)*>) by DM1, FINSEQ_1: 13;

          

          thus (X "*" Y) = (( Sum ( mlt (X0,Y0))) + ((X /. (n + 1)) * (Y /. (n + 1)))) by FVSUM_1: 71, Q8

          .= (F . (( Sum ( lmlt (x0,y))) + ((x /. (n + 1)) * w))) by Q4, Q11, X1

          .= (F . ( Sum ( lmlt (x,(y ^ <*w*>))))) by FVSUM_1: 71, Q12;

        end;

      end;

      

       A4: P[( <*> the carrier of V)]

      proof

        let x be FinSequence of INT.Ring , X,Y be FinSequence of F_Real ;

        assume that

         R1: X = x and

         R2: ( len ( <*> the carrier of V)) = ( len x) and ( len X) = ( len Y) and for k be Nat st k in ( Seg ( len x)) holds (Y . k) = (F . (( <*> the carrier of V) /. k));

        set y = ( <*> the carrier of V);

        

         Q2: X = ( <*> the carrier of F_Real ) by R1, R2;

        

         Q4: ( mlt (X,Y)) = ( <*> the carrier of F_Real ) by Q2;

        reconsider I0 = 0 as Element of INT.Ring ;

        

         X1: F is additive;

        

         X2: (F . ( 0. V)) = (F . (( 0. V) + ( 0. V)))

        .= ((F . ( 0. V)) + (F . ( 0. V))) by X1;

        

        thus (X "*" Y) = ( 0. F_Real ) by Q4, RLVECT_1: 43

        .= (F . ( Sum ( lmlt (x,y)))) by X2, RLVECT_1: 43;

      end;

      for p be FinSequence of V holds P[p] from FINSEQ_2:sch 2( A4, A2);

      hence thesis;

    end;

    theorem :: ZMODLAT1:91

    

     LMThMBF1X: for V1,V2 be finite-rank free Z_Module, b2 be OrdBasis of V2, b3 be OrdBasis of V2, f be bilinear-FrForm of V1, V2, v1 be Vector of V1, v2 be Vector of V2, X,Y be FinSequence of F_Real st ( len X) = ( len b2) & ( len Y) = ( len b2) & (for k be Nat st k in ( Seg ( len b2)) holds (Y . k) = (f . (v1,(b2 /. k)))) & X = (v2 |-- b2) holds (Y "*" X) = (f . (v1,v2))

    proof

      let V1,V2 be finite-rank free Z_Module, b2 be OrdBasis of V2, b3 be OrdBasis of V2, f be bilinear-FrForm of V1, V2, v1 be Vector of V1, v2 be Vector of V2, X,Y be FinSequence of F_Real ;

      assume that

       A1: ( len X) = ( len b2) and

       A2: ( len Y) = ( len b2) and

       A3: (for k be Nat st k in ( Seg ( len b2)) holds (Y . k) = (f . (v1,(b2 /. k)))) and

       A4: X = (v2 |-- b2);

      set x = (v2 |-- b2);

      

       P2: for k be Nat st k in ( Seg ( len x)) holds (Y . k) = (( FrFunctionalFAF (f,v1)) . (b2 /. k))

      proof

        let k be Nat;

        assume k in ( Seg ( len x));

        then (Y . k) = (f . (v1,(b2 /. k))) by A1, A3, A4;

        hence (Y . k) = (( FrFunctionalFAF (f,v1)) . (b2 /. k)) by HTh8;

      end;

      

      thus (Y "*" X) = (X "*" Y) by FVSUM_1: 90

      .= (( FrFunctionalFAF (f,v1)) . ( Sum ( lmlt ((v2 |-- b2),b2)))) by LMThMBF1X0, A1, A2, A4, P2

      .= (f . (v1,( Sum ( lmlt ((v2 |-- b2),b2))))) by HTh8

      .= (f . (v1,v2)) by ZMATRLIN: 30;

    end;

    theorem :: ZMODLAT1:92

    

     LMThMBF1Y: for V1,V2 be finite-rank free Z_Module, b1 be OrdBasis of V1, f be bilinear-FrForm of V1, V2, v1 be Vector of V1, v2 be Vector of V2, X,Y be FinSequence of F_Real st ( len X) = ( len b1) & ( len Y) = ( len b1) & (for k be Nat st k in ( Seg ( len b1)) holds (Y . k) = (f . ((b1 /. k),v2))) & X = (v1 |-- b1) holds (X "*" Y) = (f . (v1,v2))

    proof

      let V1,V2 be finite-rank free Z_Module, b1 be OrdBasis of V1, f be bilinear-FrForm of V1, V2, v1 be Vector of V1, v2 be Vector of V2, X,Y be FinSequence of F_Real ;

      assume that

       A1: ( len X) = ( len b1) and

       A2: ( len Y) = ( len b1) and

       A3: for k be Nat st k in ( Seg ( len b1)) holds (Y . k) = (f . ((b1 /. k),v2)) and

       A4: X = (v1 |-- b1);

      set x = (v1 |-- b1);

      

       P2: for k be Nat st k in ( Seg ( len x)) holds (Y . k) = (( FrFunctionalSAF (f,v2)) . (b1 /. k))

      proof

        let k be Nat;

        assume k in ( Seg ( len x));

        then (Y . k) = (f . ((b1 /. k),v2)) by A1, A3, A4;

        hence (Y . k) = (( FrFunctionalSAF (f,v2)) . (b1 /. k)) by HTh9;

      end;

      

      thus (X "*" Y) = (( FrFunctionalSAF (f,v2)) . ( Sum ( lmlt ((v1 |-- b1),b1)))) by LMThMBF1X0, A1, A2, A4, P2

      .= (f . (( Sum ( lmlt ((v1 |-- b1),b1))),v2)) by HTh9

      .= (f . (v1,v2)) by ZMATRLIN: 30;

    end;

    theorem :: ZMODLAT1:93

    

     INTTOREAL: for M be Matrix of INT.Ring holds M is Matrix of F_Real

    proof

      let M be Matrix of INT.Ring ;

      (the carrier of INT.Ring * ) c= (the carrier of F_Real * ) by NUMBERS: 15, FINSEQ_1: 62;

      then ( rng M) c= (the carrier of F_Real * );

      hence thesis by FINSEQ_1:def 4;

    end;

    definition

      let M be Matrix of INT.Ring ;

      :: ZMODLAT1:def33

      func inttorealM (M) -> Matrix of F_Real equals M;

      correctness by INTTOREAL;

    end

    definition

      let n,m be Nat;

      let M be Matrix of n, m, INT.Ring ;

      :: original: inttorealM

      redefine

      func inttorealM (M) -> Matrix of n, m, F_Real ;

      correctness

      proof

        

         B2: ( len M) = n by MATRIX_0: 25;

        per cases ;

          suppose

           X11: not 0 < n;

          then

           X1: n = 0 ;

          M = {} by X11, MATRIX_0: 25;

          hence ( inttorealM M) is Matrix of n, m, F_Real by X1, MATRIX_0: 13;

        end;

          suppose

           X2: 0 < n;

          then ( width M) = m by B2, MATRIX_0: 20;

          hence ( inttorealM M) is Matrix of n, m, F_Real by X2, B2, MATRIX_0: 20;

        end;

      end;

    end

    definition

      let n be Nat;

      let M be Matrix of n, INT.Ring ;

      :: original: inttorealM

      redefine

      func inttorealM (M) -> Matrix of n, F_Real ;

      correctness

      proof

        ( inttorealM M) is Matrix of n, n, F_Real ;

        hence thesis;

      end;

    end

    theorem :: ZMODLAT1:94

    

     MLT1: for m,l,n be Nat holds for S be Matrix of l, m, INT.Ring , T be Matrix of m, n, INT.Ring , S1 be Matrix of l, m, F_Real , T1 be Matrix of m, n, F_Real st S = S1 & T = T1 & 0 < l & 0 < m holds (S * T) = (S1 * T1)

    proof

      let m,l,n be Nat;

      let S be Matrix of l, m, INT.Ring , T be Matrix of m, n, INT.Ring , S1 be Matrix of l, m, F_Real , T1 be Matrix of m, n, F_Real ;

      assume

       AS: S = S1 & T = T1 & 0 < l & 0 < m;

      

       P1: ( len S) = l & ( width S) = m & ( Indices S) = [:( Seg l), ( Seg m):] by MATRIX_0: 23, AS;

      

       Q1: ( len S1) = l & ( width S1) = m & ( Indices S1) = [:( Seg l), ( Seg m):] by MATRIX_0: 23, AS;

      

       P2: ( len T) = m & ( width T) = n & ( Indices T) = [:( Seg m), ( Seg n):] by MATRIX_0: 23, AS;

      

       Q2: ( len T1) = m & ( width T1) = n & ( Indices T1) = [:( Seg m), ( Seg n):] by MATRIX_0: 23, AS;

      

       P3: ( len (S * T)) = ( len S) & ( width (S * T)) = ( width T) by P1, P2, MATRIX_3:def 4;

      

       Q3: ( len (S1 * T1)) = ( len S1) & ( width (S1 * T1)) = ( width T1) by Q1, Q2, MATRIX_3:def 4;

      reconsider ST = (S * T) as Matrix of l, n, INT.Ring by P3, AS, P1, P2, MATRIX_0: 20;

      reconsider S1T1 = (S1 * T1) as Matrix of l, n, F_Real by Q3, AS, Q1, Q2, MATRIX_0: 20;

      for i,j be Nat st [i, j] in ( Indices ST) holds (ST * (i,j)) = (S1T1 * (i,j))

      proof

        let i,j be Nat;

        assume

         A1: [i, j] in ( Indices ST);

        

         A2: ( Indices ST) = [:( Seg ( len ST)), ( Seg ( width ST)):] by FINSEQ_1:def 3

        .= ( Indices S1T1) by AS, P3, Q3, FINSEQ_1:def 3;

        i in ( dom ST) by A1, ZFMISC_1: 87;

        then i in ( Seg ( len ST)) by FINSEQ_1:def 3;

        then i in ( dom S) by FINSEQ_1:def 3, P3;

        then

         X1: ( Line (S,i)) = ( Line (S1,i)) by ZMATRLIN: 2, AS;

        j in ( Seg ( width T)) by A1, P3, ZFMISC_1: 87;

        then

         X2: ( Col (T,j)) = ( Col (T1,j)) by ZMATRLIN: 3, AS;

        

        thus (ST * (i,j)) = (( Line (S,i)) "*" ( Col (T,j))) by A1, P1, P2, MATRIX_3:def 4

        .= (( Line (S1,i)) "*" ( Col (T1,j))) by X1, X2, ZMATRLIN: 37

        .= (S1T1 * (i,j)) by A1, A2, Q1, Q2, MATRIX_3:def 4;

      end;

      hence thesis by AS, P3, Q3, ZMATRLIN: 4;

    end;

    theorem :: ZMODLAT1:95

    

     MLT2: for n be Nat holds ( 1. ( INT.Ring ,n)) = ( 1. ( F_Real ,n))

    proof

      let n be Nat;

      set M = ( 1. ( INT.Ring ,n));

      set L = ( 1. ( F_Real ,n));

      

       P1: ( len M) = n & ( width M) = n & ( Indices M) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      

       P2: ( len L) = n & ( width L) = n & ( Indices L) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      for i,j be Nat st [i, j] in ( Indices M) holds (M * (i,j)) = (L * (i,j))

      proof

        let i,j be Nat;

        assume

         AS: [i, j] in ( Indices M);

        per cases ;

          suppose

           Q1: i = j;

          

          hence (M * (i,j)) = ( 1. INT.Ring ) by MATRIX_1:def 3, AS

          .= ( 1. F_Real )

          .= (L * (i,j)) by Q1, MATRIX_1:def 3, P1, P2, AS;

        end;

          suppose

           Q2: i <> j;

          

          hence (M * (i,j)) = ( 0. INT.Ring ) by MATRIX_1:def 3, AS

          .= ( 0. F_Real )

          .= (L * (i,j)) by Q2, MATRIX_1:def 3, P1, P2, AS;

        end;

      end;

      hence thesis by P1, P2, ZMATRLIN: 4;

    end;

    theorem :: ZMODLAT1:96

    

     ThMBF1: for V1,V2 be finite-rank free Z_Module, b1 be OrdBasis of V1, b2 be OrdBasis of V2, b3 be OrdBasis of V2, f be bilinear-FrForm of V1, V2 st 0 < ( rank V1) holds ( BilinearM (f,b1,b3)) = (( BilinearM (f,b1,b2)) * (( inttorealM ( AutMt (( id V2),b3,b2))) @ ))

    proof

      let V1,V2 be finite-rank free Z_Module, b1 be OrdBasis of V1, b2 be OrdBasis of V2, b3 be OrdBasis of V2, f be bilinear-FrForm of V1, V2;

      set I = ( inttorealM ( AutMt (( id V2),b3,b2)));

      assume

       AS: 0 < ( rank V1);

      set n = ( len b2);

      

       A2: ( len b2) = ( rank V2) by ZMATRLIN: 49;

      

       A3: ( len b3) = ( rank V2) by ZMATRLIN: 49;

      reconsider IM1 = ( AutMt (( id V2),b3,b2)) as Matrix of n, INT.Ring by ZMATRLIN: 50, A2;

      reconsider M1 = ( inttorealM (IM1 @ )) as Matrix of n, F_Real ;

      set M2 = (( BilinearM (f,b1,b2)) * M1);

      

       B1: ( len M1) = n & ( width M1) = n & ( Indices M1) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      

       F1: ( len IM1) = n & ( width IM1) = n & ( Indices IM1) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

      

       B2: 0 < ( len b1) by AS, ZMATRLIN: 49;

      then

       B3: ( len ( BilinearM (f,b1,b2))) = ( len b1) & ( width ( BilinearM (f,b1,b2))) = ( len b2) by MATRIX_0: 23;

      

       C1: ( width ( BilinearM (f,b1,b2))) = ( len M1) by B1, B2, MATRIX_0: 23;

      

       X0: ( len M2) = ( len b1) & ( width M2) = n by B1, B3, MATRIX_3:def 4;

      then

      reconsider M2 as Matrix of ( len b1), n, F_Real by B2, MATRIX_0: 20;

      set FM1 = M1;

      set FBM = ( BilinearM (f,b1,b2));

      

       X1: ( len ( BilinearM (f,b1,b3))) = ( len M2) & ( width ( BilinearM (f,b1,b3))) = ( width M2) by A2, A3, B2, X0, MATRIX_0: 23;

      

       X2: M1 = (I @ ) by ZMATRLIN: 6;

      for i,j be Nat st [i, j] in ( Indices ( BilinearM (f,b1,b3))) holds (( BilinearM (f,b1,b3)) * (i,j)) = (M2 * (i,j))

      proof

        let i,j be Nat;

        assume [i, j] in ( Indices ( BilinearM (f,b1,b3)));

        then

         B6: [i, j] in [:( Seg ( len b1)), ( Seg ( len b3)):] by B2, MATRIX_0: 23;

        then

         B7: i in ( Seg ( len b1)) & j in ( Seg ( len b3)) by ZFMISC_1: 87;

        then

         B8: i in ( dom b1) & j in ( dom b3) by FINSEQ_1:def 3;

        then

         B9: (( BilinearM (f,b1,b3)) * (i,j)) = (f . ((b1 /. i),(b3 /. j))) by defBilinearM;

         [i, j] in ( Indices M2) by B2, B6, A2, A3, MATRIX_0: 23;

        then

         B11: (M2 * (i,j)) = (( Line (FBM,i)) "*" ( Col (FM1,j))) by C1, MATRIX_3:def 4;

        

         B12: ( len ( Line (FBM,i))) = ( len b2) by B3, MATRIX_0:def 7;

         B13:

        now

          let k be Nat;

          assume

           B131: k in ( Seg ( len b2));

          then

           B132: k in ( Seg ( width FBM)) by B2, MATRIX_0: 23;

          

           B81: k in ( dom b2) by FINSEQ_1:def 3, B131;

          

          thus (( Line (FBM,i)) . k) = (FBM * (i,k)) by B132, MATRIX_0:def 7

          .= (f . ((b1 /. i),(b2 /. k))) by B8, B81, defBilinearM;

        end;

        

         B14: ( len ( Col (FM1,j))) = ( len b2) by B1, MATRIX_0:def 8;

        

         B135: j in ( Seg n) by B6, A2, A3, ZFMISC_1: 87;

         B15:

        now

          let k be Nat;

          assume 1 <= k & k <= ( len ( Col (FM1,j)));

          then

           B131: k in ( Seg ( len b2)) by B14;

          then

           B132: k in ( dom FM1) by B1, FINSEQ_1:def 3;

          

           B132A: j in ( dom IM1) by B135, F1, FINSEQ_1:def 3;

          

           Y1: [j, k] in ( Indices IM1) by F1, B131, B135, ZFMISC_1: 87;

          then

          consider p be FinSequence of INT such that

           B133: p = (IM1 . j) & (IM1 * (j,k)) = (p . k) by MATRIX_0:def 5;

          

           B81A: j in ( dom b3) by B7, FINSEQ_1:def 3;

          

           Y2: [k, j] in ( Indices (IM1 @ )) by Y1, MATRIX_0:def 6;

          

           X0: (( Col (FM1,j)) . k) = (FM1 * (k,j)) by B132, MATRIX_0:def 8

          .= ((IM1 @ ) * (k,j)) by Y2, ZMATRLIN: 1

          .= (( AutMt (( id V2),b3,b2)) * (j,k)) by Y1, MATRIX_0:def 6;

          (IM1 . j) = (( AutMt (( id V2),b3,b2)) /. j) by B132A, PARTFUN1:def 6

          .= ((( id V2) . (b3 /. j)) |-- b2) by B81A, ZMATRLIN:def 8;

          hence (( Col (FM1,j)) . k) = (((b3 /. j) |-- b2) . k) by B133, X0;

        end;

        ( len ( Col (FM1,j))) = ( len ((b3 /. j) |-- b2)) by B14, ZMATRLIN:def 7;

        hence thesis by B9, B11, B12, B13, B14, B15, LMThMBF1X, FINSEQ_1:def 17;

      end;

      hence thesis by ZMATRLIN: 4, X1, X2;

    end;

    theorem :: ZMODLAT1:97

    

     ThMBF2: for V1,V2 be finite-rank free Z_Module, b1 be OrdBasis of V1, b2 be OrdBasis of V2, b3 be OrdBasis of V1, f be bilinear-FrForm of V1, V2 st 0 < ( rank V1) holds ( BilinearM (f,b3,b2)) = (( inttorealM ( AutMt (( id V1),b3,b1))) * ( BilinearM (f,b1,b2)))

    proof

      let V1,V2 be finite-rank free Z_Module, b1 be OrdBasis of V1, b2 be OrdBasis of V2, b3 be OrdBasis of V1, f be bilinear-FrForm of V1, V2;

      assume

       AS: 0 < ( rank V1);

      set I = ( inttorealM ( AutMt (( id V1),b3,b1)));

      set n = ( len b3);

      

       A1: ( len b1) = ( rank V1) by ZMATRLIN: 49;

      

       A3: ( len b3) = ( rank V1) by ZMATRLIN: 49;

      reconsider IM1 = ( AutMt (( id V1),b3,b1)) as Matrix of n, INT.Ring by ZMATRLIN: 50, A3;

      reconsider M1 = ( inttorealM IM1) as Matrix of n, F_Real ;

      set M2 = (M1 * ( BilinearM (f,b1,b2)));

      

       B1: ( len M1) = n & ( width M1) = n & ( Indices M1) = [:( Seg n), ( Seg n):] by MATRIX_0: 24;

       0 < ( len b1) by AS, ZMATRLIN: 49;

      then

       B3: ( len ( BilinearM (f,b1,b2))) = ( len b1) & ( width ( BilinearM (f,b1,b2))) = ( len b2) by MATRIX_0: 23;

      then

       X0: ( len M2) = n & ( width M2) = ( len b2) by A1, A3, B1, MATRIX_3:def 4;

      then

      reconsider M2 as Matrix of n, ( len b2), F_Real by A3, AS, MATRIX_0: 20;

      set FM1 = M1;

      set FBM = ( BilinearM (f,b1,b2));

      

       X1: ( len ( BilinearM (f,b3,b2))) = ( len M2) & ( width ( BilinearM (f,b3,b2))) = ( width M2) by AS, A3, X0, MATRIX_0: 23;

      for i,j be Nat st [i, j] in ( Indices ( BilinearM (f,b3,b2))) holds (( BilinearM (f,b3,b2)) * (i,j)) = (M2 * (i,j))

      proof

        let i,j be Nat;

        assume [i, j] in ( Indices ( BilinearM (f,b3,b2)));

        then

         B6: [i, j] in [:( Seg ( len b3)), ( Seg ( len b2)):] by AS, A3, MATRIX_0: 23;

        then i in ( Seg ( len b3)) & j in ( Seg ( len b2)) by ZFMISC_1: 87;

        then

         B8: i in ( dom b3) & j in ( dom b2) by FINSEQ_1:def 3;

        then

         B9: (( BilinearM (f,b3,b2)) * (i,j)) = (f . ((b3 /. i),(b2 /. j))) by defBilinearM;

         [i, j] in ( Indices M2) by AS, A3, B6, MATRIX_0: 23;

        then

         B11: (M2 * (i,j)) = (( Line (FM1,i)) "*" ( Col (FBM,j))) by A1, A3, B1, B3, MATRIX_3:def 4;

        

         B12: ( len ( Line (FM1,i))) = ( len b3) by B1, MATRIX_0:def 7;

        

         B14: ( len ( Col (FBM,j))) = ( len b3) by B3, A1, A3, MATRIX_0:def 8;

         B13:

        now

          let k be Nat;

          assume

           B131: k in ( Seg ( len b1));

          then

           B132: k in ( dom FBM) by B3, FINSEQ_1:def 3;

          

           B81: k in ( dom b1) by FINSEQ_1:def 3, B131;

          

          thus (( Col (FBM,j)) . k) = (FBM * (k,j)) by B132, MATRIX_0:def 8

          .= (f . ((b1 /. k),(b2 /. j))) by B8, B81, defBilinearM;

        end;

        

         B135: i in ( Seg n) by B6, ZFMISC_1: 87;

        then

         B135A: i in ( dom M1) by B1, FINSEQ_1:def 3;

        

         B136: i in ( dom b3) by B135, FINSEQ_1:def 3;

         B15:

        now

          let k be Nat;

          assume

           BX131: 1 <= k & k <= ( len ( Line (FM1,i)));

          then

           B131: k in ( Seg ( len b1)) by B12, A1, A3;

          

           XX1: [i, k] in ( Indices M1) by A1, A3, B1, B131, B135, ZFMISC_1: 87;

          

           X0: (( Line (FM1,i)) . k) = (FM1 * (i,k)) by B1, B12, BX131, FINSEQ_1: 1, MATRIX_0:def 7

          .= (( AutMt (( id V1),b3,b1)) * (i,k)) by XX1, ZMATRLIN: 1;

           [i, k] in ( Indices IM1) by A1, A3, B1, B131, B135, ZFMISC_1: 87;

          then

           XX3: ex p be FinSequence of INT.Ring st p = (IM1 . i) & (IM1 * (i,k)) = (p . k) by MATRIX_0:def 5;

          (IM1 . i) = (( AutMt (( id V1),b3,b1)) /. i) by B135A, PARTFUN1:def 6

          .= ((( id V1) . (b3 /. i)) |-- b1) by B136, ZMATRLIN:def 8

          .= ((b3 /. i) |-- b1);

          hence (( Line (FM1,i)) . k) = (((b3 /. i) |-- b1) . k) by X0, XX3;

        end;

        ( len ( Line (FM1,i))) = ( len ((b3 /. i) |-- b1)) by A1, A3, B12, ZMATRLIN:def 7;

        hence thesis by A1, A3, B9, B11, B12, B13, B14, B15, LMThMBF1Y, FINSEQ_1:def 17;

      end;

      hence thesis by X1, ZMATRLIN: 4;

    end;

    theorem :: ZMODLAT1:98

    

     ThMBF3: for V be finite-rank free Z_Module, b1,b2 be OrdBasis of V, f be bilinear-FrForm of V, V st 0 < ( rank V) holds ( BilinearM (f,b2,b2)) = ((( inttorealM ( AutMt (( id V),b2,b1))) * ( BilinearM (f,b1,b1))) * (( inttorealM ( AutMt (( id V),b2,b1))) @ ))

    proof

      let V be finite-rank free Z_Module, b1,b2 be OrdBasis of V, f be bilinear-FrForm of V, V;

      set I = ( inttorealM ( AutMt (( id V),b2,b1)));

      assume

       AS: 0 < ( rank V);

      set n = ( len b1);

      

       A1: ( len b1) = ( rank V) by ZMATRLIN: 49;

      reconsider IM1 = ( AutMt (( id V),b2,b1)) as Matrix of n, INT.Ring by ZMATRLIN: 50, A1;

      reconsider IM2 = ( AutMt (( id V),b2,b1)) as Matrix of n, INT.Ring by ZMATRLIN: 50, A1;

      reconsider M1 = (IM1 @ ) as Matrix of n, INT.Ring ;

      reconsider M2 = IM2 as Matrix of n, INT.Ring ;

      

       Y1: ( width IM1) = n by MATRIX_0: 24;

      

       Yb: ( width ( BilinearM (f,b1,b1))) = ( len b1) by MATRIX_0: 24;

      ( width ( AutMt (( id V),b2,b1))) = ( len ( BilinearM (f,b1,b1))) & ( width ( BilinearM (f,b1,b1))) = ( len (( AutMt (( id V),b2,b1)) @ )) by MATRIX_0:def 2, Y1, Yb;

      then

       X1: ( width I) = ( len ( BilinearM (f,b1,b1))) & ( width ( BilinearM (f,b1,b1))) = ( len (I @ )) by ZMATRLIN: 6;

      

      thus ( BilinearM (f,b2,b2)) = (I * ( BilinearM (f,b1,b2))) by ThMBF2, AS

      .= (I * (( BilinearM (f,b1,b1)) * (I @ ))) by ThMBF1, AS

      .= ((I * ( BilinearM (f,b1,b1))) * (I @ )) by MATRIX_3: 33, X1;

    end;

    theorem :: ZMODLAT1:99

    

     ThSign2: for V be finite-rank free Z_Module, b1,b2 be OrdBasis of V, M be Matrix of ( rank V), F_Real st M = ( AutMt (( id V),b1,b2)) holds (( Det M) = 1 & ( Det (M @ )) = 1) or (( Det M) = ( - 1) & ( Det (M @ )) = ( - 1))

    proof

      let V be finite-rank free Z_Module, b1,b2 be OrdBasis of V, M be Matrix of ( rank V), F_Real ;

      assume

       AS1: M = ( AutMt (( id V),b1,b2));

      set n = ( rank V);

      per cases ;

        suppose

         AS1: ( rank V) = 0 ;

        

        then

         A1: ( Det M) = ( 1. F_Real ) by MATRIXR2: 41

        .= 1;

        ( Det (M @ )) = ( 1. F_Real ) by AS1, MATRIXR2: 41

        .= 1;

        hence thesis by A1;

      end;

        suppose

         AS2: ( rank V) > 0 ;

        

         B0: ( len b1) = ( rank V) by ZMATRLIN: 49;

        

         B1: ( len ( AutMt (( id V),b2,b1))) = ( len b2) by ZMATRLIN:def 8

        .= ( rank V) by ZMATRLIN: 49;

        ( len b2) = ( rank V) by ZMATRLIN: 49;

        then ( width ( AutMt (( id V),b2,b1))) = ( len b1) by AS2, ZMATRLIN: 34;

        then

        reconsider M2 = ( AutMt (( id V),b2,b1)) as Matrix of ( rank V), INT.Ring by AS2, B0, B1, MATRIX_0: 20;

        ( AutMt (( id V),b1,b2)) is Matrix of n, INT.Ring & ( AutMt (( id V),b2,b1)) is Matrix of n, INT.Ring by ZMATRLIN: 50;

        

        then

         A1: (M * ( inttorealM M2)) = (( AutMt (( id V),b1,b2)) * ( AutMt (( id V),b2,b1))) by AS1, AS2, MLT1

        .= ( 1. ( INT.Ring ,( rank V))) by ZMATRLIN: 54, AS2

        .= ( 1. ( F_Real ,( rank V))) by MLT2;

        then

        reconsider MM2 = (M * ( inttorealM M2)) as Matrix of ( rank V), F_Real ;

        

         A2: (( Det M) * ( Det ( inttorealM M2))) = ( Det MM2) by MATRIXR2: 45

        .= ( 1_ F_Real ) by AS2, A1, NAT_1: 14, MATRIX_7: 16

        .= 1;

        reconsider i = ( Det M) as Integer by AS1, ZMATRLIN: 51, INT_1:def 2;

        ( Det ( inttorealM M2)) in INT by ZMATRLIN: 51;

        then

        reconsider j = ( Det ( inttorealM M2)) as Integer;

        (i * j) = 1 by A2;

        then ( Det M) = 1 or ( Det M) = ( - 1) by INT_1: 9;

        hence thesis by AS2, MATRIX_7: 37, NAT_1: 14;

      end;

    end;

    theorem :: ZMODLAT1:100

    for V be finite-rank free Z_Module, b1,b2 be OrdBasis of V, M be Matrix of ( rank V), F_Real st M = ( AutMt (( id V),b1,b2)) holds |.( Det M).| = 1

    proof

      let V be finite-rank free Z_Module, b1,b2 be OrdBasis of V, M be Matrix of ( rank V), F_Real ;

      assume M = ( AutMt (( id V),b1,b2));

      then ( Det M) = 1 or ( Det M) = ( - 1) by ThSign2;

      then |.( Det M).| = 1 or |.( Det M).| = ( - ( - 1)) by ABSVALUE:def 1;

      hence thesis;

    end;

    theorem :: ZMODLAT1:101

    

     ThMBFY: for V be finite-rank free Z_Module, b1,b2 be OrdBasis of V, f be bilinear-FrForm of V, V holds ( Det ( BilinearM (f,b2,b2))) = ( Det ( BilinearM (f,b1,b1)))

    proof

      let V be finite-rank free Z_Module, b1,b2 be OrdBasis of V, f be bilinear-FrForm of V, V;

      set n = ( len b1);

      

       A1: ( len b1) = ( rank V) by ZMATRLIN: 49;

      

       A2: ( len b2) = ( rank V) by ZMATRLIN: 49;

      reconsider B1 = ( BilinearM (f,b1,b1)) as Matrix of n, F_Real ;

      reconsider B2 = ( BilinearM (f,b2,b2)) as Matrix of n, F_Real by A1, A2;

      reconsider I1 = ( AutMt (( id V),b2,b1)) as Matrix of n, INT.Ring by A1, ZMATRLIN: 50;

      set I = ( inttorealM I1);

      per cases ;

        suppose ( rank V) = 0 ;

        hence ( Det ( BilinearM (f,b2,b2))) = ( Det ( BilinearM (f,b1,b1))) by A1, A2, MATRIX_0: 45;

      end;

        suppose

         ZZ: ( rank V) > 0 ;

        then

         B2: ( BilinearM (f,b2,b2)) = ((I * ( BilinearM (f,b1,b1))) * (I @ )) by ThMBF3;

        set M1 = (I @ );

        set M2 = I;

        ( width M2) = n & ( len M2) = n & ( width B1) = n & ( len B1) = n by MATRIX_0: 24;

        then ( width M2) = ( len B1) & ( len M2) > 0 & ( len B1) > 0 by ZZ, ZMATRLIN: 49;

        then

        reconsider M2B1 = (M2 * B1) as Matrix of n, F_Real by MATRIX_4: 64;

        

         X2: (( Det M2) = 1 & ( Det M1) = 1) or (( Det M2) = ( - 1) & ( Det M1) = ( - 1)) by A1, ThSign2;

        

        thus ( Det ( BilinearM (f,b2,b2))) = ( Det B2) by A1, ZMATRLIN: 49

        .= (( Det M2B1) * ( Det M1)) by A1, B2, ZZ, MATRIX11: 62

        .= ((( Det M2) * ( Det B1)) * ( Det M1)) by ZZ, A1, MATRIX11: 62

        .= ( Det ( BilinearM (f,b1,b1))) by X2;

      end;

    end;

    theorem :: ZMODLAT1:102

    for V be finite-rank free Z_Module, b1,b2 be OrdBasis of V, f be bilinear-FrForm of V, V holds |.( Det ( BilinearM (f,b2,b2))).| = |.( Det ( BilinearM (f,b1,b1))).| by ThMBFY;

    definition

      let V be finite-rank free Z_Module;

      let f be bilinear-FrForm of V, V;

      let b be OrdBasis of V;

      :: ZMODLAT1:def34

      func GramMatrix (f,b) -> Matrix of ( rank V), F_Real equals ( BilinearM (f,b,b));

      correctness

      proof

        ( len b) = ( rank V) by ZMATRLIN: 49;

        hence thesis;

      end;

    end

    definition

      let V be finite-rank free Z_Module;

      let f be bilinear-FrForm of V, V;

      :: ZMODLAT1:def35

      func GramDet (f) -> Element of F_Real means

      : defGramDet: for b be OrdBasis of V holds it = ( Det ( GramMatrix (f,b)));

      existence

      proof

        set b1 = the OrdBasis of V;

        for b be OrdBasis of V holds ( Det ( GramMatrix (f,b))) = ( Det ( GramMatrix (f,b1)))

        proof

          let b be OrdBasis of V;

          

          thus ( Det ( GramMatrix (f,b))) = ( Det ( BilinearM (f,b,b))) by ZMATRLIN: 49

          .= ( Det ( BilinearM (f,b1,b1))) by ThMBFY

          .= ( Det ( GramMatrix (f,b1))) by ZMATRLIN: 49;

        end;

        hence thesis;

      end;

      uniqueness

      proof

        let n,m be Element of F_Real ;

        assume that

         A1: for b be OrdBasis of V holds ( Det ( GramMatrix (f,b))) = n and

         A2: for b be OrdBasis of V holds ( Det ( GramMatrix (f,b))) = m;

        set b1 = the OrdBasis of V;

        ( Det ( GramMatrix (f,b1))) = n by A1;

        hence thesis by A2;

      end;

    end

    definition

      let L be Z_Lattice;

      :: ZMODLAT1:def36

      func InnerProduct (L) -> FrForm of L, L equals the scalar of L;

      correctness ;

    end

    registration

      let L be Z_Lattice;

      cluster ( InnerProduct L) -> additiveSAF homogeneousSAF additiveFAF homogeneousFAF;

      correctness

      proof

        set f = ( InnerProduct L);

        for v be Vector of L holds (( curry' f) . v) is additive

        proof

          let v be Vector of L;

          set g = (( curry' f) . v);

          for w1,w2 be Vector of L holds (g . (w1 + w2)) = ((g . w1) + (g . w2))

          proof

            let w1,w2 be Vector of L;

            

            thus (g . (w1 + w2)) = (f . ((w1 + w2),v)) by FUNCT_5: 70

            .= <;(w1 + w2), v;>

            .= <;v, (w1 + w2);> by defZLattice

            .= ( <;v, w1;> + <;v, w2;>) by ThSc2

            .= ( <;w1, v;> + <;v, w2;>) by defZLattice

            .= ( <;w1, v;> + <;w2, v;>) by defZLattice

            .= ((f . (w1,v)) + (f . (w2,v)))

            .= ((g . w1) + (f . (w2,v))) by FUNCT_5: 70

            .= ((g . w1) + (g . w2)) by FUNCT_5: 70;

          end;

          hence thesis;

        end;

        hence f is additiveSAF;

        for v be Vector of L holds (( curry' f) . v) is homogeneous

        proof

          let v be Vector of L;

          set g = (( curry' f) . v);

          for w be Vector of L, i be Element of INT.Ring holds (g . (i * w)) = (i * (g . w))

          proof

            let w be Vector of L, i be Element of INT.Ring ;

            

            thus (g . (i * w)) = (f . ((i * w),v)) by FUNCT_5: 70

            .= <;(i * w), v;>

            .= <;v, (i * w);> by defZLattice

            .= (i * <;v, w;>) by ThSc3

            .= (i * <;w, v;>) by defZLattice

            .= (i * (f . (w,v)))

            .= (i * (g . w)) by FUNCT_5: 70;

          end;

          hence thesis;

        end;

        hence f is homogeneousSAF;

        for v be Vector of L holds (( curry f) . v) is additive

        proof

          let v be Vector of L;

          set g = (( curry f) . v);

          for w1,w2 be Vector of L holds (g . (w1 + w2)) = ((g . w1) + (g . w2))

          proof

            let w1,w2 be Vector of L;

            

            thus (g . (w1 + w2)) = (f . (v,(w1 + w2))) by FUNCT_5: 69

            .= <;v, (w1 + w2);>

            .= ( <;v, w1;> + <;v, w2;>) by ThSc2

            .= ((f . (v,w1)) + (f . (v,w2)))

            .= ((g . w1) + (f . (v,w2))) by FUNCT_5: 69

            .= ((g . w1) + (g . w2)) by FUNCT_5: 69;

          end;

          hence thesis;

        end;

        hence f is additiveFAF;

        for v be Vector of L holds (( curry f) . v) is homogeneous

        proof

          let v be Vector of L;

          set g = (( curry f) . v);

          for w be Vector of L, i be Element of INT.Ring holds (g . (i * w)) = (i * (g . w))

          proof

            let w be Vector of L, i be Element of INT.Ring ;

            

            thus (g . (i * w)) = (f . (v,(i * w))) by FUNCT_5: 69

            .= <;v, (i * w);>

            .= (i * <;v, w;>) by ThSc3

            .= (i * (f . (v,w)))

            .= (i * (g . w)) by FUNCT_5: 69;

          end;

          hence thesis;

        end;

        hence f is homogeneousFAF;

      end;

    end

    definition

      let L be Z_Lattice;

      let b be OrdBasis of L;

      :: ZMODLAT1:def37

      func GramMatrix (b) -> Matrix of ( dim L), F_Real equals ( GramMatrix (( InnerProduct L),b));

      correctness ;

    end

    definition

      let L be Z_Lattice;

      :: ZMODLAT1:def38

      func GramDet (L) -> Element of F_Real equals ( GramDet ( InnerProduct L));

      correctness ;

    end

    theorem :: ZMODLAT1:103

    for L be INTegral Z_Lattice holds ( InnerProduct L) is bilinear-Form of L, L

    proof

      let L be INTegral Z_Lattice;

      

       X1: ( dom ( InnerProduct L)) = [:the carrier of L, the carrier of L:] by FUNCT_2:def 1;

      for z be object st z in [:the carrier of L, the carrier of L:] holds (( InnerProduct L) . z) in the carrier of INT.Ring

      proof

        let z be object;

        assume z in [:the carrier of L, the carrier of L:];

        then

        consider x1,x2 be object such that

         B1: x1 in the carrier of L & x2 in the carrier of L & z = [x1, x2] by ZFMISC_1:def 2;

        reconsider x1, x2 as Vector of L by B1;

        (( InnerProduct L) . z) = <;x1, x2;> by B1;

        hence (( InnerProduct L) . z) in the carrier of INT.Ring by defIntegral;

      end;

      then

      reconsider f = ( InnerProduct L) as Form of L, L by X1, FUNCT_2: 3;

      for v be Vector of L holds ( FunctionalSAF (f,v)) is additive

      proof

        let v be Vector of L;

        for x,y be Vector of L holds (( FunctionalSAF (f,v)) . (x + y)) = ((( FunctionalSAF (f,v)) . x) + (( FunctionalSAF (f,v)) . y))

        proof

          let x,y be Vector of L;

          

          thus (( FunctionalSAF (f,v)) . (x + y)) = (f . ((x + y),v)) by FUNCT_5: 70

          .= <;(x + y), v;>

          .= <;v, (x + y);> by defZLattice

          .= ( <;v, x;> + <;v, y;>) by ThSc2

          .= ( <;x, v;> + <;v, y;>) by defZLattice

          .= ( <;x, v;> + <;y, v;>) by defZLattice

          .= ((f . (x,v)) + (f . (y,v)))

          .= (((( curry' f) . v) . x) + (f . (y,v))) by FUNCT_5: 70

          .= ((( FunctionalSAF (f,v)) . x) + (( FunctionalSAF (f,v)) . y)) by FUNCT_5: 70;

        end;

        hence ( FunctionalSAF (f,v)) is additive;

      end;

      then

       X1: f is additiveSAF;

      for v be Vector of L holds ( FunctionalSAF (f,v)) is homogeneous

      proof

        let v be Vector of L;

        for x be Vector of L, i be Element of INT.Ring holds (( FunctionalSAF (f,v)) . (i * x)) = (i * (( FunctionalSAF (f,v)) . x))

        proof

          let x be Vector of L, i be Element of INT.Ring ;

          

          thus (( FunctionalSAF (f,v)) . (i * x)) = (f . ((i * x),v)) by FUNCT_5: 70

          .= <;(i * x), v;>

          .= <;v, (i * x);> by defZLattice

          .= (i * <;v, x;>) by ThSc3

          .= (i * <;x, v;>) by defZLattice

          .= (i * (f . (x,v)))

          .= (i * (( FunctionalSAF (f,v)) . x)) by FUNCT_5: 70;

        end;

        hence ( FunctionalSAF (f,v)) is homogeneous;

      end;

      then

       X2: f is homogeneousSAF;

      for v be Vector of L holds ( FunctionalFAF (f,v)) is additive

      proof

        let v be Vector of L;

        for x,y be Vector of L holds (( FunctionalFAF (f,v)) . (x + y)) = ((( FunctionalFAF (f,v)) . x) + (( FunctionalFAF (f,v)) . y))

        proof

          let x,y be Vector of L;

          

          thus (( FunctionalFAF (f,v)) . (x + y)) = (f . (v,(x + y))) by FUNCT_5: 69

          .= <;v, (x + y);>

          .= ( <;v, x;> + <;v, y;>) by ThSc2

          .= ((f . (v,x)) + (f . (v,y)))

          .= (((( curry f) . v) . x) + (f . (v,y))) by FUNCT_5: 69

          .= ((( FunctionalFAF (f,v)) . x) + (( FunctionalFAF (f,v)) . y)) by FUNCT_5: 69;

        end;

        hence ( FunctionalFAF (f,v)) is additive;

      end;

      then

       X3: f is additiveFAF;

      for v be Vector of L holds ( FunctionalFAF (f,v)) is homogeneous

      proof

        let v be Vector of L;

        for x be Vector of L, i be Element of INT.Ring holds (( FunctionalFAF (f,v)) . (i * x)) = (i * (( FunctionalFAF (f,v)) . x))

        proof

          let x be Vector of L, i be Element of INT.Ring ;

          

          thus (( FunctionalFAF (f,v)) . (i * x)) = (f . (v,(i * x))) by FUNCT_5: 69

          .= <;v, (i * x);>

          .= (i * <;v, x;>) by ThSc3

          .= (i * (f . (v,x)))

          .= (i * (( FunctionalFAF (f,v)) . x)) by FUNCT_5: 69;

        end;

        hence ( FunctionalFAF (f,v)) is homogeneous;

      end;

      then f is homogeneousFAF;

      hence thesis by X1, X2, X3;

    end;

    theorem :: ZMODLAT1:104

    

     ThIntLatY: for L be INTegral Z_Lattice, b be OrdBasis of L holds ( GramMatrix b) is Matrix of ( dim L), INT.Ring

    proof

      let L be INTegral Z_Lattice, b be OrdBasis of L;

      

       X1: ( len ( GramMatrix b)) = ( dim L) & ( width ( GramMatrix b)) = ( dim L) & ( Indices ( GramMatrix b)) = [:( Seg ( dim L)), ( Seg ( dim L)):] by MATRIX_0: 24;

      

       X3: ( len b) = ( dim L) by ZMATRLIN: 49;

      for i,j be Nat st [i, j] in ( Indices ( GramMatrix b)) holds (( GramMatrix b) * (i,j)) in the carrier of INT.Ring

      proof

        let i,j be Nat;

        assume [i, j] in ( Indices ( GramMatrix b));

        then i in ( Seg ( dim L)) & j in ( Seg ( dim L)) by X1, ZFMISC_1: 87;

        then

         D1: i in ( dom b) & j in ( dom b) by X3, FINSEQ_1:def 3;

        (( GramMatrix b) * (i,j)) = (( InnerProduct L) . ((b /. i),(b /. j))) by defBilinearM, D1

        .= <;(b /. i), (b /. j);>;

        hence (( GramMatrix b) * (i,j)) in the carrier of INT.Ring by defIntegral;

      end;

      hence ( GramMatrix b) is Matrix of ( dim L), INT.Ring by LMEQ;

    end;

    

     ThIntLatZ: for L be INTegral Z_Lattice holds ( GramDet L) is Integer

    proof

      let L be INTegral Z_Lattice;

      set b = the OrdBasis of L;

      ( GramMatrix b) is Matrix of ( dim L), INT.Ring by ThIntLatY;

      then ( Det ( GramMatrix b)) in INT by ZMATRLIN: 47;

      hence thesis by defGramDet;

    end;

    registration

      let L be INTegral Z_Lattice;

      cluster ( GramDet L) -> integer;

      correctness by ThIntLatZ;

    end