bilinear.miz



    begin

    definition

      let K be 1-sorted;

      let V,W be ModuleStr over K;

      mode Form of V,W is Function of [:the carrier of V, the carrier of W:], the carrier of K;

    end

    definition

      let K be non empty ZeroStr;

      let V,W be ModuleStr over K;

      :: BILINEAR:def1

      func NulForm (V,W) -> Form of V, W equals ( [:the carrier of V, the carrier of W:] --> ( 0. K));

      coherence ;

    end

    definition

      let K be non empty addLoopStr;

      let V,W be non empty ModuleStr over K;

      let f,g be Form of V, W;

      :: BILINEAR:def2

      func f + g -> Form 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 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)) + (g . ($1,$2)));

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

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

        reconsider ff as Form of V, W;

        take ff;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let F,G be Form 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 K be non empty multMagma;

      let V,W be non empty ModuleStr over K;

      let f be Form of V, W;

      let a be Element of K;

      :: BILINEAR:def3

      func a * f -> Form 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 X = the carrier of V, Y = the carrier of W, Z = the carrier of K;

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

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

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

        reconsider ff as Form of V, W;

        take ff;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let F,G be Form 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 K be non empty addLoopStr;

      let V,W be non empty ModuleStr over K;

      let f be Form of V, W;

      :: BILINEAR:def4

      func - f -> Form 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 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 holds for y be Element of Y holds (ff . (x,y)) = F(x,y) from BINOP_1:sch 4;

        reconsider ff as Form of V, W;

        take ff;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let F,G be Form 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 K be add-associative right_zeroed right_complementable left-distributive left_unital non empty doubleLoopStr;

      let V,W be non empty ModuleStr over K;

      let f be Form of V, W;

      :: original: -

      redefine

      :: BILINEAR:def5

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

      compatibility

      proof

        let g be Form of V, W;

        thus g = ( - f) implies g = (( - ( 1. K)) * 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. K)) * (f . (v,w))) by VECTSP_2: 29

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

          end;

          hence thesis;

        end;

        assume

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

        now

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

          

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

          .= ( - (f . (v,w))) by VECTSP_2: 29

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

        end;

        hence thesis;

      end;

    end

    definition

      let K be non empty addLoopStr;

      let V,W be non empty ModuleStr over K;

      let f,g be Form of V, W;

      :: BILINEAR:def6

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

      correctness ;

    end

    definition

      let K be non empty addLoopStr;

      let V,W be non empty ModuleStr over K;

      let f,g be Form of V, W;

      :: original: -

      redefine

      :: BILINEAR:def7

      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 Form 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

          .= ((f . (v,w)) - (g . (v,w))) by RLVECT_1:def 11;

        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 RLVECT_1:def 11

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

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

        end;

        hence thesis;

      end;

    end

    definition

      let K be Abelian non empty addLoopStr;

      let V,W be non empty ModuleStr over K;

      let f,g be Form of V, W;

      :: original: +

      redefine

      func f + g;

      commutativity

      proof

        let f,g be Form 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 :: BILINEAR:1

    for K be right_zeroed non empty addLoopStr holds for V,W be non empty ModuleStr over K holds for f be Form of V, W holds (f + ( NulForm (V,W))) = f

    proof

      let K be right_zeroed non empty addLoopStr, V,W be non empty ModuleStr over K, f be Form of V, W;

      set g = ( NulForm (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. K)) by FUNCOP_1: 70

        .= (f . (v,w)) by RLVECT_1:def 4;

      end;

      hence thesis;

    end;

    theorem :: BILINEAR:2

    for K be add-associative non empty addLoopStr holds for V,W be non empty ModuleStr over K holds for f,g,h be Form of V, W holds ((f + g) + h) = (f + (g + h))

    proof

      let K be add-associative non empty addLoopStr, V,W be non empty ModuleStr over K, f,g,h be Form 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)))) by RLVECT_1:def 3

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

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

      end;

      hence thesis;

    end;

    theorem :: BILINEAR:3

    for K be add-associative right_zeroed right_complementable non empty addLoopStr holds for V,W be non empty ModuleStr over K holds for f be Form of V, W holds (f - f) = ( NulForm (V,W))

    proof

      let K be add-associative right_zeroed right_complementable non empty addLoopStr, V,W be non empty ModuleStr over K, f be Form 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

        .= ( 0. K) by RLVECT_1: 15

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

      end;

      hence thesis;

    end;

    theorem :: BILINEAR:4

    for K be right-distributive non empty doubleLoopStr holds for V,W be non empty ModuleStr over K, a be Element of K holds for f,g be Form of V, W holds (a * (f + g)) = ((a * f) + (a * g))

    proof

      let K be right-distributive non empty doubleLoopStr, V,W be non empty ModuleStr over K, r be Element of K, f,g be Form 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)))) by VECTSP_1:def 2

        .= (((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 :: BILINEAR:5

    for K be left-distributive non empty doubleLoopStr holds for V,W be non empty ModuleStr over K holds for a,b be Element of K holds for f be Form of V, W holds ((a + b) * f) = ((a * f) + (b * f))

    proof

      let K be left-distributive non empty doubleLoopStr, V,W be non empty ModuleStr over K, r,s be Element of K, f be Form 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)))) by VECTSP_1:def 3

        .= (((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 :: BILINEAR:6

    for K be associative non empty doubleLoopStr holds for V,W be non empty ModuleStr over K holds for a,b be Element of K holds for f be Form of V, W holds ((a * b) * f) = (a * (b * f))

    proof

      let K be associative non empty doubleLoopStr, V,W be non empty ModuleStr over K, r,s be Element of K, f be Form 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)))) by GROUP_1:def 3

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

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

      end;

      hence thesis;

    end;

    theorem :: BILINEAR:7

    for K be left_unital non empty doubleLoopStr holds for V,W be non empty ModuleStr over K holds for f be Form of V, W holds (( 1. K) * f) = f

    proof

      let K be left_unital non empty doubleLoopStr, V,W be non empty ModuleStr over K, f be Form of V, W;

      now

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

        

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

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

      end;

      hence thesis;

    end;

    begin

    definition

      let K be non empty 1-sorted;

      let V,W be non empty ModuleStr over K;

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

      :: BILINEAR:def8

      func FunctionalFAF (f,v) -> Functional of W equals (( curry f) . v);

      correctness ;

    end

    definition

      let K be non empty 1-sorted;

      let V,W be non empty ModuleStr over K;

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

      :: BILINEAR:def9

      func FunctionalSAF (f,w) -> Functional of V equals (( curry' f) . w);

      correctness ;

    end

    theorem :: BILINEAR:8

    

     Th8: for K be non empty 1-sorted holds for V,W be non empty ModuleStr over K holds for f be Form of V, W, v be Vector of V holds ( dom ( FunctionalFAF (f,v))) = the carrier of W & ( rng ( FunctionalFAF (f,v))) c= the carrier of K & for w be Vector of W holds (( FunctionalFAF (f,v)) . w) = (f . (v,w))

    proof

      let K be non empty 1-sorted, V,W be non empty ModuleStr over K;

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

      set F = ( FunctionalFAF (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 K;

      let y be Vector of W;

      thus thesis by A1;

    end;

    theorem :: BILINEAR:9

    

     Th9: for K be non empty 1-sorted holds for V,W be non empty ModuleStr over K holds for f be Form of V, W, w be Vector of W holds ( dom ( FunctionalSAF (f,w))) = the carrier of V & ( rng ( FunctionalSAF (f,w))) c= the carrier of K & for v be Vector of V holds (( FunctionalSAF (f,w)) . v) = (f . (v,w))

    proof

      let K be non empty 1-sorted, V,W be non empty ModuleStr over K, f be Form of V, W, w be Vector of W;

      set F = ( FunctionalSAF (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 K;

      let v be Vector of V;

      thus thesis by A1;

    end;

    theorem :: BILINEAR:10

    

     Th10: for K be non empty ZeroStr, V,W be non empty ModuleStr over K, v be Vector of V holds ( FunctionalFAF (( NulForm (V,W)),v)) = ( 0Functional W)

    proof

      let K be non empty ZeroStr, V,W be non empty ModuleStr over K, v be Vector of V;

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

      now

        let y be Vector of W;

        

        thus (( FunctionalFAF (N,v)) . y) = (N . (v,y)) by Th8

        .= ( 0. K) by FUNCOP_1: 70

        .= (( 0Functional W) . y) by HAHNBAN1: 14;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: BILINEAR:11

    

     Th11: for K be non empty ZeroStr, V,W be non empty ModuleStr over K, w be Vector of W holds ( FunctionalSAF (( NulForm (V,W)),w)) = ( 0Functional V)

    proof

      let K be non empty ZeroStr, V,W be non empty ModuleStr over K, y be Vector of W;

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

      now

        let v be Vector of V;

        

        thus (( FunctionalSAF (N,y)) . v) = (N . (v,y)) by Th9

        .= ( 0. K) by FUNCOP_1: 70

        .= (( 0Functional V) . v) by HAHNBAN1: 14;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: BILINEAR:12

    

     Th12: for K be non empty addLoopStr holds for V,W be non empty ModuleStr over K holds for f,g be Form of V, W, w be Vector of W holds ( FunctionalSAF ((f + g),w)) = (( FunctionalSAF (f,w)) + ( FunctionalSAF (g,w)))

    proof

      let K be non empty addLoopStr, V,W be non empty ModuleStr over K, f,g be Form of V, W, w be Vector of W;

      now

        let v be Vector of V;

        

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

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

        .= ((( FunctionalSAF (f,w)) . v) + (g . (v,w))) by Th9

        .= ((( FunctionalSAF (f,w)) . v) + (( FunctionalSAF (g,w)) . v)) by Th9

        .= ((( FunctionalSAF (f,w)) + ( FunctionalSAF (g,w))) . v) by HAHNBAN1:def 3;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: BILINEAR:13

    

     Th13: for K be non empty addLoopStr holds for V,W be non empty ModuleStr over K holds for f,g be Form of V, W, v be Vector of V holds ( FunctionalFAF ((f + g),v)) = (( FunctionalFAF (f,v)) + ( FunctionalFAF (g,v)))

    proof

      let K be non empty addLoopStr, V,W be non empty ModuleStr over K, f,g be Form of V, W, w be Vector of V;

      now

        let v be Vector of W;

        

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

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

        .= ((( FunctionalFAF (f,w)) . v) + (g . (w,v))) by Th8

        .= ((( FunctionalFAF (f,w)) . v) + (( FunctionalFAF (g,w)) . v)) by Th8

        .= ((( FunctionalFAF (f,w)) + ( FunctionalFAF (g,w))) . v) by HAHNBAN1:def 3;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: BILINEAR:14

    

     Th14: for K be non empty doubleLoopStr holds for V,W be non empty ModuleStr over K holds for f be Form of V, W, a be Element of K, w be Vector of W holds ( FunctionalSAF ((a * f),w)) = (a * ( FunctionalSAF (f,w)))

    proof

      let K be non empty doubleLoopStr, V,W be non empty ModuleStr over K, f be Form of V, W, a be Element of K, w be Vector of W;

      now

        let v be Vector of V;

        

        thus (( FunctionalSAF ((a * f),w)) . v) = ((a * f) . (v,w)) by Th9

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

        .= (a * (( FunctionalSAF (f,w)) . v)) by Th9

        .= ((a * ( FunctionalSAF (f,w))) . v) by HAHNBAN1:def 6;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: BILINEAR:15

    

     Th15: for K be non empty doubleLoopStr holds for V,W be non empty ModuleStr over K holds for f be Form of V, W, a be Element of K, v be Vector of V holds ( FunctionalFAF ((a * f),v)) = (a * ( FunctionalFAF (f,v)))

    proof

      let K be non empty doubleLoopStr, V,W be non empty ModuleStr over K, f be Form of V, W, a be Element of K, w be Vector of V;

      now

        let v be Vector of W;

        

        thus (( FunctionalFAF ((a * f),w)) . v) = ((a * f) . (w,v)) by Th8

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

        .= (a * (( FunctionalFAF (f,w)) . v)) by Th8

        .= ((a * ( FunctionalFAF (f,w))) . v) by HAHNBAN1:def 6;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: BILINEAR:16

    

     Th16: for K be non empty addLoopStr holds for V,W be non empty ModuleStr over K holds for f be Form of V, W, w be Vector of W holds ( FunctionalSAF (( - f),w)) = ( - ( FunctionalSAF (f,w)))

    proof

      let K be non empty addLoopStr, V,W be non empty ModuleStr over K, f be Form of V, W, w be Vector of W;

      now

        let v be Vector of V;

        

        thus (( FunctionalSAF (( - f),w)) . v) = (( - f) . (v,w)) by Th9

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

        .= ( - (( FunctionalSAF (f,w)) . v)) by Th9

        .= (( - ( FunctionalSAF (f,w))) . v) by HAHNBAN1:def 4;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: BILINEAR:17

    

     Th17: for K be non empty addLoopStr holds for V,W be non empty ModuleStr over K holds for f be Form of V, W, v be Vector of V holds ( FunctionalFAF (( - f),v)) = ( - ( FunctionalFAF (f,v)))

    proof

      let K be non empty addLoopStr, V,W be non empty ModuleStr over K, f be Form of V, W, w be Vector of V;

      now

        let v be Vector of W;

        

        thus (( FunctionalFAF (( - f),w)) . v) = (( - f) . (w,v)) by Th8

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

        .= ( - (( FunctionalFAF (f,w)) . v)) by Th8

        .= (( - ( FunctionalFAF (f,w))) . v) by HAHNBAN1:def 4;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: BILINEAR:18

    for K be non empty addLoopStr holds for V,W be non empty ModuleStr over K holds for f,g be Form of V, W, w be Vector of W holds ( FunctionalSAF ((f - g),w)) = (( FunctionalSAF (f,w)) - ( FunctionalSAF (g,w)))

    proof

      let K be non empty addLoopStr, V,W be non empty ModuleStr over K, f,g be Form of V, W, w be Vector of W;

      now

        let v be Vector of V;

        

        thus (( FunctionalSAF ((f - g),w)) . v) = ((f - g) . (v,w)) by Th9

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

        .= ((( FunctionalSAF (f,w)) . v) - (g . (v,w))) by Th9

        .= ((( FunctionalSAF (f,w)) . v) - (( FunctionalSAF (g,w)) . v)) by Th9

        .= ((( FunctionalSAF (f,w)) . v) + ( - (( FunctionalSAF (g,w)) . v))) by RLVECT_1:def 11

        .= ((( FunctionalSAF (f,w)) . v) + (( - ( FunctionalSAF (g,w))) . v)) by HAHNBAN1:def 4

        .= ((( FunctionalSAF (f,w)) - ( FunctionalSAF (g,w))) . v) by HAHNBAN1:def 3;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: BILINEAR:19

    for K be non empty addLoopStr holds for V,W be non empty ModuleStr over K holds for f,g be Form of V, W, v be Vector of V holds ( FunctionalFAF ((f - g),v)) = (( FunctionalFAF (f,v)) - ( FunctionalFAF (g,v)))

    proof

      let K be non empty addLoopStr, V,W be non empty ModuleStr over K, f,g be Form of V, W, w be Vector of V;

      now

        let v be Vector of W;

        

        thus (( FunctionalFAF ((f - g),w)) . v) = ((f - g) . (w,v)) by Th8

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

        .= ((( FunctionalFAF (f,w)) . v) - (g . (w,v))) by Th8

        .= ((( FunctionalFAF (f,w)) . v) - (( FunctionalFAF (g,w)) . v)) by Th8

        .= ((( FunctionalFAF (f,w)) . v) + ( - (( FunctionalFAF (g,w)) . v))) by RLVECT_1:def 11

        .= ((( FunctionalFAF (f,w)) . v) + (( - ( FunctionalFAF (g,w))) . v)) by HAHNBAN1:def 4

        .= ((( FunctionalFAF (f,w)) - ( FunctionalFAF (g,w))) . v) by HAHNBAN1:def 3;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    begin

    definition

      let K be non empty multMagma;

      let V,W be non empty ModuleStr over K;

      let f be Functional of V;

      let g be Functional of W;

      :: BILINEAR:def10

      func FormFunctional (f,g) -> Form of V, W means

      : Def10: 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 K;

        consider i be Function of [:c1, c2:], k such that

         A1: for x be Element of c1 holds for y be Element of c2 holds (i . (x,y)) = F(x,y) from BINOP_1:sch 4;

        reconsider i as Form of V, W;

        take i;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let F1,F2 be Form 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 :: BILINEAR:20

    

     Th20: for K be add-associative right_zeroed right_complementable right-distributive non empty doubleLoopStr holds for V,W be non empty ModuleStr over K holds for f be Functional of V, v be Vector of V, w be Vector of W holds (( FormFunctional (f,( 0Functional W))) . (v,w)) = ( 0. K)

    proof

      let K be add-associative right_zeroed right_complementable right-distributive non empty doubleLoopStr;

      let V,W be non empty ModuleStr over K;

      let f be Functional of V, v be Vector of V, y be Vector of W;

      set 0F = ( 0Functional W), F = ( FormFunctional (f,0F));

      

      thus (F . (v,y)) = ((f . v) * (0F . y)) by Def10

      .= ((f . v) * ( 0. K)) by FUNCOP_1: 7

      .= ( 0. K);

    end;

    theorem :: BILINEAR:21

    

     Th21: for K be add-associative right_zeroed right_complementable left-distributive non empty doubleLoopStr holds for V,W be non empty ModuleStr over K holds for g be Functional of W, v be Vector of V, w be Vector of W holds (( FormFunctional (( 0Functional V),g)) . (v,w)) = ( 0. K)

    proof

      let K be add-associative right_zeroed right_complementable left-distributive non empty doubleLoopStr;

      let V,W be non empty ModuleStr over K;

      let h be Functional of W, v be Vector of V, y be Vector of W;

      set 0F = ( 0Functional V), F = ( FormFunctional (0F,h));

      

      thus (F . (v,y)) = ((0F . v) * (h . y)) by Def10

      .= (( 0. K) * (h . y)) by FUNCOP_1: 7

      .= ( 0. K);

    end;

    theorem :: BILINEAR:22

    for K be add-associative right_zeroed right_complementable right-distributive non empty doubleLoopStr holds for V,W be non empty ModuleStr over K holds for f be Functional of V holds ( FormFunctional (f,( 0Functional W))) = ( NulForm (V,W))

    proof

      let K be add-associative right_zeroed right_complementable right-distributive non empty doubleLoopStr;

      let V,W be non empty ModuleStr over K, f be Functional of V;

      now

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

        

        thus (( FormFunctional (f,( 0Functional W))) . (v,y)) = ( 0. K) by Th20

        .= (( NulForm (V,W)) . (v,y)) by FUNCOP_1: 70;

      end;

      hence thesis;

    end;

    theorem :: BILINEAR:23

    for K be add-associative right_zeroed right_complementable left-distributive non empty doubleLoopStr holds for V,W be non empty ModuleStr over K holds for g be Functional of W holds ( FormFunctional (( 0Functional V),g)) = ( NulForm (V,W))

    proof

      let K be add-associative right_zeroed right_complementable left-distributive non empty doubleLoopStr;

      let V,W be non empty ModuleStr over K, h be Functional of W;

      now

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

        

        thus (( FormFunctional (( 0Functional V),h)) . (v,y)) = ( 0. K) by Th21

        .= (( NulForm (V,W)) . (v,y)) by FUNCOP_1: 70;

      end;

      hence thesis;

    end;

    theorem :: BILINEAR:24

    

     Th24: for K be non empty multMagma holds for V,W be non empty ModuleStr over K holds for f be Functional of V, g be Functional of W, v be Vector of V holds ( FunctionalFAF (( FormFunctional (f,g)),v)) = ((f . v) * g)

    proof

      let K be non empty multMagma, V,W be non empty ModuleStr over K;

      let f be Functional of V, h be Functional of W, v be Vector of V;

      set F = ( FormFunctional (f,h)), FF = ( FunctionalFAF (F,v));

      now

        let y be Vector of W;

        

        thus (FF . y) = (F . (v,y)) by Th8

        .= ((f . v) * (h . y)) by Def10

        .= (((f . v) * h) . y) by HAHNBAN1:def 6;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: BILINEAR:25

    

     Th25: for K be commutative non empty multMagma holds for V,W be non empty ModuleStr over K holds for f be Functional of V, g be Functional of W, w be Vector of W holds ( FunctionalSAF (( FormFunctional (f,g)),w)) = ((g . w) * f)

    proof

      let K be commutative non empty multMagma, V,W be non empty ModuleStr over K;

      let f be Functional of V, h be Functional of W, y be Vector of W;

      set F = ( FormFunctional (f,h)), FF = ( FunctionalSAF (F,y));

      now

        let v be Vector of V;

        

        thus (FF . v) = (F . (v,y)) by Th9

        .= ((f . v) * (h . y)) by Def10

        .= (((h . y) * f) . v) by HAHNBAN1:def 6;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    begin

    definition

      let K be non empty addLoopStr;

      let V,W be non empty ModuleStr over K;

      let f be Form of V, W;

      :: BILINEAR:def11

      attr f is additiveFAF means

      : Def11: for v be Vector of V holds ( FunctionalFAF (f,v)) is additive;

      :: BILINEAR:def12

      attr f is additiveSAF means

      : Def12: for w be Vector of W holds ( FunctionalSAF (f,w)) is additive;

    end

    definition

      let K be non empty multMagma;

      let V,W be non empty ModuleStr over K;

      let f be Form of V, W;

      :: BILINEAR:def13

      attr f is homogeneousFAF means

      : Def13: for v be Vector of V holds ( FunctionalFAF (f,v)) is homogeneous;

      :: BILINEAR:def14

      attr f is homogeneousSAF means

      : Def14: for w be Vector of W holds ( FunctionalSAF (f,w)) is homogeneous;

    end

    registration

      let K be right_zeroed non empty addLoopStr;

      let V,W be non empty ModuleStr over K;

      cluster ( NulForm (V,W)) -> additiveFAF;

      coherence

      proof

        let v be Vector of V;

        ( FunctionalFAF (( NulForm (V,W)),v)) = ( 0Functional W) by Th10;

        hence thesis;

      end;

      cluster ( NulForm (V,W)) -> additiveSAF;

      coherence

      proof

        let y be Vector of W;

        ( FunctionalSAF (( NulForm (V,W)),y)) = ( 0Functional V) by Th11;

        hence thesis;

      end;

    end

    registration

      let K be right_zeroed non empty addLoopStr;

      let V,W be non empty ModuleStr over K;

      cluster additiveFAF additiveSAF for Form of V, W;

      existence

      proof

        take ( NulForm (V,W));

        thus thesis;

      end;

    end

    registration

      let K be add-associative right_zeroed right_complementable right-distributive non empty doubleLoopStr;

      let V,W be non empty ModuleStr over K;

      cluster ( NulForm (V,W)) -> homogeneousFAF;

      coherence

      proof

        let v be Vector of V;

        ( FunctionalFAF (( NulForm (V,W)),v)) = ( 0Functional W) by Th10;

        hence thesis;

      end;

      cluster ( NulForm (V,W)) -> homogeneousSAF;

      coherence

      proof

        let y be Vector of W;

        ( FunctionalSAF (( NulForm (V,W)),y)) = ( 0Functional V) by Th11;

        hence thesis;

      end;

    end

    registration

      let K be add-associative right_zeroed right_complementable right-distributive non empty doubleLoopStr;

      let V,W be non empty ModuleStr over K;

      cluster additiveFAF homogeneousFAF additiveSAF homogeneousSAF for Form of V, W;

      existence

      proof

        take ( NulForm (V,W));

        thus thesis;

      end;

    end

    definition

      let K be add-associative right_zeroed right_complementable right-distributive non empty doubleLoopStr;

      let V,W be non empty ModuleStr over K;

      mode bilinear-Form of V,W is additiveSAF homogeneousSAF additiveFAF homogeneousFAF Form of V, W;

    end

    registration

      let K be add-associative right_zeroed right_complementable right-distributive non empty doubleLoopStr;

      let V,W be non empty ModuleStr over K;

      let f be additiveFAF Form of V, W, v be Vector of V;

      cluster ( FunctionalFAF (f,v)) -> additive;

      coherence by Def11;

    end

    registration

      let K be add-associative right_zeroed right_complementable right-distributive non empty doubleLoopStr;

      let V,W be non empty ModuleStr over K;

      let f be additiveSAF Form of V, W, w be Vector of W;

      cluster ( FunctionalSAF (f,w)) -> additive;

      coherence by Def12;

    end

    registration

      let K be add-associative right_zeroed right_complementable right-distributive non empty doubleLoopStr;

      let V,W be non empty ModuleStr over K;

      let f be homogeneousFAF Form of V, W, v be Vector of V;

      cluster ( FunctionalFAF (f,v)) -> homogeneous;

      coherence by Def13;

    end

    registration

      let K be add-associative right_zeroed right_complementable right-distributive non empty doubleLoopStr;

      let V,W be non empty ModuleStr over K;

      let f be homogeneousSAF Form of V, W, w be Vector of W;

      cluster ( FunctionalSAF (f,w)) -> homogeneous;

      coherence by Def14;

    end

    registration

      let K be add-associative right_zeroed right_complementable right-distributive non empty doubleLoopStr;

      let V,W be non empty ModuleStr over K;

      let f be Functional of V, g be additive Functional of W;

      cluster ( FormFunctional (f,g)) -> additiveFAF;

      coherence

      proof

        let v be Vector of V;

        set fg = ( FormFunctional (f,g)), F = ( FunctionalFAF (fg,v));

        let y,y9 be Vector of W;

        

         A1: F = ((f . v) * g) by Th24;

        

        hence (F . (y + y9)) = ((f . v) * (g . (y + y9))) by HAHNBAN1:def 6

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

        .= (((f . v) * (g . y)) + ((f . v) * (g . y9))) by VECTSP_1:def 2

        .= (((f . v) * (g . y)) + (F . y9)) by A1, HAHNBAN1:def 6

        .= ((F . y) + (F . y9)) by A1, HAHNBAN1:def 6;

      end;

    end

    registration

      let K be add-associative right_zeroed right_complementable commutative right-distributive non empty doubleLoopStr;

      let V,W be non empty ModuleStr over K;

      let f be additive Functional of V, g be Functional of W;

      cluster ( FormFunctional (f,g)) -> additiveSAF;

      coherence

      proof

        let y be Vector of W;

        set fg = ( FormFunctional (f,g)), F = ( FunctionalSAF (fg,y));

        F = ((g . y) * f) by Th25;

        hence thesis;

      end;

    end

    registration

      let K be add-associative right_zeroed right_complementable commutative associative right-distributive non empty doubleLoopStr;

      let V,W be non empty ModuleStr over K;

      let f be Functional of V, g be homogeneous Functional of W;

      cluster ( FormFunctional (f,g)) -> homogeneousFAF;

      coherence

      proof

        let v be Vector of V;

        set fg = ( FormFunctional (f,g)), F = ( FunctionalFAF (fg,v));

        let y be Vector of W, r be Scalar of W;

        

         A1: F = ((f . v) * g) by Th24;

        

        hence (F . (r * y)) = ((f . v) * (g . (r * y))) by HAHNBAN1:def 6

        .= ((f . v) * (r * (g . y))) by HAHNBAN1:def 8

        .= (r * ((f . v) * (g . y))) by GROUP_1:def 3

        .= (r * (F . y)) by A1, HAHNBAN1:def 6;

      end;

    end

    registration

      let K be add-associative right_zeroed right_complementable commutative associative right-distributive non empty doubleLoopStr;

      let V,W be non empty ModuleStr over K;

      let f be homogeneous Functional of V, g be Functional of W;

      cluster ( FormFunctional (f,g)) -> homogeneousSAF;

      coherence

      proof

        let y be Vector of W;

        set fg = ( FormFunctional (f,g));

        set F = ( FunctionalSAF (fg,y));

        let v be Vector of V, r be Scalar of V;

        

         A1: F = ((g . y) * f) by Th25;

        

        hence (F . (r * v)) = ((g . y) * (f . (r * v))) by HAHNBAN1:def 6

        .= ((g . y) * (r * (f . v))) by HAHNBAN1:def 8

        .= (r * ((g . y) * (f . v))) by GROUP_1:def 3

        .= (r * (F . v)) by A1, HAHNBAN1:def 6;

      end;

    end

    registration

      let K be non degenerated non empty doubleLoopStr;

      let V be non trivial ModuleStr over K, W be non empty ModuleStr over K;

      let f be Functional of V, g be Functional of W;

      cluster ( FormFunctional (f,g)) -> non trivial;

      coherence

      proof

        set fg = ( FormFunctional (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 K be non degenerated non empty doubleLoopStr;

      let V be non empty ModuleStr over K, W be non trivial ModuleStr over K;

      let f be Functional of V, g be Functional of W;

      cluster ( FormFunctional (f,g)) -> non trivial;

      coherence

      proof

        set fg = ( FormFunctional (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

    registration

      let K be Field;

      let V,W be non trivial VectSp of K;

      let f be non constant 0-preserving Functional of V, g be non constant 0-preserving Functional of W;

      cluster ( FormFunctional (f,g)) -> non constant;

      coherence

      proof

        set fg = ( FormFunctional (f,g));

        consider v be Vector of V such that v <> ( 0. V) and

         A1: (f . v) <> ( 0. K) by VECTSP10: 28;

        consider w be Vector of W such that w <> ( 0. W) and

         A2: (g . w) <> ( 0. K) by VECTSP10: 28;

        (fg . (v,w)) = ((f . v) * (g . w)) by Def10;

        then

         A3: ( dom fg) = [:the carrier of V, the carrier of W:] & (fg . (v,w)) <> ( 0. K) by A1, A2, FUNCT_2:def 1, VECTSP_1: 12;

        (fg . (( 0. V),( 0. W))) = ((f . ( 0. V)) * (g . ( 0. W))) by Def10

        .= (( 0. K) * (g . ( 0. W))) by HAHNBAN1:def 9

        .= ( 0. K);

        hence thesis by A3, BINOP_1: 19;

      end;

    end

    registration

      let K be Field;

      let V,W be non trivial VectSp of K;

      cluster non trivial non constant additiveFAF homogeneousFAF additiveSAF homogeneousSAF for Form of V, W;

      existence

      proof

        set f = the non constant non trivial linear-Functional of V, g = the non constant non trivial linear-Functional of W;

        take ( FormFunctional (f,g));

        thus thesis;

      end;

    end

    registration

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

      let V,W be non empty ModuleStr over K;

      let f,g be additiveSAF Form of V, W;

      cluster (f + g) -> additiveSAF;

      correctness

      proof

        let w be Vector of W;

        set Ffg = ( FunctionalSAF ((f + g),w)), Ff = ( FunctionalSAF (f,w));

        set Fg = ( FunctionalSAF (g,w));

        let v,y be Vector of V;

        

         A1: Ff is additive by Def12;

        

         A2: Fg is additive by Def12;

        

        thus (Ffg . (v + y)) = ((Ff + Fg) . (v + y)) by Th12

        .= ((Ff . (v + y)) + (Fg . (v + y))) by HAHNBAN1:def 3

        .= (((Ff . v) + (Ff . y)) + (Fg . (v + y))) by A1

        .= (((Ff . v) + (Ff . y)) + ((Fg . v) + (Fg . y))) by A2

        .= ((((Ff . v) + (Ff . y)) + (Fg . v)) + (Fg . y)) by RLVECT_1:def 3

        .= ((((Ff . v) + (Fg . v)) + (Ff . y)) + (Fg . y)) by RLVECT_1:def 3

        .= ((((Ff + Fg) . v) + (Ff . y)) + (Fg . y)) by HAHNBAN1:def 3

        .= (((Ff + Fg) . v) + ((Ff . y) + (Fg . y))) by RLVECT_1:def 3

        .= (((Ff + Fg) . v) + ((Ff + Fg) . y)) by HAHNBAN1:def 3

        .= ((Ffg . v) + ((Ff + Fg) . y)) by Th12

        .= ((Ffg . v) + (Ffg . y)) by Th12;

      end;

    end

    registration

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

      let V,W be non empty ModuleStr over K;

      let f,g be additiveFAF Form of V, W;

      cluster (f + g) -> additiveFAF;

      correctness

      proof

        let w be Vector of V;

        set Ffg = ( FunctionalFAF ((f + g),w)), Ff = ( FunctionalFAF (f,w));

        set Fg = ( FunctionalFAF (g,w));

        let v,y be Vector of W;

        

         A1: Ff is additive by Def11;

        

         A2: Fg is additive by Def11;

        

        thus (Ffg . (v + y)) = ((Ff + Fg) . (v + y)) by Th13

        .= ((Ff . (v + y)) + (Fg . (v + y))) by HAHNBAN1:def 3

        .= (((Ff . v) + (Ff . y)) + (Fg . (v + y))) by A1

        .= (((Ff . v) + (Ff . y)) + ((Fg . v) + (Fg . y))) by A2

        .= ((((Ff . v) + (Ff . y)) + (Fg . v)) + (Fg . y)) by RLVECT_1:def 3

        .= ((((Ff . v) + (Fg . v)) + (Ff . y)) + (Fg . y)) by RLVECT_1:def 3

        .= ((((Ff + Fg) . v) + (Ff . y)) + (Fg . y)) by HAHNBAN1:def 3

        .= (((Ff + Fg) . v) + ((Ff . y) + (Fg . y))) by RLVECT_1:def 3

        .= (((Ff + Fg) . v) + ((Ff + Fg) . y)) by HAHNBAN1:def 3

        .= ((Ffg . v) + ((Ff + Fg) . y)) by Th13

        .= ((Ffg . v) + (Ffg . y)) by Th13;

      end;

    end

    registration

      let K be right-distributive right_zeroed non empty doubleLoopStr;

      let V,W be non empty ModuleStr over K;

      let f be additiveSAF Form of V, W;

      let a be Element of K;

      cluster (a * f) -> additiveSAF;

      correctness

      proof

        let w be Vector of W;

        set Ffg = ( FunctionalSAF ((a * f),w)), Ff = ( FunctionalSAF (f,w));

        let v,y be Vector of V;

        

         A1: Ff is additive by Def12;

        

        thus (Ffg . (v + y)) = ((a * Ff) . (v + y)) by Th14

        .= (a * (Ff . (v + y))) by HAHNBAN1:def 6

        .= (a * ((Ff . v) + (Ff . y))) by A1

        .= ((a * (Ff . v)) + (a * (Ff . y))) by VECTSP_1:def 2

        .= (((a * Ff) . v) + (a * (Ff . y))) by HAHNBAN1:def 6

        .= (((a * Ff) . v) + ((a * Ff) . y)) by HAHNBAN1:def 6

        .= ((Ffg . v) + ((a * Ff) . y)) by Th14

        .= ((Ffg . v) + (Ffg . y)) by Th14;

      end;

    end

    registration

      let K be right-distributive right_zeroed non empty doubleLoopStr;

      let V,W be non empty ModuleStr over K;

      let f be additiveFAF Form of V, W;

      let a be Element of K;

      cluster (a * f) -> additiveFAF;

      correctness

      proof

        let w be Vector of V;

        set Ffg = ( FunctionalFAF ((a * f),w)), Ff = ( FunctionalFAF (f,w));

        let v,y be Vector of W;

        

         A1: Ff is additive by Def11;

        

        thus (Ffg . (v + y)) = ((a * Ff) . (v + y)) by Th15

        .= (a * (Ff . (v + y))) by HAHNBAN1:def 6

        .= (a * ((Ff . v) + (Ff . y))) by A1

        .= ((a * (Ff . v)) + (a * (Ff . y))) by VECTSP_1:def 2

        .= (((a * Ff) . v) + (a * (Ff . y))) by HAHNBAN1:def 6

        .= (((a * Ff) . v) + ((a * Ff) . y)) by HAHNBAN1:def 6

        .= ((Ffg . v) + ((a * Ff) . y)) by Th15

        .= ((Ffg . v) + (Ffg . y)) by Th15;

      end;

    end

    registration

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

      let V,W be non empty ModuleStr over K;

      let f be additiveSAF Form of V, W;

      cluster ( - f) -> additiveSAF;

      correctness

      proof

        let w be Vector of W;

        set Ffg = ( FunctionalSAF (( - f),w)), Ff = ( FunctionalSAF (f,w));

        let v,y be Vector of V;

        

         A1: Ff is additive by Def12;

        

        thus (Ffg . (v + y)) = (( - Ff) . (v + y)) by Th16

        .= ( - (Ff . (v + y))) by HAHNBAN1:def 4

        .= ( - ((Ff . v) + (Ff . y))) by A1

        .= (( - (Ff . v)) - (Ff . y)) by RLVECT_1: 30

        .= ((( - Ff) . v) - (Ff . y)) by HAHNBAN1:def 4

        .= ((( - Ff) . v) + ( - (Ff . y))) by RLVECT_1:def 11

        .= ((( - Ff) . v) + (( - Ff) . y)) by HAHNBAN1:def 4

        .= ((Ffg . v) + (( - Ff) . y)) by Th16

        .= ((Ffg . v) + (Ffg . y)) by Th16;

      end;

    end

    registration

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

      let V,W be non empty ModuleStr over K;

      let f be additiveFAF Form of V, W;

      cluster ( - f) -> additiveFAF;

      correctness

      proof

        let w be Vector of V;

        set Ffg = ( FunctionalFAF (( - f),w)), Ff = ( FunctionalFAF (f,w));

        let v,y be Vector of W;

        

         A1: Ff is additive by Def11;

        

        thus (Ffg . (v + y)) = (( - Ff) . (v + y)) by Th17

        .= ( - (Ff . (v + y))) by HAHNBAN1:def 4

        .= ( - ((Ff . v) + (Ff . y))) by A1

        .= (( - (Ff . v)) - (Ff . y)) by RLVECT_1: 30

        .= ((( - Ff) . v) - (Ff . y)) by HAHNBAN1:def 4

        .= ((( - Ff) . v) + ( - (Ff . y))) by RLVECT_1:def 11

        .= ((( - Ff) . v) + (( - Ff) . y)) by HAHNBAN1:def 4

        .= ((Ffg . v) + (( - Ff) . y)) by Th17

        .= ((Ffg . v) + (Ffg . y)) by Th17;

      end;

    end

    registration

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

      let V,W be non empty ModuleStr over K;

      let f,g be additiveSAF Form of V, W;

      cluster (f - g) -> additiveSAF;

      correctness ;

    end

    registration

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

      let V,W be non empty ModuleStr over K;

      let f,g be additiveFAF Form of V, W;

      cluster (f - g) -> additiveFAF;

      correctness ;

    end

    registration

      let K be add-associative right_zeroed right_complementable right-distributive non empty doubleLoopStr;

      let V,W be non empty ModuleStr over K;

      let f,g be homogeneousSAF Form of V, W;

      cluster (f + g) -> homogeneousSAF;

      correctness

      proof

        let w be Vector of W;

        set Ffg = ( FunctionalSAF ((f + g),w)), Ff = ( FunctionalSAF (f,w));

        set Fg = ( FunctionalSAF (g,w));

        let v be Vector of V, a be Scalar of V;

        

        thus (Ffg . (a * v)) = ((Ff + Fg) . (a * v)) by Th12

        .= ((Ff . (a * v)) + (Fg . (a * v))) by HAHNBAN1:def 3

        .= ((a * (Ff . v)) + (Fg . (a * v))) by HAHNBAN1:def 8

        .= ((a * (Ff . v)) + (a * (Fg . v))) by HAHNBAN1:def 8

        .= (a * ((Ff . v) + (Fg . v))) by VECTSP_1:def 2

        .= (a * ((Ff + Fg) . v)) by HAHNBAN1:def 3

        .= (a * (Ffg . v)) by Th12;

      end;

    end

    registration

      let K be add-associative right_zeroed right_complementable right-distributive non empty doubleLoopStr;

      let V,W be non empty ModuleStr over K;

      let f,g be homogeneousFAF Form of V, W;

      cluster (f + g) -> homogeneousFAF;

      correctness

      proof

        let w be Vector of V;

        set Ffg = ( FunctionalFAF ((f + g),w)), Ff = ( FunctionalFAF (f,w));

        set Fg = ( FunctionalFAF (g,w));

        let v be Vector of W, a be Scalar of V;

        

        thus (Ffg . (a * v)) = ((Ff + Fg) . (a * v)) by Th13

        .= ((Ff . (a * v)) + (Fg . (a * v))) by HAHNBAN1:def 3

        .= ((a * (Ff . v)) + (Fg . (a * v))) by HAHNBAN1:def 8

        .= ((a * (Ff . v)) + (a * (Fg . v))) by HAHNBAN1:def 8

        .= (a * ((Ff . v) + (Fg . v))) by VECTSP_1:def 2

        .= (a * ((Ff + Fg) . v)) by HAHNBAN1:def 3

        .= (a * (Ffg . v)) by Th13;

      end;

    end

    registration

      let K be add-associative right_zeroed right_complementable associative commutative right-distributive non empty doubleLoopStr;

      let V,W be non empty ModuleStr over K;

      let f be homogeneousSAF Form of V, W;

      let a be Element of K;

      cluster (a * f) -> homogeneousSAF;

      correctness

      proof

        let w be Vector of W;

        set Ffg = ( FunctionalSAF ((a * f),w)), Ff = ( FunctionalSAF (f,w));

        let v be Vector of V, b be Scalar of V;

        

        thus (Ffg . (b * v)) = ((a * Ff) . (b * v)) by Th14

        .= (a * (Ff . (b * v))) by HAHNBAN1:def 6

        .= (a * (b * (Ff . v))) by HAHNBAN1:def 8

        .= (b * (a * (Ff . v))) by GROUP_1:def 3

        .= (b * ((a * Ff) . v)) by HAHNBAN1:def 6

        .= (b * (Ffg . v)) by Th14;

      end;

    end

    registration

      let K be add-associative right_zeroed right_complementable associative commutative right-distributive non empty doubleLoopStr;

      let V,W be non empty ModuleStr over K;

      let f be homogeneousFAF Form of V, W;

      let a be Element of K;

      cluster (a * f) -> homogeneousFAF;

      correctness

      proof

        let w be Vector of V;

        set Ffg = ( FunctionalFAF ((a * f),w)), Ff = ( FunctionalFAF (f,w));

        let v be Vector of W, b be Scalar of V;

        

        thus (Ffg . (b * v)) = ((a * Ff) . (b * v)) by Th15

        .= (a * (Ff . (b * v))) by HAHNBAN1:def 6

        .= (a * (b * (Ff . v))) by HAHNBAN1:def 8

        .= (b * (a * (Ff . v))) by GROUP_1:def 3

        .= (b * ((a * Ff) . v)) by HAHNBAN1:def 6

        .= (b * (Ffg . v)) by Th15;

      end;

    end

    registration

      let K be add-associative right_zeroed right_complementable right-distributive non empty doubleLoopStr;

      let V,W be non empty ModuleStr over K;

      let f be homogeneousSAF Form of V, W;

      cluster ( - f) -> homogeneousSAF;

      correctness

      proof

        let w be Vector of W;

        set Ffg = ( FunctionalSAF (( - f),w)), Ff = ( FunctionalSAF (f,w));

        let v be Vector of V, a be Scalar of V;

        

        thus (Ffg . (a * v)) = (( - Ff) . (a * v)) by Th16

        .= ( - (Ff . (a * v))) by HAHNBAN1:def 4

        .= ( - (a * (Ff . v))) by HAHNBAN1:def 8

        .= (a * ( - (Ff . v))) by VECTSP_1: 8

        .= (a * (( - Ff) . v)) by HAHNBAN1:def 4

        .= (a * (Ffg . v)) by Th16;

      end;

    end

    registration

      let K be add-associative right_zeroed right_complementable right-distributive non empty doubleLoopStr;

      let V,W be non empty ModuleStr over K;

      let f be homogeneousFAF Form of V, W;

      cluster ( - f) -> homogeneousFAF;

      correctness

      proof

        let w be Vector of V;

        set Ffg = ( FunctionalFAF (( - f),w)), Ff = ( FunctionalFAF (f,w));

        let v be Vector of W, a be Scalar of W;

        

        thus (Ffg . (a * v)) = (( - Ff) . (a * v)) by Th17

        .= ( - (Ff . (a * v))) by HAHNBAN1:def 4

        .= ( - (a * (Ff . v))) by HAHNBAN1:def 8

        .= (a * ( - (Ff . v))) by VECTSP_1: 8

        .= (a * (( - Ff) . v)) by HAHNBAN1:def 4

        .= (a * (Ffg . v)) by Th17;

      end;

    end

    registration

      let K be add-associative right_zeroed right_complementable right-distributive non empty doubleLoopStr;

      let V,W be non empty ModuleStr over K;

      let f,g be homogeneousSAF Form of V, W;

      cluster (f - g) -> homogeneousSAF;

      correctness ;

    end

    registration

      let K be add-associative right_zeroed right_complementable right-distributive non empty doubleLoopStr;

      let V,W be non empty ModuleStr over K;

      let f,g be homogeneousFAF Form of V, W;

      cluster (f - g) -> homogeneousFAF;

      correctness ;

    end

    theorem :: BILINEAR:26

    

     Th26: for K be non empty addLoopStr holds for V,W be non empty ModuleStr over K holds for v,u be Vector of V, w be Vector of W, f be Form of V, W st f is additiveSAF holds (f . ((v + u),w)) = ((f . (v,w)) + (f . (u,w)))

    proof

      let K be non empty addLoopStr;

      let V,W be non empty ModuleStr over K;

      let v,w be Vector of V, y be Vector of W, f be Form of V, W;

      set F = ( FunctionalSAF (f,y));

      assume f is additiveSAF;

      then

       A1: F is additive;

      

      thus (f . ((v + w),y)) = (F . (v + w)) by Th9

      .= ((F . v) + (F . w)) by A1

      .= ((f . (v,y)) + (F . w)) by Th9

      .= ((f . (v,y)) + (f . (w,y))) by Th9;

    end;

    theorem :: BILINEAR:27

    

     Th27: for K be non empty addLoopStr holds for V,W be non empty ModuleStr over K holds for v be Vector of V, u,w be Vector of W, f be Form of V, W st f is additiveFAF holds (f . (v,(u + w))) = ((f . (v,u)) + (f . (v,w)))

    proof

      let K be non empty addLoopStr;

      let V,W be non empty ModuleStr over K;

      let v be Vector of V, y,z be Vector of W, f be Form of V, W;

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

      assume f is additiveFAF;

      then

       A1: F is additive;

      

      thus (f . (v,(y + z))) = (F . (y + z)) by Th8

      .= ((F . y) + (F . z)) by A1

      .= ((f . (v,y)) + (F . z)) by Th8

      .= ((f . (v,y)) + (f . (v,z))) by Th8;

    end;

    theorem :: BILINEAR:28

    

     Th28: for K be right_zeroed non empty addLoopStr holds for V,W be non empty ModuleStr over K holds for v,u be Vector of V, w,t be Vector of W, f be additiveSAF additiveFAF Form of V, W holds (f . ((v + u),(w + t))) = (((f . (v,w)) + (f . (v,t))) + ((f . (u,w)) + (f . (u,t))))

    proof

      let K be right_zeroed non empty addLoopStr;

      let V,W be non empty ModuleStr over K;

      let v,w be Vector of V, y,z be Vector of W, f be additiveSAF additiveFAF Form 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 Th26

      .= ((v1 + v3) + (f . (w,(y + z)))) by Th27

      .= ((v1 + v3) + (v4 + v5)) by Th27;

    end;

    theorem :: BILINEAR:29

    

     Th29: for K be add-associative right_zeroed right_complementable non empty doubleLoopStr holds for V,W be right_zeroed non empty ModuleStr over K holds for f be additiveFAF Form of V, W, v be Vector of V holds (f . (v,( 0. W))) = ( 0. K)

    proof

      let F be add-associative right_zeroed right_complementable non empty doubleLoopStr;

      let V,W be right_zeroed non empty ModuleStr over F;

      let f be additiveFAF Form 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 Th27;

      hence thesis by RLVECT_1: 9;

    end;

    theorem :: BILINEAR:30

    

     Th30: for K be add-associative right_zeroed right_complementable non empty doubleLoopStr holds for V,W be right_zeroed non empty ModuleStr over K holds for f be additiveSAF Form of V, W, w be Vector of W holds (f . (( 0. V),w)) = ( 0. K)

    proof

      let F be add-associative right_zeroed right_complementable non empty doubleLoopStr;

      let V,W be right_zeroed non empty ModuleStr over F;

      let f be additiveSAF Form 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 Th26;

      hence thesis by RLVECT_1: 9;

    end;

    theorem :: BILINEAR:31

    

     Th31: for K be non empty multMagma holds for V,W be non empty ModuleStr over K holds for v be Vector of V, w be Vector of W, a be Element of K holds for f be Form of V, W st f is homogeneousSAF holds (f . ((a * v),w)) = (a * (f . (v,w)))

    proof

      let K be non empty multMagma;

      let V,W be non empty ModuleStr over K;

      let v be Vector of V, y be Vector of W, r be Element of K, f be Form of V, W;

      set F = ( FunctionalSAF (f,y));

      assume f is homogeneousSAF;

      then

       A1: F is homogeneous;

      

      thus (f . ((r * v),y)) = (F . (r * v)) by Th9

      .= (r * (F . v)) by A1

      .= (r * (f . (v,y))) by Th9;

    end;

    theorem :: BILINEAR:32

    

     Th32: for K be non empty multMagma holds for V,W be non empty ModuleStr over K holds for v be Vector of V, w be Vector of W, a be Element of K holds for f be Form of V, W st f is homogeneousFAF holds (f . (v,(a * w))) = (a * (f . (v,w)))

    proof

      let K be non empty multMagma;

      let V,W be non empty ModuleStr over K;

      let v be Vector of V, y be Vector of W, r be Element of K, f be Form of V, W;

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

      assume f is homogeneousFAF;

      then

       A1: F is homogeneous;

      

      thus (f . (v,(r * y))) = (F . (r * y)) by Th8

      .= (r * (F . y)) by A1

      .= (r * (f . (v,y))) by Th8;

    end;

    theorem :: BILINEAR:33

    

     Th33: for K be add-associative right_zeroed right_complementable associative left_unital distributive non empty doubleLoopStr holds for V,W be add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital non empty ModuleStr over K holds for f be homogeneousSAF Form of V, W, w be Vector of W holds (f . (( 0. V),w)) = ( 0. K)

    proof

      let F be add-associative right_zeroed right_complementable associative left_unital distributive non empty doubleLoopStr;

      let V,W be add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital non empty ModuleStr over F;

      let f be homogeneousSAF Form of V, W, v be Vector of W;

      

      thus (f . (( 0. V),v)) = (f . ((( 0. F) * ( 0. V)),v)) by VECTSP10: 1

      .= (( 0. F) * (f . (( 0. V),v))) by Th31

      .= ( 0. F);

    end;

    theorem :: BILINEAR:34

    

     Th34: for K be add-associative right_zeroed right_complementable associative left_unital distributive non empty doubleLoopStr holds for V,W be add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital non empty ModuleStr over K holds for f be homogeneousFAF Form of V, W, v be Vector of V holds (f . (v,( 0. W))) = ( 0. K)

    proof

      let F be add-associative right_zeroed right_complementable associative left_unital distributive non empty doubleLoopStr;

      let V,W be add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital non empty ModuleStr over F;

      let f be homogeneousFAF Form of V, W, v be Vector of V;

      

      thus (f . (v,( 0. W))) = (f . (v,(( 0. F) * ( 0. W)))) by VECTSP10: 1

      .= (( 0. F) * (f . (v,( 0. W)))) by Th32

      .= ( 0. F);

    end;

    theorem :: BILINEAR:35

    

     Th35: for K be add-associative right_zeroed right_complementable Abelian associative well-unital distributive non empty doubleLoopStr holds for V,W be VectSp of K holds for v,u be Vector of V, w be Vector of W, f be additiveSAF homogeneousSAF Form of V, W holds (f . ((v - u),w)) = ((f . (v,w)) - (f . (u,w)))

    proof

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

      let V,W be VectSp of K, v,w be Vector of V, y be Vector of W;

      let f be additiveSAF homogeneousSAF Form of V, W;

      

      thus (f . ((v - w),y)) = (f . ((v + ( - w)),y)) by RLVECT_1:def 11

      .= ((f . (v,y)) + (f . (( - w),y))) by Th26

      .= ((f . (v,y)) + (f . ((( - ( 1. K)) * w),y))) by VECTSP_1: 14

      .= ((f . (v,y)) + (( - ( 1. K)) * (f . (w,y)))) by Th31

      .= ((f . (v,y)) + ( - (( 1. K) * (f . (w,y))))) by VECTSP_1: 9

      .= ((f . (v,y)) - (( 1. K) * (f . (w,y)))) by RLVECT_1:def 11

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

    end;

    theorem :: BILINEAR:36

    

     Th36: for K be add-associative right_zeroed right_complementable Abelian associative well-unital distributive non empty doubleLoopStr holds for V,W be VectSp of K holds for v be Vector of V, w,t be Vector of W, f be additiveFAF homogeneousFAF Form of V, W holds (f . (v,(w - t))) = ((f . (v,w)) - (f . (v,t)))

    proof

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

      let V,W be VectSp of K, v be Vector of V, y,z be Vector of W, f be additiveFAF homogeneousFAF Form of V, W;

      

      thus (f . (v,(y - z))) = (f . (v,(y + ( - z)))) by RLVECT_1:def 11

      .= ((f . (v,y)) + (f . (v,( - z)))) by Th27

      .= ((f . (v,y)) + (f . (v,(( - ( 1. K)) * z)))) by VECTSP_1: 14

      .= ((f . (v,y)) + (( - ( 1. K)) * (f . (v,z)))) by Th32

      .= ((f . (v,y)) + ( - (( 1. K) * (f . (v,z))))) by VECTSP_1: 9

      .= ((f . (v,y)) - (( 1. K) * (f . (v,z)))) by RLVECT_1:def 11

      .= ((f . (v,y)) - (f . (v,z)));

    end;

    theorem :: BILINEAR:37

    

     Th37: for K be add-associative right_zeroed right_complementable Abelian associative well-unital distributive non empty doubleLoopStr holds for V,W be VectSp of K holds for v,u be Vector of V, w,t be Vector of W, f be bilinear-Form of V, W holds (f . ((v - u),(w - t))) = (((f . (v,w)) - (f . (v,t))) - ((f . (u,w)) - (f . (u,t))))

    proof

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

      let V,W be VectSp of K;

      let v,w be Vector of V, y,z be Vector of W, f be bilinear-Form 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 Th35

      .= ((v1 - v3) - (f . (w,(y - z)))) by Th36

      .= ((v1 - v3) - (v4 - v5)) by Th36;

    end;

    theorem :: BILINEAR:38

    for K be add-associative right_zeroed right_complementable associative well-unital distributive non empty doubleLoopStr holds for V,W be add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital non empty ModuleStr over K holds for v,u be Vector of V, w,t be Vector of W, a,b be Element of K holds for f be bilinear-Form 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 K be add-associative right_zeroed right_complementable associative well-unital distributive non empty doubleLoopStr;

      let V,W be add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital non empty ModuleStr over K, v,w be Vector of V, y,z be Vector of W, a,b be Element of K;

      let f be bilinear-Form 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 Th28

      .= ((v1 + (b * v3)) + ((f . ((a * w),y)) + (f . ((a * w),(b * z))))) by Th32

      .= ((v1 + (b * v3)) + ((a * v4) + (f . ((a * w),(b * z))))) by Th31

      .= ((v1 + (b * v3)) + ((a * v4) + (a * (f . (w,(b * z)))))) by Th31

      .= ((v1 + (b * v3)) + ((a * v4) + (a * (b * v5)))) by Th32;

    end;

    theorem :: BILINEAR:39

    for K be add-associative right_zeroed right_complementable Abelian associative well-unital distributive non empty doubleLoopStr holds for V,W be VectSp of K holds for v,u be Vector of V, w,t be Vector of W, a,b be Element of K holds for f be bilinear-Form 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 K be add-associative right_zeroed right_complementable Abelian associative well-unital distributive non empty doubleLoopStr, V,W be VectSp of K, v,w be Vector of V, y,z be Vector of W, a,b be Element of K, f be bilinear-Form 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 Th37

      .= ((v1 - (b * v3)) - ((f . ((a * w),y)) - (f . ((a * w),(b * z))))) by Th32

      .= ((v1 - (b * v3)) - ((a * v4) - (f . ((a * w),(b * z))))) by Th31

      .= ((v1 - (b * v3)) - ((a * v4) - (a * (f . (w,(b * z)))))) by Th31

      .= ((v1 - (b * v3)) - ((a * v4) - (a * (b * v5)))) by Th32;

    end;

    theorem :: BILINEAR:40

    

     Th40: for K be add-associative right_zeroed right_complementable non empty doubleLoopStr, V,W be right_zeroed non empty ModuleStr over K, f be Form 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. K)

    proof

      let K be add-associative right_zeroed right_complementable non empty doubleLoopStr, V,W be right_zeroed non empty ModuleStr over K, f be Form 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. K) by A4, Th29;

        end;

          suppose

           A5: f is additiveSAF;

          

          thus (f . (v,w)) = (f . (( 0. V),w)) by A1, A3, BINOP_1: 19

          .= ( 0. K) by A5, Th30;

        end;

      end;

      hereby

        assume

         A6: for v be Vector of V, w be Vector of W holds (f . (v,w)) = ( 0. K);

        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. K) 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 K be ZeroStr;

      let V,W be non empty ModuleStr over K;

      let f be Form of V, W;

      :: BILINEAR:def15

      func leftker f -> Subset of V equals { v where v be Vector of V : for w be Vector of W holds (f . (v,w)) = ( 0. K) };

      correctness

      proof

        set A = { v where v be Vector of V : for w be Vector of W holds (f . (v,w)) = ( 0. K) };

        A c= the carrier of V

        proof

          let x be object;

          assume x in A;

          then ex v be Vector of V st v = x & for w be Vector of W holds (f . (v,w)) = ( 0. K);

          hence thesis;

        end;

        hence thesis;

      end;

    end

    definition

      let K be ZeroStr;

      let V,W be non empty ModuleStr over K;

      let f be Form of V, W;

      :: BILINEAR:def16

      func rightker f -> Subset of W equals { w where w be Vector of W : for v be Vector of V holds (f . (v,w)) = ( 0. K) };

      correctness

      proof

        set A = { w where w be Vector of W : for v be Vector of V holds (f . (v,w)) = ( 0. K) };

        A c= the carrier of W

        proof

          let x be object;

          assume x in A;

          then ex w be Vector of W st w = x & for v be Vector of V holds (f . (v,w)) = ( 0. K);

          hence thesis;

        end;

        hence thesis;

      end;

    end

    definition

      let K be ZeroStr;

      let V be non empty ModuleStr over K;

      let f be Form of V, V;

      :: BILINEAR:def17

      func diagker f -> Subset of V equals { v where v be Vector of V : (f . (v,v)) = ( 0. K) };

      correctness

      proof

        set A = { v where v be Vector of V : (f . (v,v)) = ( 0. K) };

        A c= the carrier of V

        proof

          let x be object;

          assume x in A;

          then ex v be Vector of V st v = x & (f . (v,v)) = ( 0. K);

          hence thesis;

        end;

        hence thesis;

      end;

    end

    registration

      let K be add-associative right_zeroed right_complementable right-distributive non empty doubleLoopStr;

      let V be right_zeroed non empty ModuleStr over K;

      let W be non empty ModuleStr over K;

      let f be additiveSAF Form of V, W;

      cluster ( leftker f) -> non empty;

      coherence

      proof

        now

          let w be Vector of W;

          

          thus (f . (( 0. V),w)) = (( FunctionalSAF (f,w)) . ( 0. V)) by Th9

          .= ( 0. K) by HAHNBAN1:def 9;

        end;

        then ( 0. V) in ( leftker f);

        hence thesis;

      end;

    end

    registration

      let K be add-associative right_zeroed right_complementable associative well-unital distributive non empty doubleLoopStr;

      let V be add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital non empty ModuleStr over K;

      let W be non empty ModuleStr over K;

      let f be homogeneousSAF Form of V, W;

      cluster ( leftker f) -> non empty;

      coherence

      proof

        now

          let w be Vector of W;

          

          thus (f . (( 0. V),w)) = (( FunctionalSAF (f,w)) . ( 0. V)) by Th9

          .= ( 0. K) by HAHNBAN1:def 9;

        end;

        then ( 0. V) in ( leftker f);

        hence thesis;

      end;

    end

    registration

      let K be add-associative right_zeroed right_complementable right-distributive non empty doubleLoopStr;

      let V be non empty ModuleStr over K;

      let W be right_zeroed non empty ModuleStr over K;

      let f be additiveFAF Form of V, W;

      cluster ( rightker f) -> non empty;

      coherence

      proof

        now

          let v be Vector of V;

          

          thus (f . (v,( 0. W))) = (( FunctionalFAF (f,v)) . ( 0. W)) by Th8

          .= ( 0. K) by HAHNBAN1:def 9;

        end;

        then ( 0. W) in ( rightker f);

        hence thesis;

      end;

    end

    registration

      let K be add-associative right_zeroed right_complementable associative well-unital distributive non empty doubleLoopStr;

      let V be non empty ModuleStr over K;

      let W be add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital non empty ModuleStr over K;

      let f be homogeneousFAF Form of V, W;

      cluster ( rightker f) -> non empty;

      coherence

      proof

        now

          let v be Vector of V;

          

          thus (f . (v,( 0. W))) = (( FunctionalFAF (f,v)) . ( 0. W)) by Th8

          .= ( 0. K) by HAHNBAN1:def 9;

        end;

        then ( 0. W) in ( rightker f);

        hence thesis;

      end;

    end

    registration

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

      let V be right_zeroed non empty ModuleStr over K;

      let f be additiveFAF Form of V, V;

      cluster ( diagker f) -> non empty;

      coherence

      proof

        (f . (( 0. V),( 0. V))) = ( 0. K) by Th29;

        then ( 0. V) in ( diagker f);

        hence thesis;

      end;

    end

    registration

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

      let V be right_zeroed non empty ModuleStr over K;

      let f be additiveSAF Form of V, V;

      cluster ( diagker f) -> non empty;

      coherence

      proof

        (f . (( 0. V),( 0. V))) = ( 0. K) by Th30;

        then ( 0. V) in ( diagker f);

        hence thesis;

      end;

    end

    registration

      let K be add-associative right_zeroed right_complementable associative well-unital distributive non empty doubleLoopStr;

      let V be add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital non empty ModuleStr over K;

      let f be homogeneousFAF Form of V, V;

      cluster ( diagker f) -> non empty;

      coherence

      proof

        (f . (( 0. V),( 0. V))) = ( 0. K) by Th34;

        then ( 0. V) in ( diagker f);

        hence thesis;

      end;

    end

    registration

      let K be add-associative right_zeroed right_complementable associative well-unital distributive non empty doubleLoopStr;

      let V be add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital non empty ModuleStr over K;

      let f be homogeneousSAF Form of V, V;

      cluster ( diagker f) -> non empty;

      coherence

      proof

        (f . (( 0. V),( 0. V))) = ( 0. K) by Th33;

        then ( 0. V) in ( diagker f);

        hence thesis;

      end;

    end

    theorem :: BILINEAR:41

    for K be ZeroStr, V be non empty ModuleStr over K holds for f be Form of V, V holds ( leftker f) c= ( diagker f) & ( rightker f) c= ( diagker f)

    proof

      let K be ZeroStr, V be non empty ModuleStr over K, f be Form of V, V;

      thus ( leftker f) c= ( diagker f)

      proof

        let x be object;

        assume x in ( leftker f);

        then

        consider v be Vector of V such that

         A1: v = x and

         A2: for w be Vector of V holds (f . (v,w)) = ( 0. K);

        (f . (v,v)) = ( 0. K) by A2;

        hence thesis by A1;

      end;

      let x be object;

      assume x in ( rightker f);

      then

      consider v be Vector of V such that

       A3: v = x and

       A4: for w be Vector of V holds (f . (w,v)) = ( 0. K);

      (f . (v,v)) = ( 0. K) by A4;

      hence thesis by A3;

    end;

    theorem :: BILINEAR:42

    

     Th42: for K be add-associative right_zeroed right_complementable right-distributive non empty doubleLoopStr holds for V,W be non empty ModuleStr over K holds for f be additiveSAF homogeneousSAF Form of V, W holds ( leftker f) is linearly-closed

    proof

      let K be add-associative right_zeroed right_complementable right-distributive non empty doubleLoopStr;

      let V,W be non empty ModuleStr over K;

      let f be additiveSAF homogeneousSAF Form of V, W;

      set V1 = ( leftker f);

      thus for v,u be Vector of V st v in V1 & u in V1 holds (v + u) in V1

      proof

        let v,u be Vector of V;

        assume that

         A1: v in V1 and

         A2: u in V1;

        consider u1 be Vector of V such that

         A3: u1 = u and

         A4: for w be Vector of W holds (f . (u1,w)) = ( 0. K) by A2;

        consider v1 be Vector of V such that

         A5: v1 = v and

         A6: for w be Vector of W holds (f . (v1,w)) = ( 0. K) by A1;

        now

          let w be Vector of W;

          

          thus (f . ((v + u),w)) = ((f . (v1,w)) + (f . (u1,w))) by A5, A3, Th26

          .= (( 0. K) + (f . (u1,w))) by A6

          .= (( 0. K) + ( 0. K)) by A4

          .= ( 0. K) by RLVECT_1:def 4;

        end;

        hence thesis;

      end;

      let a be Element of K, v be Vector of V;

      assume v in V1;

      then

      consider v1 be Vector of V such that

       A7: v1 = v and

       A8: for w be Vector of W holds (f . (v1,w)) = ( 0. K);

      now

        let w be Vector of W;

        

        thus (f . ((a * v),w)) = (a * (f . (v1,w))) by A7, Th31

        .= (a * ( 0. K)) by A8

        .= ( 0. K);

      end;

      hence thesis;

    end;

    theorem :: BILINEAR:43

    

     Th43: for K be add-associative right_zeroed right_complementable right-distributive non empty doubleLoopStr holds for V,W be non empty ModuleStr over K holds for f be additiveFAF homogeneousFAF Form of V, W holds ( rightker f) is linearly-closed

    proof

      let K be add-associative right_zeroed right_complementable right-distributive non empty doubleLoopStr;

      let V,W be non empty ModuleStr over K;

      let f be additiveFAF homogeneousFAF Form of V, W;

      set V1 = ( rightker f);

      thus for v,u be Vector of W st v in V1 & u in V1 holds (v + u) in V1

      proof

        let v,u be Vector of W;

        assume that

         A1: v in V1 and

         A2: u in V1;

        consider u1 be Vector of W such that

         A3: u1 = u and

         A4: for w be Vector of V holds (f . (w,u1)) = ( 0. K) by A2;

        consider v1 be Vector of W such that

         A5: v1 = v and

         A6: for w be Vector of V holds (f . (w,v1)) = ( 0. K) by A1;

        now

          let w be Vector of V;

          

          thus (f . (w,(v + u))) = ((f . (w,v1)) + (f . (w,u1))) by A5, A3, Th27

          .= (( 0. K) + (f . (w,u1))) by A6

          .= (( 0. K) + ( 0. K)) by A4

          .= ( 0. K) by RLVECT_1:def 4;

        end;

        hence thesis;

      end;

      let a be Element of K, v be Vector of W;

      assume v in V1;

      then

      consider v1 be Vector of W such that

       A7: v1 = v and

       A8: for w be Vector of V holds (f . (w,v1)) = ( 0. K);

      now

        let w be Vector of V;

        

        thus (f . (w,(a * v))) = (a * (f . (w,v1))) by A7, Th32

        .= (a * ( 0. K)) by A8

        .= ( 0. K);

      end;

      hence thesis;

    end;

    definition

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

      let V be VectSp of K, W be non empty ModuleStr over K;

      let f be additiveSAF homogeneousSAF Form of V, W;

      :: BILINEAR:def18

      func LKer f -> strict non empty Subspace of V means

      : Def18: the carrier of it = ( leftker f);

      existence by Th42, VECTSP_4: 34;

      uniqueness by VECTSP_4: 29;

    end

    definition

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

      let V be non empty ModuleStr over K, W be VectSp of K;

      let f be additiveFAF homogeneousFAF Form of V, W;

      :: BILINEAR:def19

      func RKer f -> strict non empty Subspace of W means

      : Def19: the carrier of it = ( rightker f);

      existence by Th43, VECTSP_4: 34;

      uniqueness by VECTSP_4: 29;

    end

    definition

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

      let V be VectSp of K, W be non empty ModuleStr over K;

      let f be additiveSAF homogeneousSAF Form of V, W;

      :: BILINEAR:def20

      func LQForm (f) -> additiveSAF homogeneousSAF Form of ( VectQuot (V,( LKer f))), W means

      : Def20: for A be Vector of ( VectQuot (V,( LKer f))), w be Vector of W, v be Vector of V st A = (v + ( LKer f)) holds (it . (A,w)) = (f . (v,w));

      existence

      proof

        set L = ( LKer f), vq = ( VectQuot (V,L)), C = ( CosetSet (V,L)), aC = ( addCoset (V,L)), mC = ( lmultCoset (V,L));

        defpred P[ set, set, set] means for a be Vector of V st $1 = (a + L) holds $3 = (f . (a,$2));

         A1:

        now

          let A be Vector of vq, w0 be Vector of W;

          consider a be Vector of V such that

           A2: A = (a + L) by VECTSP10: 22;

          take y = (f . (a,w0));

          now

            let a1 be Vector of V;

            assume A = (a1 + L);

            then a in (a1 + L) by A2, VECTSP_4: 44;

            then

            consider w be Vector of V such that

             A3: w in L and

             A4: a = (a1 + w) by VECTSP_4: 42;

            w in the carrier of L by A3;

            then w in ( leftker f) by Def18;

            then

             A5: ex aa be Vector of V st aa = w & for ww be Vector of W holds (f . (aa,ww)) = ( 0. K);

            

            thus y = ((f . (a1,w0)) + (f . (w,w0))) by A4, Th26

            .= ((f . (a1,w0)) + ( 0. K)) by A5

            .= (f . (a1,w0)) by RLVECT_1:def 4;

          end;

          hence P[A, w0, y];

        end;

        consider ff be Function of [:the carrier of vq, the carrier of W:], the carrier of K such that

         A6: for A be Vector of vq, w be Vector of W holds P[A, w, (ff . (A,w))] from BINOP_1:sch 3( A1);

        reconsider ff as Form of vq, W;

        

         A7: C = the carrier of vq by VECTSP10:def 6;

        now

          let w be Vector of W;

          set ffw = ( FunctionalSAF (ff,w));

          now

            let A,B be Vector of vq;

            consider a be Vector of V such that

             A8: A = (a + L) by VECTSP10: 22;

            consider b be Vector of V such that

             A9: B = (b + L) by VECTSP10: 22;

            

             A10: the addF of vq = ( addCoset (V,L)) & (aC . (A,B)) = ((a + b) + L) by A7, A8, A9, VECTSP10:def 3, VECTSP10:def 6;

            

            thus (ffw . (A + B)) = (ff . ((A + B),w)) by Th9

            .= (f . ((a + b),w)) by A6, A10, RLVECT_1: 2

            .= ((f . (a,w)) + (f . (b,w))) by Th26

            .= ((ff . (A,w)) + (f . (b,w))) by A6, A8

            .= ((ff . (A,w)) + (ff . (B,w))) by A6, A9

            .= ((ffw . A) + (ff . (B,w))) by Th9

            .= ((ffw . A) + (ffw . B)) by Th9;

          end;

          hence ffw is additive;

        end;

        then

        reconsider ff as additiveSAF Form of vq, W by Def12;

        now

          let w be Vector of W;

          set ffw = ( FunctionalSAF (ff,w));

          now

            let A be Vector of vq, r be Element of K;

            consider a be Vector of V such that

             A11: A = (a + L) by VECTSP10: 22;

            

             A12: the lmult of vq = ( lmultCoset (V,L)) & (mC . (r,A)) = ((r * a) + L) by A7, A11, VECTSP10:def 5, VECTSP10:def 6;

            

            thus (ffw . (r * A)) = (ff . ((r * A),w)) by Th9

            .= (f . ((r * a),w)) by A6, A12

            .= (r * (f . (a,w))) by Th31

            .= (r * (ff . (A,w))) by A6, A11

            .= (r * (ffw . A)) by Th9;

          end;

          hence ffw is homogeneous;

        end;

        then

        reconsider ff as additiveSAF homogeneousSAF Form of vq, W by Def14;

        take ff;

        thus thesis by A6;

      end;

      uniqueness

      proof

        set L = ( LKer f), vq = ( VectQuot (V,L));

        let f1,f2 be additiveSAF homogeneousSAF Form of vq, W such that

         A13: for A be Vector of vq, w be Vector of W, a be Vector of V st A = (a + ( LKer f)) holds (f1 . (A,w)) = (f . (a,w)) and

         A14: for A be Vector of vq, w be Vector of W, a be Vector of V st A = (a + ( LKer f)) holds (f2 . (A,w)) = (f . (a,w));

        now

          let A be Vector of vq, w be Vector of W;

          consider a be Vector of V such that

           A15: A = (a + L) by VECTSP10: 22;

          

          thus (f1 . (A,w)) = (f . (a,w)) by A13, A15

          .= (f2 . (A,w)) by A14, A15;

        end;

        hence thesis;

      end;

    end

    definition

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

      let V be non empty ModuleStr over K, W be VectSp of K;

      let f be additiveFAF homogeneousFAF Form of V, W;

      :: BILINEAR:def21

      func RQForm (f) -> additiveFAF homogeneousFAF Form of V, ( VectQuot (W,( RKer f))) means

      : Def21: for A be Vector of ( VectQuot (W,( RKer f))), v be Vector of V, w be Vector of W st A = (w + ( RKer f)) holds (it . (v,A)) = (f . (v,w));

      existence

      proof

        set L = ( RKer f), vq = ( VectQuot (W,L)), C = ( CosetSet (W,L)), aC = ( addCoset (W,L)), mC = ( lmultCoset (W,L));

        defpred P[ set, set, set] means for w be Vector of W st $2 = (w + L) holds $3 = (f . ($1,w));

         A1:

        now

          let v0 be Vector of V, A be Vector of vq;

          consider a be Vector of W such that

           A2: A = (a + L) by VECTSP10: 22;

          take y = (f . (v0,a));

          now

            let a1 be Vector of W;

            assume A = (a1 + L);

            then a in (a1 + L) by A2, VECTSP_4: 44;

            then

            consider w be Vector of W such that

             A3: w in L and

             A4: a = (a1 + w) by VECTSP_4: 42;

            w in the carrier of L by A3;

            then w in ( rightker f) by Def19;

            then

             A5: ex aa be Vector of W st aa = w & for vv be Vector of V holds (f . (vv,aa)) = ( 0. K);

            

            thus y = ((f . (v0,a1)) + (f . (v0,w))) by A4, Th27

            .= ((f . (v0,a1)) + ( 0. K)) by A5

            .= (f . (v0,a1)) by RLVECT_1:def 4;

          end;

          hence P[v0, A, y];

        end;

        consider ff be Function of [:the carrier of V, the carrier of vq:], the carrier of K such that

         A6: for v be Vector of V, A be Vector of vq holds P[v, A, (ff . (v,A))] from BINOP_1:sch 3( A1);

        reconsider ff as Form of V, vq;

        

         A7: C = the carrier of vq by VECTSP10:def 6;

        now

          let v be Vector of V;

          set ffw = ( FunctionalFAF (ff,v));

          now

            let A,B be Vector of vq;

            consider a be Vector of W such that

             A8: A = (a + L) by VECTSP10: 22;

            consider b be Vector of W such that

             A9: B = (b + L) by VECTSP10: 22;

            

             A10: the addF of vq = ( addCoset (W,L)) & (aC . (A,B)) = ((a + b) + L) by A7, A8, A9, VECTSP10:def 3, VECTSP10:def 6;

            

            thus (ffw . (A + B)) = (ff . (v,(A + B))) by Th8

            .= (f . (v,(a + b))) by A6, A10, RLVECT_1: 2

            .= ((f . (v,a)) + (f . (v,b))) by Th27

            .= ((ff . (v,A)) + (f . (v,b))) by A6, A8

            .= ((ff . (v,A)) + (ff . (v,B))) by A6, A9

            .= ((ffw . A) + (ff . (v,B))) by Th8

            .= ((ffw . A) + (ffw . B)) by Th8;

          end;

          hence ffw is additive;

        end;

        then

        reconsider ff as additiveFAF Form of V, vq by Def11;

        now

          let v be Vector of V;

          set ffw = ( FunctionalFAF (ff,v));

          now

            let A be Vector of vq, r be Element of K;

            consider a be Vector of W such that

             A11: A = (a + L) by VECTSP10: 22;

            

             A12: the lmult of vq = ( lmultCoset (W,L)) & (mC . (r,A)) = ((r * a) + L) by A7, A11, VECTSP10:def 5, VECTSP10:def 6;

            

            thus (ffw . (r * A)) = (ff . (v,(r * A))) by Th8

            .= (f . (v,(r * a))) by A6, A12

            .= (r * (f . (v,a))) by Th32

            .= (r * (ff . (v,A))) by A6, A11

            .= (r * (ffw . A)) by Th8;

          end;

          hence ffw is homogeneous;

        end;

        then

        reconsider ff as additiveFAF homogeneousFAF Form of V, vq by Def13;

        take ff;

        thus thesis by A6;

      end;

      uniqueness

      proof

        set L = ( RKer f), vq = ( VectQuot (W,L));

        let f1,f2 be additiveFAF homogeneousFAF Form of V, vq such that

         A13: for A be Vector of vq, v be Vector of V, a be Vector of W st A = (a + ( RKer f)) holds (f1 . (v,A)) = (f . (v,a)) and

         A14: for A be Vector of vq, v be Vector of V, a be Vector of W st A = (a + ( RKer f)) holds (f2 . (v,A)) = (f . (v,a));

        now

          let v be Vector of V, A be Vector of vq;

          consider a be Vector of W such that

           A15: A = (a + L) by VECTSP10: 22;

          

          thus (f1 . (v,A)) = (f . (v,a)) by A13, A15

          .= (f2 . (v,A)) by A14, A15;

        end;

        hence thesis;

      end;

    end

    registration

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

      let V,W be VectSp of K;

      let f be bilinear-Form of V, W;

      cluster ( LQForm f) -> additiveFAF homogeneousFAF;

      coherence

      proof

        set lf = ( LQForm f);

        thus ( LQForm f) is additiveFAF

        proof

          let A be Vector of ( VectQuot (V,( LKer f)));

          set flf = ( FunctionalFAF (lf,A));

          consider v be Vector of V such that

           A1: A = (v + ( LKer f)) by VECTSP10: 22;

          let w,t be Vector of W;

          

          thus (flf . (w + t)) = (lf . (A,(w + t))) by Th8

          .= (f . (v,(w + t))) by A1, Def20

          .= ((f . (v,w)) + (f . (v,t))) by Th27

          .= ((lf . (A,w)) + (f . (v,t))) by A1, Def20

          .= ((lf . (A,w)) + (lf . (A,t))) by A1, Def20

          .= ((flf . w) + (lf . (A,t))) by Th8

          .= ((flf . w) + (flf . t)) by Th8;

        end;

        let A be Vector of ( VectQuot (V,( LKer f)));

        set flf = ( FunctionalFAF (lf,A));

        consider v be Vector of V such that

         A2: A = (v + ( LKer f)) by VECTSP10: 22;

        let w be Vector of W, r be Scalar of W;

        

        thus (flf . (r * w)) = (lf . (A,(r * w))) by Th8

        .= (f . (v,(r * w))) by A2, Def20

        .= (r * (f . (v,w))) by Th32

        .= (r * (lf . (A,w))) by A2, Def20

        .= (r * (flf . w)) by Th8;

      end;

      cluster ( RQForm f) -> additiveSAF homogeneousSAF;

      coherence

      proof

        set lf = ( RQForm f);

        thus ( RQForm f) is additiveSAF

        proof

          let A be Vector of ( VectQuot (W,( RKer f)));

          set flf = ( FunctionalSAF (lf,A));

          consider w be Vector of W such that

           A3: A = (w + ( RKer f)) by VECTSP10: 22;

          let v,t be Vector of V;

          

          thus (flf . (v + t)) = (lf . ((v + t),A)) by Th9

          .= (f . ((v + t),w)) by A3, Def21

          .= ((f . (v,w)) + (f . (t,w))) by Th26

          .= ((lf . (v,A)) + (f . (t,w))) by A3, Def21

          .= ((lf . (v,A)) + (lf . (t,A))) by A3, Def21

          .= ((flf . v) + (lf . (t,A))) by Th9

          .= ((flf . v) + (flf . t)) by Th9;

        end;

        let A be Vector of ( VectQuot (W,( RKer f)));

        set flf = ( FunctionalSAF (lf,A));

        consider w be Vector of W such that

         A4: A = (w + ( RKer f)) by VECTSP10: 22;

        let v be Vector of V, r be Scalar of V;

        

        thus (flf . (r * v)) = (lf . ((r * v),A)) by Th9

        .= (f . ((r * v),w)) by A4, Def21

        .= (r * (f . (v,w))) by Th31

        .= (r * (lf . (v,A))) by A4, Def21

        .= (r * (flf . v)) by Th9;

      end;

    end

    definition

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

      let V,W be VectSp of K;

      let f be bilinear-Form of V, W;

      :: BILINEAR:def22

      func QForm (f) -> bilinear-Form of ( VectQuot (V,( LKer f))), ( VectQuot (W,( RKer f))) means

      : Def22: for A be Vector of ( VectQuot (V,( LKer f))), B be Vector of ( VectQuot (W,( RKer f))) holds for v be Vector of V, w be Vector of W st A = (v + ( LKer f)) & B = (w + ( RKer f)) holds (it . (A,B)) = (f . (v,w));

      existence

      proof

        set L = ( LKer f), vq = ( VectQuot (V,L)), Cv = ( CosetSet (V,L)), aCv = ( addCoset (V,L)), mCv = ( lmultCoset (V,L)), R = ( RKer f), wq = ( VectQuot (W,R)), Cw = ( CosetSet (W,R)), aCw = ( addCoset (W,R)), mCw = ( lmultCoset (W,R));

        defpred P[ set, set, set] means for v be Vector of V, w be Vector of W st $1 = (v + L) & $2 = (w + R) holds $3 = (f . (v,w));

         A1:

        now

          let A be Vector of vq, B be Vector of wq;

          consider a be Vector of V such that

           A2: A = (a + L) by VECTSP10: 22;

          consider b be Vector of W such that

           A3: B = (b + R) by VECTSP10: 22;

          take y = (f . (a,b));

          now

            let a1 be Vector of V;

            let b1 be Vector of W;

            assume A = (a1 + L);

            then a in (a1 + L) by A2, VECTSP_4: 44;

            then

            consider vv be Vector of V such that

             A4: vv in L and

             A5: a = (a1 + vv) by VECTSP_4: 42;

            vv in the carrier of L by A4;

            then vv in ( leftker f) by Def18;

            then

             A6: ex aa be Vector of V st aa = vv & for w0 be Vector of W holds (f . (aa,w0)) = ( 0. K);

            assume B = (b1 + R);

            then b in (b1 + R) by A3, VECTSP_4: 44;

            then

            consider ww be Vector of W such that

             A7: ww in R and

             A8: b = (b1 + ww) by VECTSP_4: 42;

            ww in the carrier of R by A7;

            then ww in ( rightker f) by Def19;

            then

             A9: ex bb be Vector of W st bb = ww & for v0 be Vector of V holds (f . (v0,bb)) = ( 0. K);

            

            thus y = (((f . (a1,b1)) + (f . (a1,ww))) + ((f . (vv,b1)) + (f . (vv,ww)))) by A5, A8, Th28

            .= (((f . (a1,b1)) + ( 0. K)) + ((f . (vv,b1)) + (f . (vv,ww)))) by A9

            .= (((f . (a1,b1)) + ( 0. K)) + (( 0. K) + (f . (vv,ww)))) by A6

            .= ((f . (a1,b1)) + (( 0. K) + (f . (vv,ww)))) by RLVECT_1:def 4

            .= ((f . (a1,b1)) + (f . (vv,ww))) by RLVECT_1: 4

            .= ((f . (a1,b1)) + ( 0. K)) by A6

            .= (f . (a1,b1)) by RLVECT_1:def 4;

          end;

          hence P[A, B, y];

        end;

        consider ff be Function of [:the carrier of vq, the carrier of wq:], the carrier of K such that

         A10: for A be Vector of vq, B be Vector of wq holds P[A, B, (ff . (A,B))] from BINOP_1:sch 3( A1);

        reconsider ff as Form of vq, wq;

        

         A11: Cv = the carrier of vq by VECTSP10:def 6;

         A12:

        now

          let ww be Vector of wq;

          consider w be Vector of W such that

           A13: ww = (w + R) by VECTSP10: 22;

          set ffw = ( FunctionalSAF (ff,ww));

          now

            let A be Vector of vq, r be Element of K;

            consider a be Vector of V such that

             A14: A = (a + L) by VECTSP10: 22;

            

             A15: the lmult of vq = mCv & (mCv . (r,A)) = ((r * a) + L) by A11, A14, VECTSP10:def 5, VECTSP10:def 6;

            

            thus (ffw . (r * A)) = (ff . ((r * A),ww)) by Th9

            .= (f . ((r * a),w)) by A10, A13, A15

            .= (r * (f . (a,w))) by Th31

            .= (r * (ff . (A,ww))) by A10, A13, A14

            .= (r * (ffw . A)) by Th9;

          end;

          hence ffw is homogeneous;

        end;

        

         A16: Cw = the carrier of wq by VECTSP10:def 6;

         A17:

        now

          let vv be Vector of vq;

          consider v be Vector of V such that

           A18: vv = (v + L) by VECTSP10: 22;

          set ffv = ( FunctionalFAF (ff,vv));

          now

            let A be Vector of wq, r be Element of K;

            consider a be Vector of W such that

             A19: A = (a + R) by VECTSP10: 22;

            

             A20: the lmult of wq = mCw & (mCw . (r,A)) = ((r * a) + R) by A16, A19, VECTSP10:def 5, VECTSP10:def 6;

            

            thus (ffv . (r * A)) = (ff . (vv,(r * A))) by Th8

            .= (f . (v,(r * a))) by A10, A18, A20

            .= (r * (f . (v,a))) by Th32

            .= (r * (ff . (vv,A))) by A10, A18, A19

            .= (r * (ffv . A)) by Th8;

          end;

          hence ffv is homogeneous;

        end;

         A21:

        now

          let ww be Vector of wq;

          consider w be Vector of W such that

           A22: ww = (w + R) by VECTSP10: 22;

          set ffw = ( FunctionalSAF (ff,ww));

          now

            let A,B be Vector of vq;

            consider a be Vector of V such that

             A23: A = (a + L) by VECTSP10: 22;

            consider b be Vector of V such that

             A24: B = (b + L) by VECTSP10: 22;

            

             A25: the addF of vq = aCv & (aCv . (A,B)) = ((a + b) + L) by A11, A23, A24, VECTSP10:def 3, VECTSP10:def 6;

            

            thus (ffw . (A + B)) = (ff . ((A + B),ww)) by Th9

            .= (f . ((a + b),w)) by A10, A22, A25, RLVECT_1: 2

            .= ((f . (a,w)) + (f . (b,w))) by Th26

            .= ((ff . (A,ww)) + (f . (b,w))) by A10, A22, A23

            .= ((ff . (A,ww)) + (ff . (B,ww))) by A10, A22, A24

            .= ((ffw . A) + (ff . (B,ww))) by Th9

            .= ((ffw . A) + (ffw . B)) by Th9;

          end;

          hence ffw is additive;

        end;

        now

          let vv be Vector of vq;

          consider v be Vector of V such that

           A26: vv = (v + L) by VECTSP10: 22;

          set ffv = ( FunctionalFAF (ff,vv));

          now

            let A,B be Vector of wq;

            consider a be Vector of W such that

             A27: A = (a + R) by VECTSP10: 22;

            consider b be Vector of W such that

             A28: B = (b + R) by VECTSP10: 22;

            

             A29: the addF of wq = aCw & (aCw . (A,B)) = ((a + b) + R) by A16, A27, A28, VECTSP10:def 3, VECTSP10:def 6;

            

            thus (ffv . (A + B)) = (ff . (vv,(A + B))) by Th8

            .= (f . (v,(a + b))) by A10, A26, A29, RLVECT_1: 2

            .= ((f . (v,a)) + (f . (v,b))) by Th27

            .= ((ff . (vv,A)) + (f . (v,b))) by A10, A26, A27

            .= ((ff . (vv,A)) + (ff . (vv,B))) by A10, A26, A28

            .= ((ffv . A) + (ff . (vv,B))) by Th8

            .= ((ffv . A) + (ffv . B)) by Th8;

          end;

          hence ffv is additive;

        end;

        then

        reconsider ff as bilinear-Form of vq, wq by A21, A12, A17, Def11, Def12, Def13, Def14;

        take ff;

        thus thesis by A10;

      end;

      uniqueness

      proof

        set L = ( LKer f), vq = ( VectQuot (V,L)), R = ( RKer f), wq = ( VectQuot (W,R));

        let f1,f2 be bilinear-Form of vq, wq;

        assume that

         A30: for A be Vector of vq, B be Vector of wq holds for v be Vector of V, w be Vector of W st A = (v + L) & B = (w + R) holds (f1 . (A,B)) = (f . (v,w)) and

         A31: for A be Vector of vq, B be Vector of wq holds for v be Vector of V, w be Vector of W st A = (v + L) & B = (w + R) holds (f2 . (A,B)) = (f . (v,w));

        now

          let A be Vector of vq, B be Vector of wq;

          consider a be Vector of V such that

           A32: A = (a + L) by VECTSP10: 22;

          consider b be Vector of W such that

           A33: B = (b + R) by VECTSP10: 22;

          

          thus (f1 . (A,B)) = (f . (a,b)) by A30, A32, A33

          .= (f2 . (A,B)) by A31, A32, A33;

        end;

        hence thesis;

      end;

    end

    theorem :: BILINEAR:44

    

     Th44: for K be add-associative right_zeroed right_complementable Abelian associative well-unital distributive non empty doubleLoopStr holds for V be VectSp of K, W be non empty ModuleStr over K holds for f be additiveSAF homogeneousSAF Form of V, W holds ( rightker f) = ( rightker ( LQForm f))

    proof

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

      let V be VectSp of K, W be non empty ModuleStr over K;

      let f be additiveSAF homogeneousSAF Form of V, W;

      set lf = ( LQForm f), qv = ( VectQuot (V,( LKer f)));

      thus ( rightker f) c= ( rightker ( LQForm f))

      proof

        let x be object;

        assume x in ( rightker f);

        then

        consider w be Vector of W such that

         A1: x = w and

         A2: for v be Vector of V holds (f . (v,w)) = ( 0. K);

        now

          let A be Vector of qv;

          consider v be Vector of V such that

           A3: A = (v + ( LKer f)) by VECTSP10: 22;

          

          thus (lf . (A,w)) = (f . (v,w)) by A3, Def20

          .= ( 0. K) by A2;

        end;

        hence thesis by A1;

      end;

      let x be object;

      assume x in ( rightker lf);

      then

      consider w be Vector of W such that

       A4: x = w and

       A5: for A be Vector of qv holds (lf . (A,w)) = ( 0. K);

      now

        let v be Vector of V;

        reconsider A = (v + ( LKer f)) as Vector of qv by VECTSP10: 23;

        

        thus (f . (v,w)) = (lf . (A,w)) by Def20

        .= ( 0. K) by A5;

      end;

      hence thesis by A4;

    end;

    theorem :: BILINEAR:45

    

     Th45: for K be add-associative right_zeroed right_complementable Abelian associative well-unital distributive non empty doubleLoopStr holds for V be non empty ModuleStr over K, W be VectSp of K holds for f be additiveFAF homogeneousFAF Form of V, W holds ( leftker f) = ( leftker ( RQForm f))

    proof

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

      let V be non empty ModuleStr over K, W be VectSp of K;

      let f be additiveFAF homogeneousFAF Form of V, W;

      set rf = ( RQForm f), qw = ( VectQuot (W,( RKer f)));

      thus ( leftker f) c= ( leftker ( RQForm f))

      proof

        let x be object;

        assume x in ( leftker f);

        then

        consider v be Vector of V such that

         A1: x = v and

         A2: for w be Vector of W holds (f . (v,w)) = ( 0. K);

        now

          let A be Vector of qw;

          consider w be Vector of W such that

           A3: A = (w + ( RKer f)) by VECTSP10: 22;

          

          thus (rf . (v,A)) = (f . (v,w)) by A3, Def21

          .= ( 0. K) by A2;

        end;

        hence thesis by A1;

      end;

      let x be object;

      assume x in ( leftker rf);

      then

      consider v be Vector of V such that

       A4: x = v and

       A5: for A be Vector of qw holds (rf . (v,A)) = ( 0. K);

      now

        let w be Vector of W;

        reconsider A = (w + ( RKer f)) as Vector of qw by VECTSP10: 23;

        

        thus (f . (v,w)) = (rf . (v,A)) by Def21

        .= ( 0. K) by A5;

      end;

      hence thesis by A4;

    end;

    theorem :: BILINEAR:46

    

     Th46: for K be add-associative right_zeroed right_complementable Abelian associative well-unital distributive non empty doubleLoopStr holds for V,W be VectSp of K, f be bilinear-Form of V, W holds ( RKer f) = ( RKer ( LQForm f))

    proof

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

      let V,W be VectSp of K, f be bilinear-Form of V, W;

      the carrier of ( RKer f) = ( rightker f) by Def19

      .= ( rightker ( LQForm f)) by Th44

      .= the carrier of ( RKer ( LQForm f)) by Def19;

      hence thesis by VECTSP_4: 29;

    end;

    theorem :: BILINEAR:47

    

     Th47: for K be add-associative right_zeroed right_complementable Abelian associative well-unital distributive non empty doubleLoopStr holds for V,W be VectSp of K, f be bilinear-Form of V, W holds ( LKer f) = ( LKer ( RQForm f))

    proof

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

      let V,W be VectSp of K, f be bilinear-Form of V, W;

      the carrier of ( LKer f) = ( leftker f) by Def18

      .= ( leftker ( RQForm f)) by Th45

      .= the carrier of ( LKer ( RQForm f)) by Def18;

      hence thesis by VECTSP_4: 29;

    end;

    theorem :: BILINEAR:48

    

     Th48: for K be add-associative right_zeroed right_complementable Abelian associative well-unital distributive non empty doubleLoopStr holds for V,W be VectSp of K, f be bilinear-Form of V, W holds ( QForm f) = ( RQForm ( LQForm f)) & ( QForm f) = ( LQForm ( RQForm f))

    proof

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

      let V,W be VectSp of K, f be bilinear-Form of V, W;

      set L = ( LKer f), vq = ( VectQuot (V,L)), R = ( RKer f), wq = ( VectQuot (W,R)), RL = ( RKer ( LQForm f)), wqr = ( VectQuot (W,RL)), LR = ( LKer ( RQForm f)), vql = ( VectQuot (V,LR));

      

       A1: ( dom ( QForm f)) = [:the carrier of vq, the carrier of wq:] by FUNCT_2:def 1;

       A2:

      now

        let x be object;

        assume x in ( dom ( QForm f));

        then

        consider A be Vector of vq, B be Vector of wq such that

         A3: x = [A, B] by DOMAIN_1: 1;

        consider w be Vector of W such that

         A4: B = (w + R) by VECTSP10: 22;

        

         A5: R = RL by Th46;

        consider v be Vector of V such that

         A6: A = (v + L) by VECTSP10: 22;

        

        thus (( QForm f) . x) = (( QForm f) . (A,B)) by A3

        .= (f . (v,w)) by A6, A4, Def22

        .= (( LQForm f) . (A,w)) by A6, Def20

        .= (( RQForm ( LQForm f)) . (A,B)) by A4, A5, Def21

        .= (( RQForm ( LQForm f)) . x) by A3;

      end;

      ( dom ( RQForm ( LQForm f))) = [:the carrier of vq, the carrier of wqr:] & the carrier of wqr = the carrier of wq by Th46, FUNCT_2:def 1;

      hence ( QForm f) = ( RQForm ( LQForm f)) by A1, A2, FUNCT_1: 2;

       A7:

      now

        let x be object;

        assume x in ( dom ( QForm f));

        then

        consider A be Vector of vq, B be Vector of wq such that

         A8: x = [A, B] by DOMAIN_1: 1;

        consider w be Vector of W such that

         A9: B = (w + R) by VECTSP10: 22;

        

         A10: L = LR by Th47;

        consider v be Vector of V such that

         A11: A = (v + L) by VECTSP10: 22;

        

        thus (( QForm f) . x) = (( QForm f) . (A,B)) by A8

        .= (f . (v,w)) by A11, A9, Def22

        .= (( RQForm f) . (v,B)) by A9, Def21

        .= (( LQForm ( RQForm f)) . (A,B)) by A11, A10, Def20

        .= (( LQForm ( RQForm f)) . x) by A8;

      end;

      ( dom ( LQForm ( RQForm f))) = [:the carrier of vql, the carrier of wq:] & the carrier of vql = the carrier of vq by Th47, FUNCT_2:def 1;

      hence thesis by A1, A7, FUNCT_1: 2;

    end;

    theorem :: BILINEAR:49

    

     Th49: for K be add-associative right_zeroed right_complementable Abelian associative well-unital distributive non empty doubleLoopStr holds for V,W be VectSp of K, f be bilinear-Form of V, W holds ( leftker ( QForm f)) = ( leftker ( RQForm ( LQForm f))) & ( rightker ( QForm f)) = ( rightker ( RQForm ( LQForm f))) & ( leftker ( QForm f)) = ( leftker ( LQForm ( RQForm f))) & ( rightker ( QForm f)) = ( rightker ( LQForm ( RQForm f)))

    proof

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

      let V,W be VectSp of K, f be bilinear-Form of V, W;

      set vq = ( VectQuot (V,( LKer f))), wq = ( VectQuot (W,( RKer f))), wqr = ( VectQuot (W,( RKer ( LQForm f)))), vql = ( VectQuot (V,( LKer ( RQForm f))));

      set rlf = ( RQForm ( LQForm f)), qf = ( QForm f), lrf = ( LQForm ( RQForm f));

      thus ( leftker qf) c= ( leftker rlf)

      proof

        let x be object;

        assume x in ( leftker qf);

        then

        consider vv be Vector of vq such that

         A1: x = vv and

         A2: for ww be Vector of wq holds (qf . (vv,ww)) = ( 0. K);

        now

          let ww be Vector of wqr;

          reconsider w = ww as Vector of wq by Th46;

          

          thus (rlf . (vv,ww)) = (qf . (vv,w)) by Th48

          .= ( 0. K) by A2;

        end;

        hence thesis by A1;

      end;

      thus ( leftker rlf) c= ( leftker qf)

      proof

        let x be object;

        assume x in ( leftker rlf);

        then

        consider vv be Vector of vq such that

         A3: x = vv and

         A4: for ww be Vector of wqr holds (rlf . (vv,ww)) = ( 0. K);

        now

          let ww be Vector of wq;

          reconsider w = ww as Vector of wqr by Th46;

          

          thus (qf . (vv,ww)) = (rlf . (vv,w)) by Th48

          .= ( 0. K) by A4;

        end;

        hence thesis by A3;

      end;

      thus ( rightker qf) c= ( rightker rlf)

      proof

        let x be object;

        assume x in ( rightker qf);

        then

        consider ww be Vector of wq such that

         A5: x = ww and

         A6: for vv be Vector of vq holds (qf . (vv,ww)) = ( 0. K);

        reconsider w = ww as Vector of wqr by Th46;

        now

          let vv be Vector of vq;

          

          thus (rlf . (vv,w)) = (qf . (vv,ww)) by Th48

          .= ( 0. K) by A6;

        end;

        hence thesis by A5;

      end;

      thus ( rightker rlf) c= ( rightker qf)

      proof

        let x be object;

        assume x in ( rightker rlf);

        then

        consider ww be Vector of wqr such that

         A7: x = ww and

         A8: for vv be Vector of vq holds (rlf . (vv,ww)) = ( 0. K);

        reconsider w = ww as Vector of wq by Th46;

        now

          let vv be Vector of vq;

          

          thus (qf . (vv,w)) = (rlf . (vv,ww)) by Th48

          .= ( 0. K) by A8;

        end;

        hence thesis by A7;

      end;

      thus ( leftker qf) c= ( leftker lrf)

      proof

        let x be object;

        assume x in ( leftker qf);

        then

        consider vv be Vector of vq such that

         A9: x = vv and

         A10: for ww be Vector of wq holds (qf . (vv,ww)) = ( 0. K);

        reconsider v = vv as Vector of vql by Th47;

        now

          let ww be Vector of wq;

          

          thus (lrf . (v,ww)) = (qf . (vv,ww)) by Th48

          .= ( 0. K) by A10;

        end;

        hence thesis by A9;

      end;

      thus ( leftker lrf) c= ( leftker qf)

      proof

        let x be object;

        assume x in ( leftker lrf);

        then

        consider vv be Vector of vql such that

         A11: x = vv and

         A12: for ww be Vector of wq holds (lrf . (vv,ww)) = ( 0. K);

        reconsider v = vv as Vector of vq by Th47;

        now

          let ww be Vector of wq;

          

          thus (qf . (v,ww)) = (lrf . (vv,ww)) by Th48

          .= ( 0. K) by A12;

        end;

        hence thesis by A11;

      end;

      thus ( rightker qf) c= ( rightker lrf)

      proof

        let x be object;

        assume x in ( rightker qf);

        then

        consider ww be Vector of wq such that

         A13: x = ww and

         A14: for vv be Vector of vq holds (qf . (vv,ww)) = ( 0. K);

        now

          let vv be Vector of vql;

          reconsider v = vv as Vector of vq by Th47;

          

          thus (lrf . (vv,ww)) = (qf . (v,ww)) by Th48

          .= ( 0. K) by A14;

        end;

        hence thesis by A13;

      end;

      let x be object;

      assume x in ( rightker lrf);

      then

      consider ww be Vector of wq such that

       A15: x = ww and

       A16: for vv be Vector of vql holds (lrf . (vv,ww)) = ( 0. K);

      now

        let vv be Vector of vq;

        reconsider v = vv as Vector of vql by Th47;

        

        thus (qf . (vv,ww)) = (lrf . (v,ww)) by Th48

        .= ( 0. K) by A16;

      end;

      hence thesis by A15;

    end;

    theorem :: BILINEAR:50

    

     Th50: for K be add-associative right_zeroed right_complementable distributive non empty doubleLoopStr holds for V,W be non empty ModuleStr over K holds for f be Functional of V, g be Functional of W holds ( ker f) c= ( leftker ( FormFunctional (f,g)))

    proof

      let K be add-associative right_zeroed right_complementable distributive non empty doubleLoopStr, V,W be non empty ModuleStr over K, f be Functional of V, g be Functional of W;

      set fg = ( FormFunctional (f,g));

      

       A1: ( ker f) = { v where v be Vector of V : (f . v) = ( 0. K) } by VECTSP10:def 9;

      let x be object;

      assume x in ( ker f);

      then

      consider v be Vector of V such that

       A2: x = v and

       A3: (f . v) = ( 0. K) by A1;

      now

        let w be Vector of W;

        

        thus (fg . (v,w)) = ((f . v) * (g . w)) by Def10

        .= ( 0. K) by A3;

      end;

      hence thesis by A2;

    end;

    theorem :: BILINEAR:51

    

     Th51: for K be add-associative right_zeroed right_complementable associative commutative well-unital almost_left_invertible distributive non empty doubleLoopStr holds for V,W be non empty ModuleStr over K holds for f be Functional of V, g be Functional of W st g <> ( 0Functional W) holds ( leftker ( FormFunctional (f,g))) = ( ker f)

    proof

      let K be add-associative right_zeroed right_complementable associative commutative well-unital almost_left_invertible distributive non empty doubleLoopStr, V,W be non empty ModuleStr over K, f be Functional of V, g be Functional of W;

      set fg = ( FormFunctional (f,g));

      assume

       A1: g <> ( 0Functional W);

      

       A2: ( ker f) = { v where v be Vector of V : (f . v) = ( 0. K) } by VECTSP10:def 9;

      thus ( leftker fg) c= ( ker f)

      proof

        let x be object;

        assume x in ( leftker fg);

        then

        consider v be Vector of V such that

         A3: x = v and

         A4: for w be Vector of W holds (fg . (v,w)) = ( 0. K);

        assume not x in ( ker f);

        then

         A5: (f . v) <> ( 0. K) by A2, A3;

        now

          let w be Vector of W;

          ((f . v) * (g . w)) = (fg . (v,w)) by Def10

          .= ( 0. K) by A4;

          

          hence (g . w) = ( 0. K) by A5, VECTSP_1: 12

          .= (( 0Functional W) . w) by HAHNBAN1: 14;

        end;

        hence contradiction by A1, FUNCT_2: 63;

      end;

      thus thesis by Th50;

    end;

    theorem :: BILINEAR:52

    

     Th52: for K be add-associative right_zeroed right_complementable distributive non empty doubleLoopStr holds for V,W be non empty ModuleStr over K holds for f be Functional of V, g be Functional of W holds ( ker g) c= ( rightker ( FormFunctional (f,g)))

    proof

      let K be add-associative right_zeroed right_complementable distributive non empty doubleLoopStr, V,W be non empty ModuleStr over K, f be Functional of V, g be Functional of W;

      set fg = ( FormFunctional (f,g));

      

       A1: ( ker g) = { w where w be Vector of W : (g . w) = ( 0. K) } by VECTSP10:def 9;

      let x be object;

      assume x in ( ker g);

      then

      consider w be Vector of W such that

       A2: x = w and

       A3: (g . w) = ( 0. K) by A1;

      now

        let v be Vector of V;

        

        thus (fg . (v,w)) = ((f . v) * (g . w)) by Def10

        .= ( 0. K) by A3;

      end;

      hence thesis by A2;

    end;

    theorem :: BILINEAR:53

    

     Th53: for K be add-associative right_zeroed right_complementable associative commutative well-unital almost_left_invertible distributive non empty doubleLoopStr holds for V,W be non empty ModuleStr over K holds for f be Functional of V, g be Functional of W st f <> ( 0Functional V) holds ( rightker ( FormFunctional (f,g))) = ( ker g)

    proof

      let K be add-associative right_zeroed right_complementable associative commutative well-unital almost_left_invertible distributive non empty doubleLoopStr, V,W be non empty ModuleStr over K, f be Functional of V, g be Functional of W;

      set fg = ( FormFunctional (f,g));

      assume

       A1: f <> ( 0Functional V);

      

       A2: ( ker g) = { w where w be Vector of W : (g . w) = ( 0. K) } by VECTSP10:def 9;

      thus ( rightker fg) c= ( ker g)

      proof

        let x be object;

        assume x in ( rightker fg);

        then

        consider w be Vector of W such that

         A3: x = w and

         A4: for v be Vector of V holds (fg . (v,w)) = ( 0. K);

        assume not x in ( ker g);

        then

         A5: (g . w) <> ( 0. K) by A2, A3;

        now

          let v be Vector of V;

          ((f . v) * (g . w)) = (fg . (v,w)) by Def10

          .= ( 0. K) by A4;

          

          hence (f . v) = ( 0. K) by A5, VECTSP_1: 12

          .= (( 0Functional V) . v) by HAHNBAN1: 14;

        end;

        hence contradiction by A1, FUNCT_2: 63;

      end;

      thus thesis by Th52;

    end;

    theorem :: BILINEAR:54

    

     Th54: for K be add-associative right_zeroed right_complementable commutative Abelian associative well-unital distributive almost_left_invertible non empty doubleLoopStr holds for V be VectSp of K, W be non empty ModuleStr over K holds for f be linear-Functional of V, g be Functional of W st g <> ( 0Functional W) holds ( LKer ( FormFunctional (f,g))) = ( Ker f) & ( LQForm ( FormFunctional (f,g))) = ( FormFunctional (( CQFunctional f),g))

    proof

      let K be add-associative right_zeroed right_complementable commutative Abelian associative well-unital distributive almost_left_invertible non empty doubleLoopStr, V be VectSp of K, W be non empty ModuleStr over K, f be linear-Functional of V, g be Functional of W;

      set fg = ( FormFunctional (f,g)), cf = ( CQFunctional f), fcfg = ( FormFunctional (( CQFunctional f),g)), vql = ( VectQuot (V,( LKer fg))), vq = ( VectQuot (V,( Ker f)));

      assume g <> ( 0Functional W);

      then

       A1: ( leftker fg) = ( ker f) by Th51;

      the carrier of ( LKer fg) = ( leftker fg) by Def18;

      hence

       A2: ( LKer fg) = ( Ker f) by A1, VECTSP10:def 11;

       A3:

      now

        let x be object;

        assume x in ( dom fcfg);

        then

        consider A be Vector of vq, B be Vector of W such that

         A4: x = [A, B] by DOMAIN_1: 1;

        consider v be Vector of V such that

         A5: A = (v + ( Ker f)) by VECTSP10: 22;

        

        thus (fcfg . x) = (fcfg . (A,B)) by A4

        .= ((cf . A) * (g . B)) by Def10

        .= ((f . v) * (g . B)) by A5, VECTSP10: 35

        .= (fg . (v,B)) by Def10

        .= (( LQForm fg) . (A,B)) by A2, A5, Def20

        .= (( LQForm fg) . x) by A4;

      end;

      ( dom ( LQForm fg)) = [:the carrier of vql, the carrier of W:] & ( dom fcfg) = [:the carrier of vq, the carrier of W:] by FUNCT_2:def 1;

      hence thesis by A2, A3, FUNCT_1: 2;

    end;

    theorem :: BILINEAR:55

    

     Th55: for K be add-associative right_zeroed right_complementable commutative Abelian associative well-unital distributive almost_left_invertible non empty doubleLoopStr holds for V be non empty ModuleStr over K, W be VectSp of K holds for f be Functional of V, g be linear-Functional of W st f <> ( 0Functional V) holds ( RKer ( FormFunctional (f,g))) = ( Ker g) & ( RQForm ( FormFunctional (f,g))) = ( FormFunctional (f,( CQFunctional g)))

    proof

      let K be add-associative right_zeroed right_complementable commutative Abelian associative well-unital distributive almost_left_invertible non empty doubleLoopStr, V be non empty ModuleStr over K, W be VectSp of K, f be Functional of V, g be linear-Functional of W;

      set fg = ( FormFunctional (f,g)), cg = ( CQFunctional g), fcfg = ( FormFunctional (f,( CQFunctional g))), wqr = ( VectQuot (W,( RKer fg))), wq = ( VectQuot (W,( Ker g)));

      assume f <> ( 0Functional V);

      then

       A1: ( rightker fg) = ( ker g) by Th53;

      the carrier of ( RKer fg) = ( rightker fg) by Def19;

      hence

       A2: ( RKer fg) = ( Ker g) by A1, VECTSP10:def 11;

       A3:

      now

        let x be object;

        assume x in ( dom fcfg);

        then

        consider A be Vector of V, B be Vector of wq such that

         A4: x = [A, B] by DOMAIN_1: 1;

        consider w be Vector of W such that

         A5: B = (w + ( Ker g)) by VECTSP10: 22;

        

        thus (fcfg . x) = (fcfg . (A,B)) by A4

        .= ((f . A) * (cg . B)) by Def10

        .= ((f . A) * (g . w)) by A5, VECTSP10: 35

        .= (fg . (A,w)) by Def10

        .= (( RQForm fg) . (A,B)) by A2, A5, Def21

        .= (( RQForm fg) . x) by A4;

      end;

      ( dom ( RQForm fg)) = [:the carrier of V, the carrier of wqr:] & ( dom fcfg) = [:the carrier of V, the carrier of wq:] by FUNCT_2:def 1;

      hence thesis by A2, A3, FUNCT_1: 2;

    end;

    theorem :: BILINEAR:56

    for K be Field, V,W be non trivial VectSp of K holds for f be non constant linear-Functional of V, g be non constant linear-Functional of W holds ( QForm ( FormFunctional (f,g))) = ( FormFunctional (( CQFunctional f),( CQFunctional g)))

    proof

      let K be Field, V,W be non trivial VectSp of K, f be non constant linear-Functional of V, g be non constant linear-Functional of W;

      

       A1: ( CQFunctional f) <> ( 0Functional ( VectQuot (V,( Ker f))));

      

       A2: g <> ( 0Functional W);

      then

       A3: ( LQForm ( FormFunctional (f,g))) = ( FormFunctional (( CQFunctional f),g)) by Th54;

      

      thus ( QForm ( FormFunctional (f,g))) = ( RQForm ( LQForm ( FormFunctional (f,g)))) by Th48

      .= ( RQForm ( FormFunctional (( CQFunctional f),g))) by A2, A3, Th54

      .= ( FormFunctional (( CQFunctional f),( CQFunctional g))) by A1, Th55;

    end;

    definition

      let K be ZeroStr;

      let V,W be non empty ModuleStr over K;

      let f be Form of V, W;

      :: BILINEAR:def23

      attr f is degenerated-on-left means

      : Def23: ( leftker f) <> {( 0. V)};

      :: BILINEAR:def24

      attr f is degenerated-on-right means

      : Def24: ( rightker f) <> {( 0. W)};

    end

    registration

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

      let V be VectSp of K, W be right_zeroed non empty ModuleStr over K;

      let f be additiveSAF homogeneousSAF Form of V, W;

      cluster ( LQForm f) -> non degenerated-on-left;

      coherence

      proof

        set qf = ( LQForm f), L = ( LKer f), qV = ( VectQuot (V,L));

        thus ( leftker qf) c= {( 0. qV)}

        proof

          let x be object;

          assume x in ( leftker qf);

          then

          consider vv be Vector of qV such that

           A1: x = vv and

           A2: for w be Vector of W holds (qf . (vv,w)) = ( 0. K);

          consider v be Vector of V such that

           A3: vv = (v + L) by VECTSP10: 22;

          now

            let w be Vector of W;

            

            thus (f . (v,w)) = (qf . (vv,w)) by A3, Def20

            .= ( 0. K) by A2;

          end;

          then v in ( leftker f);

          then v in the carrier of L by Def18;

          then v in L;

          

          then (v + L) = the carrier of L by VECTSP_4: 49

          .= ( zeroCoset (V,L)) by VECTSP10:def 4

          .= ( 0. qV) by VECTSP10: 21;

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

        end;

        let x be object;

        assume x in {( 0. qV)};

        then

         A4: x = ( 0. qV) by TARSKI:def 1;

        for w be Vector of W holds (qf . (( 0. qV),w)) = ( 0. K) by Th30;

        hence thesis by A4;

      end;

    end

    registration

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

      let V be right_zeroed non empty ModuleStr over K, W be VectSp of K;

      let f be additiveFAF homogeneousFAF Form of V, W;

      cluster ( RQForm f) -> non degenerated-on-right;

      coherence

      proof

        set qf = ( RQForm f), R = ( RKer f), qW = ( VectQuot (W,R));

        thus ( rightker qf) c= {( 0. qW)}

        proof

          let x be object;

          assume x in ( rightker qf);

          then

          consider ww be Vector of qW such that

           A1: x = ww and

           A2: for v be Vector of V holds (qf . (v,ww)) = ( 0. K);

          consider w be Vector of W such that

           A3: ww = (w + R) by VECTSP10: 22;

          now

            let v be Vector of V;

            

            thus (f . (v,w)) = (qf . (v,ww)) by A3, Def21

            .= ( 0. K) by A2;

          end;

          then w in ( rightker f);

          then w in the carrier of R by Def19;

          then w in R;

          

          then (w + R) = the carrier of R by VECTSP_4: 49

          .= ( zeroCoset (W,R)) by VECTSP10:def 4

          .= ( 0. qW) by VECTSP10: 21;

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

        end;

        let x be object;

        assume x in {( 0. qW)};

        then

         A4: x = ( 0. qW) by TARSKI:def 1;

        for v be Vector of V holds (qf . (v,( 0. qW))) = ( 0. K) by Th29;

        hence thesis by A4;

      end;

    end

    registration

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

      let V,W be VectSp of K;

      let f be bilinear-Form of V, W;

      cluster ( QForm f) -> non degenerated-on-left non degenerated-on-right;

      coherence

      proof

        ( rightker ( RQForm f)) = {( 0. ( VectQuot (W,( RKer f))))} by Def24;

        then

         A1: ( rightker ( LQForm ( RQForm f))) = {( 0. ( VectQuot (W,( RKer f))))} by Th44;

        ( leftker ( LQForm f)) = {( 0. ( VectQuot (V,( LKer f))))} by Def23;

        then

         A2: ( leftker ( RQForm ( LQForm f))) = {( 0. ( VectQuot (V,( LKer f))))} by Th45;

        ( leftker ( RQForm ( LQForm f))) = ( leftker ( QForm f)) & ( rightker ( LQForm ( RQForm f))) = ( rightker ( QForm f)) by Th49;

        hence thesis by A2, A1;

      end;

    end

    registration

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

      let V,W be VectSp of K;

      let f be bilinear-Form of V, W;

      cluster ( RQForm ( LQForm f)) -> non degenerated-on-left non degenerated-on-right;

      coherence

      proof

        ( leftker ( LQForm f)) = {( 0. ( VectQuot (V,( LKer f))))} by Def23;

        then ( leftker ( RQForm ( LQForm f))) = {( 0. ( VectQuot (V,( LKer f))))} by Th45;

        hence thesis;

      end;

      cluster ( LQForm ( RQForm f)) -> non degenerated-on-left non degenerated-on-right;

      coherence

      proof

        ( rightker ( RQForm f)) = {( 0. ( VectQuot (W,( RKer f))))} by Def24;

        then ( rightker ( LQForm ( RQForm f))) = {( 0. ( VectQuot (W,( RKer f))))} by Th44;

        hence thesis;

      end;

    end

    registration

      let K be Field;

      let V,W be non trivial VectSp of K;

      let f be non constant bilinear-Form of V, W;

      cluster ( QForm f) -> non constant;

      coherence

      proof

        consider v be Vector of V, w be Vector of W such that

         A1: (f . (v,w)) <> ( 0. K) by Th40;

        reconsider B = (w + ( RKer f)) as Vector of ( VectQuot (W,( RKer f))) by VECTSP10: 23;

        reconsider A = (v + ( LKer f)) as Vector of ( VectQuot (V,( LKer f))) by VECTSP10: 23;

        (( QForm f) . (A,B)) = (f . (v,w)) by Def22;

        hence thesis by A1, Th40;

      end;

    end

    begin

    definition

      let K be 1-sorted;

      let V be ModuleStr over K;

      let f be Form of V, V;

      :: BILINEAR:def25

      attr f is symmetric means

      : Def25: for v,w be Vector of V holds (f . (v,w)) = (f . (w,v));

    end

    definition

      let K be ZeroStr;

      let V be ModuleStr over K;

      let f be Form of V, V;

      :: BILINEAR:def26

      attr f is alternating means

      : Def26: for v be Vector of V holds (f . (v,v)) = ( 0. K);

    end

    registration

      let K be non empty ZeroStr;

      let V be non empty ModuleStr over K;

      cluster ( NulForm (V,V)) -> symmetric;

      coherence

      proof

        let v,w be Vector of V;

        

        thus (( NulForm (V,V)) . (v,w)) = ( 0. K) by FUNCOP_1: 70

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

      end;

      cluster ( NulForm (V,V)) -> alternating;

      coherence by FUNCOP_1: 70;

    end

    registration

      let K be non empty ZeroStr;

      let V be non empty ModuleStr over K;

      cluster symmetric for Form of V, V;

      existence

      proof

        take ( NulForm (V,V));

        thus thesis;

      end;

      cluster alternating for Form of V, V;

      existence

      proof

        take ( NulForm (V,V));

        thus thesis;

      end;

    end

    registration

      let K be add-associative right_zeroed right_complementable right-distributive non empty doubleLoopStr;

      let V be non empty ModuleStr over K;

      cluster symmetric additiveFAF homogeneousFAF additiveSAF homogeneousSAF for Form of V, V;

      existence

      proof

        take ( NulForm (V,V));

        thus thesis;

      end;

      cluster alternating additiveFAF homogeneousFAF additiveSAF homogeneousSAF for Form of V, V;

      existence

      proof

        take ( NulForm (V,V));

        thus thesis;

      end;

    end

    registration

      let K be Field;

      let V be non trivial VectSp of K;

      cluster symmetric non trivial non constant additiveFAF homogeneousFAF additiveSAF homogeneousSAF for Form of V, V;

      existence

      proof

        set f = the non constant non trivial linear-Functional of V;

        take ff = ( FormFunctional (f,f));

        now

          let v,w be Vector of V;

          

          thus (ff . (v,w)) = ((f . v) * (f . w)) by Def10

          .= (ff . (w,v)) by Def10;

        end;

        hence thesis;

      end;

    end

    registration

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

      let V be non empty ModuleStr over K;

      cluster alternating additiveFAF additiveSAF for Form of V, V;

      existence

      proof

        take ( NulForm (V,V));

        thus thesis;

      end;

    end

    registration

      let K be non empty addLoopStr;

      let V be non empty ModuleStr over K;

      let f,g be symmetric Form of V, V;

      cluster (f + g) -> symmetric;

      coherence

      proof

        let v,w be Vector of V;

        

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

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

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

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

      end;

    end

    registration

      let K be non empty doubleLoopStr;

      let V be non empty ModuleStr over K;

      let f be symmetric Form of V, V;

      let a be Element of K;

      cluster (a * f) -> symmetric;

      coherence

      proof

        let v,w be Vector of V;

        

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

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

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

      end;

    end

    registration

      let K be non empty addLoopStr;

      let V be non empty ModuleStr over K;

      let f be symmetric Form of V, V;

      cluster ( - f) -> symmetric;

      coherence

      proof

        let v,w be Vector of V;

        

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

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

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

      end;

    end

    registration

      let K be non empty addLoopStr;

      let V be non empty ModuleStr over K;

      let f,g be symmetric Form of V, V;

      cluster (f - g) -> symmetric;

      coherence ;

    end

    registration

      let K be right_zeroed non empty addLoopStr;

      let V be non empty ModuleStr over K;

      let f,g be alternating Form of V, V;

      cluster (f + g) -> alternating;

      coherence

      proof

        let v be Vector of V;

        

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

        .= (( 0. K) + (g . (v,v))) by Def26

        .= (( 0. K) + ( 0. K)) by Def26

        .= ( 0. K) by RLVECT_1:def 4;

      end;

    end

    registration

      let K be add-associative right_zeroed right_complementable right-distributive non empty doubleLoopStr;

      let V be non empty ModuleStr over K;

      let f be alternating Form of V, V;

      let a be Scalar of K;

      cluster (a * f) -> alternating;

      coherence

      proof

        let v be Vector of V;

        

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

        .= (a * ( 0. K)) by Def26

        .= ( 0. K);

      end;

    end

    registration

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

      let V be non empty ModuleStr over K;

      let f be alternating Form of V, V;

      cluster ( - f) -> alternating;

      coherence

      proof

        let v be Vector of V;

        

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

        .= ( - ( 0. K)) by Def26

        .= ( 0. K) by RLVECT_1: 12;

      end;

    end

    registration

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

      let V be non empty ModuleStr over K;

      let f,g be alternating Form of V, V;

      cluster (f - g) -> alternating;

      coherence ;

    end

    theorem :: BILINEAR:57

    for K be add-associative right_zeroed right_complementable right-distributive non empty doubleLoopStr holds for V be non empty ModuleStr over K holds for f be symmetric bilinear-Form of V, V holds ( leftker f) = ( rightker f)

    proof

      let K be add-associative right_zeroed right_complementable right-distributive non empty doubleLoopStr, V be non empty ModuleStr over K, f be symmetric bilinear-Form of V, V;

      thus ( leftker f) c= ( rightker f)

      proof

        let x be object;

        assume x in ( leftker f);

        then

        consider v be Vector of V such that

         A1: v = x and

         A2: for w be Vector of V holds (f . (v,w)) = ( 0. K);

        now

          let w be Vector of V;

          

          thus (f . (w,v)) = (f . (v,w)) by Def25

          .= ( 0. K) by A2;

        end;

        hence thesis by A1;

      end;

      let x be object;

      assume x in ( rightker f);

      then

      consider w be Vector of V such that

       A3: w = x and

       A4: for v be Vector of V holds (f . (v,w)) = ( 0. K);

      now

        let v be Vector of V;

        

        thus (f . (w,v)) = (f . (v,w)) by Def25

        .= ( 0. K) by A4;

      end;

      hence thesis by A3;

    end;

    theorem :: BILINEAR:58

    

     Th58: for K be add-associative right_zeroed right_complementable non empty addLoopStr holds for V be non empty ModuleStr over K holds for f be alternating additiveSAF additiveFAF Form of V, V holds for v,w be Vector of V holds (f . (v,w)) = ( - (f . (w,v)))

    proof

      let K be add-associative right_zeroed right_complementable non empty addLoopStr, V be non empty ModuleStr over K, f be alternating additiveSAF additiveFAF Form of V, V, v,w be Vector of V;

      ( 0. K) = (f . ((v + w),(v + w))) by Def26

      .= (((f . (v,v)) + (f . (v,w))) + ((f . (w,v)) + (f . (w,w)))) by Th28

      .= ((( 0. K) + (f . (v,w))) + ((f . (w,v)) + (f . (w,w)))) by Def26

      .= ((( 0. K) + (f . (v,w))) + ((f . (w,v)) + ( 0. K))) by Def26

      .= ((( 0. K) + (f . (v,w))) + (f . (w,v))) by RLVECT_1:def 4

      .= ((f . (v,w)) + (f . (w,v))) by RLVECT_1: 4;

      hence thesis by RLVECT_1: 6;

    end;

    definition

      let K be Fanoian Field;

      let V be non empty ModuleStr over K;

      let f be additiveSAF additiveFAF Form of V, V;

      :: original: alternating

      redefine

      :: BILINEAR:def27

      attr f is alternating means for v,w be Vector of V holds (f . (v,w)) = ( - (f . (w,v)));

      compatibility

      proof

        thus f is alternating implies for v,w be Vector of V holds (f . (v,w)) = ( - (f . (w,v))) by Th58;

        assume

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

        let v be Vector of V;

        (f . (v,v)) = ( - (f . (v,v))) by A1;

        then ((f . (v,v)) + (f . (v,v))) = ( 0. K) by VECTSP_1: 16;

        hence thesis by VECTSP_1:def 18;

      end;

    end

    theorem :: BILINEAR:59

    for K be add-associative right_zeroed right_complementable right-distributive non empty doubleLoopStr holds for V be non empty ModuleStr over K holds for f be alternating bilinear-Form of V, V holds ( leftker f) = ( rightker f)

    proof

      let K be add-associative right_zeroed right_complementable right-distributive non empty doubleLoopStr, V be non empty ModuleStr over K, f be alternating bilinear-Form of V, V;

      thus ( leftker f) c= ( rightker f)

      proof

        let x be object;

        assume x in ( leftker f);

        then

        consider v be Vector of V such that

         A1: v = x and

         A2: for w be Vector of V holds (f . (v,w)) = ( 0. K);

        now

          let w be Vector of V;

          

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

          .= ( - ( 0. K)) by A2

          .= ( 0. K) by RLVECT_1: 12;

        end;

        hence thesis by A1;

      end;

      let x be object;

      assume x in ( rightker f);

      then

      consider w be Vector of V such that

       A3: w = x and

       A4: for v be Vector of V holds (f . (v,w)) = ( 0. K);

      now

        let v be Vector of V;

        

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

        .= ( - ( 0. K)) by A4

        .= ( 0. K) by RLVECT_1: 12;

      end;

      hence thesis by A3;

    end;