:: Bilinear Functionals in Vector Spaces
::  by Jaros{\l}aw Kotowicz
::
:: Received November 5, 2002
:: Copyright (c) 2002 Association of Mizar Users

environ

 vocabularies RLVECT_1, VECTSP_1, ARYTM_1, HAHNBAN, FUNCT_1, SUBSET_1,
      FUNCOP_1, GRCAT_1, UNIALG_1, BINOP_1, LATTICES, RELAT_1, HAHNBAN1,
      FUNCT_5, RLSUB_1, ALGSTR_2, REALSET1, BOOLE, SEQM_3, GROUP_6, VECTSP10,
      BILINEAR, RELAT_2, SPPOL_1, VECTSP_2, ALGSTR_0, GROUP_1;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, DOMAIN_1, FUNCT_1, RELAT_1,
      REALSET1, STRUCT_0, ALGSTR_0, RLVECT_1, BINOP_1, GROUP_1, VECTSP_1,
      RELSET_1, FUNCT_2, FUNCOP_1, FUNCT_5, VECTSP_4, HAHNBAN1, VECTSP10;
 constructors BORSUK_1, VECTSP10, FUNCOP_1;
 registrations XBOOLE_0, SUBSET_1, RELSET_1, STRUCT_0, VECTSP_1, VECTSP_4,
      HAHNBAN1, VECTSP10, FUNCT_2;
 requirements SUBSET, BOOLE;
 definitions HAHNBAN1, TARSKI, XBOOLE_0, VECTSP_4, BINOP_1;
 theorems FUNCT_5, XBOOLE_1, FUNCT_2, HAHNBAN1, VECTSP_1, PRE_TOPC, FUNCOP_1,
      RLVECT_1, ANPROJ_1, VECTSP_4, TARSKI, FUNCT_1, REALSET1, ZFMISC_1,
      DOMAIN_1, VECTSP10, MOD_1, GROUP_1, BINOP_1, STRUCT_0;
 schemes BINOP_1;

begin

:: Two Form on Vector Spaces and Operations on Them.

definition
  let K be 1-sorted;
  let V,W be VectSpStr 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 VectSpStr over K;
  canceled;
  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 VectSpStr over K;
  let f,g be Form of V,W;
  func f+g -> Form of V,W means
  :Def3:
  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 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 by BINOP_1:2;
  end;
end;

definition
  let K be non empty multMagma;
  let V,W be non empty VectSpStr over K;
  let f be Form of V,W;
  let a be Element of K;
  func a*f -> Form of V,W means
  :Def4:
  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 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 by BINOP_1:2;
  end;
end;

definition
  let K be non empty addLoopStr;
  let V,W be non empty VectSpStr over K;
  let f be Form of V,W;
  func -f -> Form of V,W means
  :Def5:
  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 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 by BINOP_1:2;
  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 VectSpStr over K;
  let f be Form of V,W;
  redefine func -f -> Form of V,W equals

  (- 1.K) *f;
  coherence;
  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,Def5
          .= (-1.K )* f.(v,w) by MOD_1:14
          .=((- 1.K) *f).(v,w) by Def4;
      end;
      hence thesis by BINOP_1:2;
    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,Def4
        .=- f.(v,w) by MOD_1:14
        .= (-f).(v,w) by Def5;
    end;
    hence thesis by BINOP_1:2;
  end;
end;

definition
  let K be non empty addLoopStr;
  let V,W be non empty VectSpStr over K;
  let f,g be Form of V,W;
  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 VectSpStr over K;
  let f,g be Form of V,W;
  redefine func f - g -> Form of V,W means
  :Def8:
  for v be Vector of V, w be Vector of W holds it.(v,w) = f.(v,w) - g.(v,w);
  coherence;
  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,Def3
        .= f.(v,w) + -g.(v,w) by Def5
        .= f.(v,w) -g.(v,w) by RLVECT_1:def 12;
    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 12
        .= f.(v,w) + (-g).(v,w) by Def5
        .= (f-g).(v,w) by Def3;
    end;
    hence thesis by BINOP_1:2;
  end;
end;

Lm1: now
  let K be Abelian (non empty addLoopStr), V,W be non empty VectSpStr over K,
  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 Def3
      .= (g+f).(v,w) by Def3;
  end;
  hence f+g=g+f by BINOP_1:2;
end;

definition
  let K be Abelian (non empty addLoopStr);
  let V,W be non empty VectSpStr over K;
  let f,g be Form of V,W;
  redefine func f+g;
  commutativity by Lm1;
end;

canceled;

theorem
  for K be right_zeroed (non empty addLoopStr)
  for V,W be non empty VectSpStr over K
  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 VectSpStr 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 Def3
      .= f.(v,w) + 0.K by FUNCOP_1:85
      .= f.(v,w) by RLVECT_1:def 7;
  end;
  hence thesis by BINOP_1:2;
end;

theorem
  for K be add-associative (non empty addLoopStr)
  for V,W be non empty VectSpStr over K
  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 VectSpStr 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 Def3
      .= f.(v,w) + g.(v,w)+ h.(v,w) by Def3
      .= f.(v,w) + (g.(v,w)+ h.(v,w)) by RLVECT_1:def 6
      .= f.(v,w) + (g+h).(v,w) by Def3
      .= (f+ (g+h)).(v,w) by Def3;
  end;
  hence thesis by BINOP_1:2;
end;

theorem
  for K be add-associative right_zeroed right_complementable (non empty
  addLoopStr ) for V,W be non empty VectSpStr over K
  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 VectSpStr 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 Def8
      .= 0.K by RLVECT_1:28
      .= (NulForm(V,W)).(v,w) by FUNCOP_1:85;
  end;
  hence thesis by BINOP_1:2;
end;

theorem
  for K be right-distributive (non empty doubleLoopStr)
  for V,W be non empty VectSpStr over K, a be Element of K
  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 VectSpStr 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 Def4
      .= r*(f.(v,w) + g.(v,w)) by Def3
      .= r*f.(v,w) + r*g.(v,w) by VECTSP_1:def 11
      .= (r*f).(v,w) + r*g.(v,w) by Def4
      .= (r*f).(v,w) + (r*g).(v,w) by Def4
      .= (r*f + r*g).(v,w) by Def3;
  end;
  hence thesis by BINOP_1:2;
end;

theorem
  for K be left-distributive (non empty doubleLoopStr)
  for V,W be non empty VectSpStr over K for a,b be Element of K
  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 VectSpStr 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 Def4
      .= r*f.(v,w) + s*f.(v,w) by VECTSP_1:def 12
      .= (r*f).(v,w) + s*f.(v,w) by Def4
      .= (r*f).(v,w) + (s*f).(v,w) by Def4
      .= (r*f + s*f).(v,w) by Def3;
  end;
  hence thesis by BINOP_1:2;
end;

theorem
  for K be associative (non empty doubleLoopStr)
  for V,W be non empty VectSpStr over K for a,b be Element of K
  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 VectSpStr 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 Def4
      .= r*(s*f.(v,w)) by GROUP_1:def 4
      .= r*(s*f).(v,w) by Def4
      .= (r*(s*f)).(v,w) by Def4;
  end;
  hence thesis by BINOP_1:2;
end;

theorem
  for K be left_unital (non empty doubleLoopStr)
  for V,W be non empty VectSpStr over K 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 VectSpStr 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 Def4
      .= f.(v,w) by VECTSP_1:def 19;
  end;
  hence thesis by BINOP_1:2;
end;

Lm2: now
  let K be non empty 1-sorted, V,W be non empty VectSpStr over K,
  f be Form of V,W, v be Element of (the carrier of V), y be Element of W;
A1: dom f = [:the carrier of V,the carrier of W:] by FUNCT_2:def 1;
  then consider g be Function such that
A2: (curry f).v = g & dom g = the carrier of W & rng g c= rng f and
  for y be set st y in the carrier of W holds g.y = f.(v,y) by FUNCT_5:36;
  reconsider g as Function of the carrier of W,the carrier of K
  by A2,FUNCT_2:4,XBOOLE_1:1;
  g = (curry f).v by A2;
  hence (curry f).v is Functional of W;
  consider h be Function such that
A3: (curry' f).y = h & dom h = the carrier of V & rng h c= rng f and
  for x be set st x in the carrier of V holds h.x = f.(x,y) by A1,FUNCT_5:39;
  reconsider h as Function of the carrier of V,the carrier of K
  by A3,FUNCT_2:4,XBOOLE_1:1;
  h =(curry' f).y by A3;
  hence (curry' f).y is Functional of V;
end;

begin

:: Functional generated by Two Form when the One of Arguments is Fixed.

definition
  let K be non empty 1-sorted;
  let V,W be non empty VectSpStr over K;
  let f be Form of V,W, v be Vector of V;
  func FunctionalFAF(f,v) -> Functional of W equals

  (curry f).v;
  correctness by Lm2;
end;

definition
  let K be non empty 1-sorted;
  let V,W be non empty VectSpStr over K;
  let f be Form of V,W, w be Vector of W;
  func FunctionalSAF(f,w) -> Functional of V equals

  (curry' f).w;
  correctness by Lm2;
end;

theorem Th9:
  for K be non empty 1-sorted for V,W be non empty VectSpStr over K
  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 VectSpStr 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:] &
  rng f c= the carrier of K by FUNCT_2:def 1;
  then consider g be Function such that
A1: (curry f).v = g & dom g = the carrier of W & rng g c= rng f and
A2: for y be set st y in the carrier of W holds g.y = f.(v,y) by FUNCT_5:36;
  thus dom F = the carrier of W & rng F c= the carrier of K by A1;
  let y be Vector of W;
  thus F.y = f.(v,y) by A1,A2;
end;

theorem Th10:
  for K be non empty 1-sorted for V,W be non empty VectSpStr over K
  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 VectSpStr 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:] &
  rng f c= the carrier of K by FUNCT_2:def 1;
  then consider g be Function such that
A1: (curry' f).w = g & dom g = the carrier of V & rng g c= rng f and
A2: for y be set st y in the carrier of V holds g.y = f.(y,w) by FUNCT_5:39;
  thus dom F = the carrier of V & rng F c= the carrier of K by A1;
  let v be Vector of V;
  thus F.v = f.(v,w) by A1,A2;
end;

theorem Th11:
  for K be non empty ZeroStr, V,W be non empty VectSpStr 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 VectSpStr 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 Th9
      .= 0.K by FUNCOP_1:85
      .= (0Functional(W)).y by HAHNBAN1:22;
  end;
  hence thesis by FUNCT_2:113;
end;

theorem Th12:
  for K be non empty ZeroStr, V,W be non empty VectSpStr 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 VectSpStr 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 Th10
      .= 0.K by FUNCOP_1:85
      .= (0Functional(V)).v by HAHNBAN1:22;
  end;
  hence thesis by FUNCT_2:113;
end;

theorem Th13:
  for K be non empty addLoopStr for V,W be non empty VectSpStr over K
  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 VectSpStr 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 Th10
      .= f.(v,w) + g.(v,w) by Def3
      .= (FunctionalSAF(f,w)).v + g.(v,w) by Th10
      .= (FunctionalSAF(f,w)).v + (FunctionalSAF(g,w)).v by Th10
      .= (FunctionalSAF(f,w) +FunctionalSAF(g,w)).v by HAHNBAN1:def 6;
  end;
  hence thesis by FUNCT_2:113;
end;

theorem Th14:
  for K be non empty addLoopStr for V,W be non empty VectSpStr over K
  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 VectSpStr 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 Th9
      .= f.(w,v) + g.(w,v) by Def3
      .= (FunctionalFAF(f,w)).v + g.(w,v) by Th9
      .= (FunctionalFAF(f,w)).v + (FunctionalFAF(g,w)).v by Th9
      .= (FunctionalFAF(f,w) + FunctionalFAF(g,w)).v by HAHNBAN1:def 6;
  end;
  hence thesis by FUNCT_2:113;
end;

theorem Th15:
  for K be non empty doubleLoopStr for V,W be non empty VectSpStr over K
  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 VectSpStr 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 Th10
      .= a*f.(v,w) by Def4
      .= a*(FunctionalSAF(f,w)).v by Th10
      .= (a*(FunctionalSAF(f,w))).v by HAHNBAN1:def 9;
  end;
  hence thesis by FUNCT_2:113;
end;

theorem Th16:
  for K be non empty doubleLoopStr for V,W be non empty VectSpStr over K
  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 VectSpStr 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 Th9
      .= a*f.(w,v) by Def4
      .= a*(FunctionalFAF(f,w)).v by Th9
      .= (a* FunctionalFAF(f,w)).v by HAHNBAN1:def 9;
  end;
  hence thesis by FUNCT_2:113;
end;

theorem Th17:
  for K be non empty addLoopStr for V,W be non empty VectSpStr over K
  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 VectSpStr 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 Th10
      .= -f.(v,w) by Def5
      .= -(FunctionalSAF(f,w)).v by Th10
      .= (- FunctionalSAF(f,w)).v by HAHNBAN1:def 7;
  end;
  hence thesis by FUNCT_2:113;
end;

theorem Th18:
  for K be non empty addLoopStr for V,W be non empty VectSpStr over K
  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 VectSpStr 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 Th9
      .= -f.(w,v) by Def5
      .= -(FunctionalFAF(f,w)).v by Th9
      .= (- FunctionalFAF(f,w)).v by HAHNBAN1:def 7;
  end;
  hence thesis by FUNCT_2:113;
end;

theorem
  for K be non empty addLoopStr for V,W be non empty VectSpStr over K
  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 VectSpStr 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 Th10
      .= f.(v,w) - g.(v,w) by Def8
      .= (FunctionalSAF(f,w)).v - g.(v,w) by Th10
      .= (FunctionalSAF(f,w)).v - (FunctionalSAF(g,w)).v by Th10
      .= (FunctionalSAF(f,w)).v +- (FunctionalSAF(g,w)).v by RLVECT_1:def 12
      .= (FunctionalSAF(f,w)).v + (-FunctionalSAF(g,w)).v by HAHNBAN1:def 7
      .= (FunctionalSAF(f,w) -FunctionalSAF(g,w)).v by HAHNBAN1:def 6;
  end;
  hence thesis by FUNCT_2:113;
end;

theorem
  for K be non empty addLoopStr for V,W be non empty VectSpStr over K
  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 VectSpStr 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 Th9
      .= f.(w,v) - g.(w,v) by Def8
      .= (FunctionalFAF(f,w)).v - g.(w,v) by Th9
      .= (FunctionalFAF(f,w)).v - (FunctionalFAF(g,w)).v by Th9
      .= (FunctionalFAF(f,w)).v +- (FunctionalFAF(g,w)).v by RLVECT_1:def 12
      .= (FunctionalFAF(f,w)).v + (-FunctionalFAF(g,w)).v by HAHNBAN1:def 7
      .= (FunctionalFAF(f,w) -FunctionalFAF(g,w)).v by HAHNBAN1:def 6;
  end;
  hence thesis by FUNCT_2:113;
end;

begin

:: Two Form generated by Functionals.

definition
  let K be non empty multMagma;
  let V,W be non empty VectSpStr over K;
  let f be Functional of V;
  let g be Functional of W;
  func FormFunctional(f,g) -> Form of V,W means
  :Def11:
  for v be Vector of V, w be Vector of W holds it.(v,w)= f.v * g.w;
  existence
  proof
    set c1 = the carrier of V, c2 = the carrier of W, k = the carrier of K;
    deffunc F(Vector of V, Vector of W) = (f.$1) * (g.$2);
    consider i be Function of [:c1,c2:],k such that
A1: for x be Element of c1 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 by BINOP_1:2;
  end;
end;

theorem Th21:
  for K be add-associative right_zeroed right_complementable
  right-distributive (non empty doubleLoopStr)
  for V,W be non empty VectSpStr over K
  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 VectSpStr 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);
A1: [#]W = the carrier of W by PRE_TOPC:12;
  thus F.(v,y) = f.v * 0F.y by Def11
    .= f.v * 0.K by A1,FUNCOP_1:13
    .= 0.K by VECTSP_1:36;
end;

theorem Th22:
  for K be add-associative right_zeroed right_complementable
  left-distributive (non empty doubleLoopStr)
  for V,W be non empty VectSpStr over K
  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 VectSpStr 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);
A1: [#]V = the carrier of V by PRE_TOPC:12;
  thus F.(v,y) = 0F.v * h.y by Def11
    .= 0.K * h.y by A1,FUNCOP_1:13
    .= 0.K by VECTSP_1:39;
end;

theorem
  for K be add-associative right_zeroed right_complementable
  right-distributive (non empty doubleLoopStr)
  for V,W be non empty VectSpStr over K

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 VectSpStr 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 Th21
      .= NulForm(V,W).(v,y) by FUNCOP_1:85;
  end;
  hence thesis by BINOP_1:2;
end;

theorem
  for K be add-associative right_zeroed right_complementable
  left-distributive (non empty doubleLoopStr)
  for V,W be non empty VectSpStr over K

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 VectSpStr 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 Th22
      .= NulForm(V,W).(v,y) by FUNCOP_1:85;
  end;
  hence thesis by BINOP_1:2;
end;

theorem Th25:
  for K be non empty multMagma for V,W be non empty VectSpStr over K
  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 VectSpStr 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 Th9
      .= f.v * h.y by Def11
      .= (f.v * h).y by HAHNBAN1:def 9;
  end;
  hence thesis by FUNCT_2:113;
end;

theorem Th26:
  for K be commutative (non empty multMagma)
  for V,W be non empty VectSpStr over K
  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 VectSpStr 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 Th10
      .= f.v * h.y by Def11
      .= (h.y * f).v by HAHNBAN1:def 9;
  end;
  hence thesis by FUNCT_2:113;
end;

begin

::Bilinear Forms and Their Properties

definition
  let K be non empty addLoopStr;
  let V,W be non empty VectSpStr over K;
  let f be Form of V,W;
  attr f is additiveFAF means
  :Def12:
  for v be Vector of V holds FunctionalFAF(f,v) is additive;
  attr f is additiveSAF means
  :Def13:
  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 VectSpStr over K;
  let f be Form of V,W;
  attr f is homogeneousFAF means
  :Def14:
  for v be Vector of V holds FunctionalFAF(f,v) is homogeneous;
  attr f is homogeneousSAF means
  :Def15:
  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 VectSpStr over K;
  cluster NulForm(V,W) -> additiveFAF;
  coherence
  proof
    let v be Vector of V;
    FunctionalFAF(NulForm(V,W),v)= 0Functional(W) by Th11;
    hence thesis;
  end;
  cluster NulForm(V,W) -> additiveSAF;
  coherence
  proof
    let y be Vector of W;
    FunctionalSAF(NulForm(V,W),y)= 0Functional(V) by Th12;
    hence thesis;
  end;
end;

registration
  let K be right_zeroed (non empty addLoopStr);
  let V,W be non empty VectSpStr over K;
  cluster additiveFAF additiveSAF 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 VectSpStr over K;
  cluster NulForm(V,W) -> homogeneousFAF;
  coherence
  proof
    let v be Vector of V;
    FunctionalFAF(NulForm(V,W),v)= 0Functional(W) by Th11;
    hence thesis;
  end;
  cluster NulForm(V,W) -> homogeneousSAF;
  coherence
  proof
    let y be Vector of W;
    FunctionalSAF(NulForm(V,W),y)= 0Functional(V) by Th12;
    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 VectSpStr over K;
  cluster additiveFAF homogeneousFAF additiveSAF homogeneousSAF 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 VectSpStr 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 VectSpStr over K;
  let f be additiveFAF Form of V,W, v be Vector of V;
  cluster FunctionalFAF(f,v) -> 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 VectSpStr over K;
  let f be additiveSAF Form of V,W, w be Vector of W;
  cluster FunctionalSAF(f,w) -> additive;
  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 VectSpStr over K;
  let f be homogeneousFAF Form of V,W, v be Vector of V;
  cluster FunctionalFAF(f,v) -> 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 VectSpStr over K;
  let f be homogeneousSAF Form of V,W, w be Vector of W;
  cluster FunctionalSAF(f,w) -> homogeneous;
  coherence by Def15;
end;

registration
  let K be add-associative right_zeroed right_complementable
  right-distributive (non empty doubleLoopStr);
  let V,W be non empty VectSpStr 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);
A1: F= f.v * g by Th25;
    let y,y' be Vector of W;
    thus F.(y+y') = f.v * g.(y+y') by A1,HAHNBAN1:def 9
      .= f.v *(g.y +g.y') by HAHNBAN1:def 11
      .= f.v * g.y + f.v * g.y' by VECTSP_1:def 11
      .=f.v * g.y + F.y' by A1,HAHNBAN1:def 9
      .=F.y + F.y' by A1,HAHNBAN1:def 9;
  end;
end;

registration
  let K be add-associative right_zeroed right_complementable
  commutative right-distributive (non empty doubleLoopStr);
  let V,W be non empty VectSpStr 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 Th26;
    hence F is additive;
  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 VectSpStr 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);
A1: F= f.v * g by Th25;
    let y be Vector of W,r be Scalar of W;
    thus F.(r* y) = f.v * g.(r*y) by A1,HAHNBAN1:def 9
      .= f.v *(r*g.y) by HAHNBAN1:def 12
      .= r*(f.v * g.y) by GROUP_1:def 4
      .= r *F.y by A1,HAHNBAN1:def 9;
  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 VectSpStr over K;
  let f be homogeneous Functional of V, g be Functional of W;
  cluster FormFunctional(f,g) -> homogeneousSAF;
  coherence
  proof
    set fg= FormFunctional(f,g);
    let y be Vector of W;
    set F = FunctionalSAF(fg,y);
A1: F= g.y * f by Th26;
    let v be Vector of V,r be Scalar of V;
    thus F.(r* v) = g.y * f.(r*v) by A1,HAHNBAN1:def 9
      .= g.y *(r*f.v) by HAHNBAN1:def 12
      .= r*(g.y * f.v) by GROUP_1:def 4
      .= r *F.v by A1,HAHNBAN1:def 9;
  end;
end;

registration
  let K be non degenerated (non empty doubleLoopStr);
  let V be non trivial (non empty VectSpStr over K),
  W be non empty VectSpStr over K;
  let f be Functional of V, g be Functional of W;
  cluster FormFunctional(f,g) -> non trivial;
  coherence
  proof
    consider v be Vector of V such that
A1: v <> 0.V by ANPROJ_1:def 8;
    consider w be Vector of W;
    set fg = FormFunctional(f,g);
    assume
A2: fg is trivial;
    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:8;
A4: [0.V,0.W] <> [v,w] by A1,ZFMISC_1:33;
    per cases by A2,REALSET1:def 4;
    suppose fg = {};
      hence contradiction;
    end;
    suppose ex x be set st fg = {x};
      then consider x be set 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 A4,ZFMISC_1:33;
    end;
  end;
end;

registration
  let K be non degenerated (non empty doubleLoopStr);
  let V be non empty VectSpStr over K,
  W be non trivial (non empty VectSpStr over K);
  let f be Functional of V, g be Functional of W;
  cluster FormFunctional(f,g) -> non trivial;
  coherence
  proof
    consider v be Vector of V;
    consider w be Vector of W such that
A1: w <> 0.W by ANPROJ_1:def 8;
    set fg = FormFunctional(f,g);
    assume
A2: fg is trivial;
    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:8;
A4: [0.V,0.W] <> [v,w] by A1,ZFMISC_1:33;
    per cases by A2,REALSET1:def 4;
    suppose fg = {};
      hence contradiction;
    end;
    suppose ex x be set st fg = {x};
      then consider x be set 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 A4,ZFMISC_1:33;
    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
    consider v be Vector of V such that
A1: v <> 0.V & f.v <> 0.K by VECTSP10:29;
    consider w be Vector of W such that
A2: w <> 0.W & g.w <> 0.K by VECTSP10:29;
    set fg = FormFunctional(f,g);
A3: fg.(0.V,0.W) = f.(0.V)*g.(0.W) by Def11
      .= 0.K * g.(0.W) by HAHNBAN1:def 13
      .= 0.K by VECTSP_1:39;
A4: dom fg = [:the carrier of V, the carrier of W:] by FUNCT_2:def 1;
    fg.(v,w) = f.v * g.w by Def11;
    then fg.(v,w) <> 0.K by A1,A2,VECTSP_1:44;
    hence thesis by A3,A4,BINOP_1:31;
  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 Form of V,W;
  existence
  proof
    consider f be non constant non trivial linear-Functional of V,
    g be 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 VectSpStr 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);
A1: Ff is additive & Fg is additive by Def13;
    let v,y be Vector of V;
    thus Ffg.(v+y) = (Ff+Fg).(v+y) by Th13
      .= Ff.(v+y) + Fg.(v+y) by HAHNBAN1:def 6
      .= Ff.v+Ff.y + Fg.(v+y) by A1,HAHNBAN1:def 11
      .= Ff.v+Ff.y + (Fg.v+Fg.y) by A1,HAHNBAN1:def 11
      .= Ff.v+Ff.y + Fg.v + Fg.y by RLVECT_1:def 6
      .= Ff.v+Fg.v + Ff.y+Fg.y by RLVECT_1:def 6
      .= (Ff+Fg).v + Ff.y+Fg.y by HAHNBAN1:def 6
      .= (Ff+Fg).v + (Ff.y+Fg.y) by RLVECT_1:def 6
      .= (Ff+Fg).v + (Ff+Fg).y by HAHNBAN1:def 6
      .= Ffg.v + (Ff+Fg).y by Th13
      .= Ffg.v + Ffg.y by Th13;
  end;
end;

registration
  let K be Abelian add-associative right_zeroed (non empty addLoopStr);
  let V,W be non empty VectSpStr 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);
A1: Ff is additive & Fg is additive by Def12;
    let v,y be Vector of W;
    thus Ffg.(v+y) = (Ff+Fg).(v+y) by Th14
      .= Ff.(v+y) + Fg.(v+y) by HAHNBAN1:def 6
      .= Ff.v+Ff.y + Fg.(v+y) by A1,HAHNBAN1:def 11
      .= Ff.v+Ff.y + (Fg.v+Fg.y) by A1,HAHNBAN1:def 11
      .= Ff.v+Ff.y + Fg.v +Fg.y by RLVECT_1:def 6
      .= Ff.v+Fg.v + Ff.y+Fg.y by RLVECT_1:def 6
      .= (Ff+Fg).v + Ff.y+Fg.y by HAHNBAN1:def 6
      .= (Ff+Fg).v + (Ff.y+Fg.y) by RLVECT_1:def 6
      .= (Ff+Fg).v + (Ff+Fg).y by HAHNBAN1:def 6
      .= Ffg.v + (Ff+Fg).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 VectSpStr 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);
A1: Ff is additive by Def13;
    let v,y be Vector of V;
    thus Ffg.(v+y) = (a*Ff).(v+y) by Th15
      .= a*Ff.(v+y) by HAHNBAN1:def 9
      .= a*(Ff.v + Ff.y) by A1,HAHNBAN1:def 11
      .= a* Ff.v + a*Ff.y by VECTSP_1:def 11
      .= (a*Ff).v +a* Ff.y by HAHNBAN1:def 9
      .= (a*Ff).v + (a*Ff).y by HAHNBAN1:def 9
      .= Ffg.v + (a*Ff).y by Th15
      .= Ffg.v + Ffg.y by Th15;
  end;
end;

registration
  let K be right-distributive right_zeroed (non empty doubleLoopStr);
  let V,W be non empty VectSpStr 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);
A1: Ff is additive by Def12;
    let v,y be Vector of W;
    thus Ffg.(v+y) = (a*Ff).(v+y) by Th16
      .= a*Ff.(v+y) by HAHNBAN1:def 9
      .= a*(Ff.v + Ff.y) by A1,HAHNBAN1:def 11
      .= a* Ff.v +a* Ff.y by VECTSP_1:def 11
      .= (a*Ff).v +a* Ff.y by HAHNBAN1:def 9
      .= (a*Ff).v + (a*Ff).y by HAHNBAN1:def 9
      .= Ffg.v + (a*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 VectSpStr 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);
A1: Ff is additive by Def13;
    let v,y be Vector of V;
    thus Ffg.(v+y) = (-Ff).(v+y) by Th17
      .= -Ff.(v+y) by HAHNBAN1:def 7
      .= -(Ff.v + Ff.y) by A1,HAHNBAN1:def 11
      .= (- Ff.v) - Ff.y by RLVECT_1:44
      .= (-Ff).v - Ff.y by HAHNBAN1:def 7
      .= (-Ff).v + - Ff.y by RLVECT_1:def 12
      .= (-Ff).v + (-Ff).y by HAHNBAN1:def 7
      .= 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 VectSpStr 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);
A1: Ff is additive by Def12;
    let v,y be Vector of W;
    thus Ffg.(v+y) = (-Ff).(v+y) by Th18
      .= -Ff.(v+y) by HAHNBAN1:def 7
      .= -(Ff.v + Ff.y) by A1,HAHNBAN1:def 11
      .= (- Ff.v) - Ff.y by RLVECT_1:44
      .= (-Ff).v - Ff.y by HAHNBAN1:def 7
      .= (-Ff).v + - Ff.y by RLVECT_1:def 12
      .= (-Ff).v + (-Ff).y by HAHNBAN1:def 7
      .= Ffg.v + (-Ff).y by Th18
      .= Ffg.v + Ffg.y by Th18;
  end;
end;

registration
  let K be Abelian add-associative right_zeroed right_complementable
  (non empty addLoopStr);
  let V,W be non empty VectSpStr 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 VectSpStr 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 VectSpStr 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 Th13
      .= Ff.(a*v) + Fg.(a*v) by HAHNBAN1:def 6
      .= a*Ff.v + Fg.(a*v) by HAHNBAN1:def 12
      .= a*Ff.v + a*Fg.v by HAHNBAN1:def 12
      .= a*(Ff.v + Fg.v) by VECTSP_1:def 11
      .= a*(Ff + Fg).v by HAHNBAN1:def 6
      .= a* Ffg.v by Th13;
  end;
end;

registration
  let K be add-associative right_zeroed right_complementable
  right-distributive (non empty doubleLoopStr);
  let V,W be non empty VectSpStr 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 Th14
      .= Ff.(a*v) + Fg.(a*v) by HAHNBAN1:def 6
      .= a*Ff.v + Fg.(a*v) by HAHNBAN1:def 12
      .= a*Ff.v + a*Fg.v by HAHNBAN1:def 12
      .= a*(Ff.v + Fg.v) by VECTSP_1:def 11
      .= a*(Ff + Fg).v by HAHNBAN1:def 6
      .= a* 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 VectSpStr 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 Th15
      .= a*Ff.(b*v) by HAHNBAN1:def 9
      .= a*(b*Ff.v) by HAHNBAN1:def 12
      .= b*(a*Ff.v) by GROUP_1:def 4
      .= b*(a*Ff).v by HAHNBAN1:def 9
      .= b* Ffg.v by Th15;
  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 VectSpStr 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 Th16
      .= a*Ff.(b*v) by HAHNBAN1:def 9
      .= a*(b*Ff.v) by HAHNBAN1:def 12
      .= b*(a*Ff.v) by GROUP_1:def 4
      .= b*(a*Ff).v by HAHNBAN1:def 9
      .= b* 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 VectSpStr 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 Th17
      .= -Ff.(a*v) by HAHNBAN1:def 7
      .= -(a*Ff.v) by HAHNBAN1:def 12
      .= a*(-Ff.v) by VECTSP_1:40
      .= a*(-Ff).v by HAHNBAN1:def 7
      .= 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 VectSpStr 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 Th18
      .= -Ff.(a*v) by HAHNBAN1:def 7
      .= -(a*Ff.v) by HAHNBAN1:def 12
      .= a*(-Ff.v) by VECTSP_1:40
      .= a*(-Ff).v by HAHNBAN1:def 7
      .= a*Ffg.v by Th18;
  end;
end;

registration
  let K be add-associative right_zeroed right_complementable
  right-distributive (non empty doubleLoopStr);
  let V,W be non empty VectSpStr 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 VectSpStr over K;
  let f,g be homogeneousFAF Form of V,W;
  cluster f-g -> homogeneousFAF;
  correctness;
end;

theorem Th27:
  for K be non empty addLoopStr for V,W be non empty VectSpStr over K
  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 VectSpStr 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 by Def13;
  thus f.(v+w,y) = F.(v+w) by Th10
    .= F.v+F.w by A1,HAHNBAN1:def 11
    .= f.(v,y) + F.w by Th10
    .= f.(v,y) + f.(w,y) by Th10;
end;

theorem Th28:
  for K be non empty addLoopStr for V,W be non empty VectSpStr over K
  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 VectSpStr 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 by Def12;
  thus f.(v,y+z) = F.(y+z) by Th9
    .= F.y+F.z by A1,HAHNBAN1:def 11
    .= f.(v,y) + F.z by Th9
    .= f.(v,y) + f.(v,z) by Th9;
end;

theorem Th29:
  for K be right_zeroed (non empty addLoopStr)
  for V,W be non empty VectSpStr over K
  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 VectSpStr 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 Th27
    .= (v1 + v3) + f.(w,y+z) by Th28
    .= v1 +v3 + (v4 + v5) by Th28;
end;

theorem Th30:
  for K be add-associative right_zeroed right_complementable
  (non empty doubleLoopStr)
  for V,W be right_zeroed (non empty VectSpStr over K)
  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 VectSpStr 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 7
    .= f.(v,0.W) + f.(v,0.W) by Th28;
  hence thesis by RLVECT_1:22;
end;

theorem Th31:
  for K be add-associative right_zeroed right_complementable
  (non empty doubleLoopStr)
  for V,W be right_zeroed (non empty VectSpStr over K)
  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 VectSpStr 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 7
    .= f.(0.V,v) + f.(0.V,v) by Th27;
  hence thesis by RLVECT_1:22;
end;

theorem Th32:
  for K be non empty multMagma for V,W be non empty VectSpStr over K
  for v be Vector of V, w be Vector of W, a be Element of K
  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 VectSpStr 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 by Def15;
  thus f.(r*v,y) = F.(r*v) by Th10
    .= r*F.v by A1,HAHNBAN1:def 12
    .= r*f.(v,y) by Th10;
end;

theorem Th33:
  for K be non empty multMagma for V,W be non empty VectSpStr over K
  for v be Vector of V, w be Vector of W, a be Element of K
  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 VectSpStr 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 by Def14;
  thus f.(v,r*y) = F.(r*y) by Th9
    .= r*F.y by A1,HAHNBAN1:def 12
    .= r*f.(v,y) by Th9;
end;

theorem Th34:
  for K be add-associative right_zeroed right_complementable
  associative left_unital distributive (non empty doubleLoopStr)
  for V,W be add-associative right_zeroed right_complementable VectSp-like
  (non empty VectSpStr over K)
  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 VectSp-like
  (non empty VectSpStr 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:2
    .= 0.F *f.(0.V,v) by Th32
    .= 0.F by VECTSP_1:39;
end;

theorem Th35:
  for K be add-associative right_zeroed right_complementable
  associative left_unital distributive (non empty doubleLoopStr)
  for V,W be add-associative right_zeroed right_complementable
  VectSp-like (non empty VectSpStr over K)
  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
  VectSp-like (non empty VectSpStr 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:2
    .= 0.F * f.(v,0.W) by Th33
    .= 0.F by VECTSP_1:39;
end;

theorem Th36:
  for K be add-associative right_zeroed right_complementable Abelian
  associative well-unital distributive (non empty doubleLoopStr)
  for V,W be VectSp of K 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 12
    .= f.(v,y) +f.(-w,y) by Th27
    .= f.(v,y) +f.((-1.K)* w,y) by VECTSP_1:59
    .= f.(v,y) +(-1.K)*f.(w,y) by Th32
    .= f.(v,y) + -(1.K * f.(w,y)) by VECTSP_1:41
    .= f.(v,y) -(1.K * f.(w,y)) by RLVECT_1:def 12
    .= f.(v,y) - f.( w,y)by VECTSP_1:def 19;
end;

theorem Th37:
  for K be add-associative right_zeroed right_complementable
  Abelian associative well-unital distributive (non empty doubleLoopStr)
  for V,W be VectSp of K 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 12
    .= f.(v,y) + f.(v,-z) by Th28
    .= f.(v,y) + f.(v,(-1.K)* z) by VECTSP_1:59
    .= f.(v,y) + (-1.K)*f.(v,z) by Th33
    .= f.(v,y) + -(1.K * f.(v,z)) by VECTSP_1:41
    .= f.(v,y) -(1.K * f.(v,z)) by RLVECT_1:def 12
    .= f.(v,y) - f.(v,z)by VECTSP_1:def 19;
end;

theorem Th38:
  for K be add-associative right_zeroed right_complementable
  Abelian associative well-unital distributive (non empty doubleLoopStr)
  for V,W be VectSp of K
  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 Th36
    .= v1 - v3 - f.(w,y-z) by Th37
    .= v1 - v3 - (v4 - v5) by Th37;
end;

theorem
  for K be add-associative right_zeroed right_complementable
  associative well-unital distributive (non empty doubleLoopStr)
  for V,W be add-associative right_zeroed right_complementable VectSp-like
  (non empty VectSpStr over K)
  for v,u be Vector of V, w,t be Vector of W, a,b be Element of K
  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 VectSp-like
  (non empty VectSpStr 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 Th29
    .= v1 +b*v3 + (f.(a*w,y) +f.(a*w,b*z)) by Th33
    .= v1 + b*v3 + (a*v4 + f.(a*w,b*z)) by Th32
    .= v1 + b*v3 + (a*v4 + a*f.(w,b*z)) by Th32
    .= v1 + b*v3 + (a*v4 + a*(b*v5)) by Th33;
end;

theorem
  for K be add-associative right_zeroed right_complementable
  Abelian associative well-unital distributive (non empty doubleLoopStr)
  for V,W be VectSp of K
  for v,u be Vector of V, w,t be Vector of W, a,b be Element of K
  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 Th38
    .= v1 -b*v3 - (f.(a*w,y) -f.(a*w,b*z)) by Th33
    .= v1 - b*v3 - (a*v4 - f.(a*w,b*z)) by Th32
    .= v1 - b*v3 - (a*v4 - a*f.(w,b*z)) by Th32
    .= v1 - b*v3 - (a*v4 - a*(b*v5)) by Th33;
end;

theorem Th41:
  for K be add-associative right_zeroed right_complementable
  (non empty doubleLoopStr), V,W be right_zeroed (non empty VectSpStr 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 VectSpStr over K),
  f be Form of V,W;
  assume that
A1: f is additiveFAF or f is additiveSAF;
A2: dom f = [: the carrier of V, the carrier of W:] by FUNCT_2:def 1;
  hereby
    assume
A3: f is constant;
    let v be Vector of V, w be Vector of W;
    per cases by A1;
    suppose
A4:   f is additiveFAF;
      thus f.(v,w) = f.(v,0.W) by A2,A3,BINOP_1:31
        .= 0.K by A4,Th30;
    end;
    suppose
A5:   f is additiveSAF;
      thus f.(v,w) = f.(0.V,w) by A2,A3,BINOP_1:31
        .= 0.K by A5,Th31;
    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 set 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:9;
      consider s be Vector of V, t be Vector of W such that
A10:  y = [s,t] by A8,DOMAIN_1:9;
      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 16;
  end;
end;

begin

:: Left and Right Kernel of Form. "Diagonal" Kernel of Form

definition
  let K be ZeroStr;
  let V,W be non empty VectSpStr over K;
  let f be Form of V,W;
  func leftker f -> Subset of V equals
  {v where v is Vector of V : for w be Vector of W holds f.(v,w) = 0.K};
  correctness
  proof

set A={v where v is 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 set;
      assume x in A;
      then consider v be Vector of V such that
A1:   v=x & for w be Vector of W holds f.(v,w)=0.K;
      thus thesis by A1;
    end;
    hence thesis;
  end;
end;

definition
  let K be ZeroStr;
  let V,W be non empty VectSpStr over K;
  let f be Form of V,W;
  func rightker f -> Subset of W equals
  {w where w is Vector of W : for v be Vector of V holds f.(v,w) = 0.K};
  correctness
  proof

set A={w where w is 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 set;
      assume x in A;
      then consider w be Vector of W such that
A1:   w=x & for v be Vector of V holds f.(v,w) = 0.K;
      thus thesis by A1;
    end;
    hence thesis;
  end;
end;

definition
  let K be ZeroStr;
  let V be non empty VectSpStr over K;
  let f be Form of V,V;
  func diagker f -> Subset of V equals
  {v where v is Vector of V : f.(v,v) = 0.K};
  correctness
  proof
    set A = {v where v is Vector of V : f.(v,v) = 0.K};
    A c= the carrier of V
    proof
      let x be set;
      assume x in A;
      then consider v be Vector of V such that
A1:   v=x & f.(v,v)=0.K;
      thus thesis by A1;
    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 VectSpStr over K);
  let W be non empty VectSpStr 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 Th10
        .= 0.K by HAHNBAN1:def 13;
    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
  VectSp-like (non empty VectSpStr over K);
  let W be non empty VectSpStr 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 Th10
        .= 0.K by HAHNBAN1:def 13;
    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 VectSpStr over K;
  let W be right_zeroed (non empty VectSpStr 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 Th9
        .= 0.K by HAHNBAN1:def 13;
    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 VectSpStr over K;
  let W be add-associative right_zeroed right_complementable
  VectSp-like (non empty VectSpStr 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 Th9
        .= 0.K by HAHNBAN1:def 13;
    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 VectSpStr over K);
  let f be additiveFAF Form of V,V;
  cluster diagker f -> non empty;
  coherence
  proof
    f.(0.V,0.V) = 0.K &
    diagker f = {v where v is Vector of V : f.(v,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
  (non empty doubleLoopStr);
  let V be right_zeroed (non empty VectSpStr over K);
  let f be additiveSAF Form of V,V;
  cluster diagker f -> non empty;
  coherence
  proof
    f.(0.V,0.V) = 0.K &
    diagker f = {v where v is Vector of V: f.(v,v) = 0.K} by Th31;
    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
  VectSp-like (non empty VectSpStr over K);
  let f be homogeneousFAF Form of V,V;
  cluster diagker f -> non empty;
  coherence
  proof
    f.(0.V,0.V) = 0.K &
    diagker f = {v where v is Vector of V : f.(v,v) = 0.K} by Th35;
    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
  VectSp-like (non empty VectSpStr over K);
  let f be homogeneousSAF Form of V,V;
  cluster diagker f -> non empty;
  coherence
  proof
    f.(0.V,0.V) = 0.K &
    diagker f = {v where v is Vector of V : f.(v,v) = 0.K} by Th34;
    then 0.V in diagker f;
    hence thesis;
  end;
end;

theorem
  for K be ZeroStr, V be non empty VectSpStr over K 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 VectSpStr over K, f be Form of V,V;
  thus leftker f c= diagker f
  proof
    let x be set;
    assume x in leftker f;
    then consider v be Vector of V such that
A1: v=x & for w be Vector of V holds f.(v,w)=0.K;
    f.(v,v) = 0.K by A1;
    hence x in diagker f by A1;
  end;
  let x be set;
  assume x in rightker f;
  then consider v be Vector of V such that
A2: v=x & for w be Vector of V holds f.(w,v)=0.K;
  f.(v,v) = 0.K by A2;
  hence x in diagker f by A2;
end;

theorem Th43:
  for K be add-associative right_zeroed right_complementable
  right-distributive (non empty doubleLoopStr)
  for V,W be non empty VectSpStr over K
  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 VectSpStr 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
A1: v in V1 & u in V1;
    then consider v1 be Vector of V such that
A2: v1= v & for w be Vector of W holds f.(v1,w)=0.K;
    consider u1 be Vector of V such that
A3: u1= u & for w be Vector of W holds f.(u1,w)=0.K by A1;
    now
      let w be Vector of W;
      thus f.(v+u,w) = f.(v1,w) + f.(u1,w) by A2,A3,Th27
        .= 0.K + f.(u1,w) by A2
        .= 0.K + 0.K by A3
        .= 0.K by RLVECT_1:def 7;
    end;
    hence v+u in V1;
  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
A4: v1= v & 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 A4,Th32
      .= a*0.K by A4
      .= 0.K by VECTSP_1:36;
  end;
  hence a * v in V1;
end;

theorem Th44:
  for K be add-associative right_zeroed right_complementable
  right-distributive (non empty doubleLoopStr)
  for V,W be non empty VectSpStr over K
  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 VectSpStr 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
A1: v in V1 & u in V1;
    then consider v1 be Vector of W such that
A2: v1= v & for w be Vector of V holds f.(w,v1)=0.K;
    consider u1 be Vector of W such that
A3: u1= u & for w be Vector of V holds f.(w,u1)=0.K by A1;
    now
      let w be Vector of V;
      thus f.(w,v+u) = f.(w,v1) + f.(w,u1) by A2,A3,Th28
        .= 0.K + f.(w,u1) by A2
        .= 0.K + 0.K by A3
        .= 0.K by RLVECT_1:def 7;
    end;
    hence v+u in V1;
  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
A4: v1= v & 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 A4,Th33
      .= a*0.K by A4
      .= 0.K by VECTSP_1:36;
  end;
  hence a * v in V1;
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 VectSpStr over K;
  let f be additiveSAF homogeneousSAF Form of V,W;
  func LKer f -> strict non empty Subspace of V means
  :Def19:
  the carrier of it = leftker f;
  existence by VECTSP_4:42,Th43;
  uniqueness by VECTSP_4:37;
end;

definition
  let K be add-associative right_zeroed right_complementable
  Abelian associative well-unital distributive (non empty doubleLoopStr);
  let V be non empty VectSpStr over K, W be VectSp of K;
  let f be additiveFAF homogeneousFAF Form of V,W;
  func RKer f -> strict non empty Subspace of W means
  :Def20:
  the carrier of it = rightker f;
  existence by VECTSP_4:42,Th44;
  uniqueness by VECTSP_4:37;
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 VectSpStr over K;
  let f be additiveSAF homogeneousSAF Form of V,W;

func LQForm(f) -> additiveSAF homogeneousSAF Form of VectQuot(V,LKer f),W means
  :Def21:
  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);
A1: C = the carrier of vq by VECTSP10:def 6;
    defpred P[set,set,set] means
    for a be Vector of V st $1 = a+L holds $3 = f.(a,$2);
A2: now
      let A be Vector of vq, w0 be Vector of W;
      consider a be Vector of V such that
A3:   A = a+L by VECTSP10:23;
      take y = f.(a,w0);
      now
        let a1 be Vector of V;
        assume A = a1+L;
        then a in a1+L by A3,VECTSP_4:59;
        then consider w be Vector of V such that
A4:     w in L & a = a1 + w by VECTSP_4:57;
        w in the carrier of L by A4,STRUCT_0:def 5;
        then w in leftker f by Def19;
        then consider aa be Vector of V such that
A5:     aa=w & for ww be Vector of W holds f.(aa,ww) =0.K;
        thus y = f.(a1,w0)+f.(w,w0) by A4,Th27
          .= f.(a1,w0) +0.K by A5
          .= f.(a1,w0) by RLVECT_1:def 7;
      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(A2);
    reconsider ff as Form of vq,W;
    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
A7:     A = a+L by VECTSP10:23;
        consider b be Vector of V such that
A8:     B = b+L by VECTSP10:23;
A9:     the addF of vq = addCoset(V,L) by VECTSP10:def 6;
A10:    aC.(A,B) =a+b+L by A1,A7,A8,VECTSP10:def 3;
        thus ffw.(A+B) = ff.(A+B,w) by Th10
          .= f.(a+b,w) by A6,A9,A10,RLVECT_1:5
          .= f.(a,w) + f.(b,w) by Th27
          .= ff.(A,w) + f.(b,w) by A6,A7
          .= ff.(A,w) + ff.(B,w) by A6,A8
          .= ffw.A + ff.(B,w) by Th10
          .= ffw.A + ffw.B by Th10;
      end;
      hence ffw is additive by HAHNBAN1:def 11;
    end;
    then reconsider ff as additiveSAF Form of vq,W by Def13;
    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:23;
A12:    the lmult of vq = lmultCoset(V,L) by VECTSP10:def 6;
A13:    mC.(r,A) =r*a+L by A1,A11,VECTSP10:def 5;
        thus ffw.(r*A) = ff.(r*A,w) by Th10
          .= f.(r*a,w) by A6,A12,A13,VECTSP_1:def 24
          .= r*f.(a,w) by Th32
          .= r*ff.(A,w) by A6,A11
          .= r*ffw.A by Th10;
      end;
      hence ffw is homogeneous by HAHNBAN1:def 12;
    end;
    then reconsider ff as additiveSAF homogeneousSAF Form of vq,W by Def15;
    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
A14: 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
A15: 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
A16:  A = a + L by VECTSP10:23;
      thus f1.(A,w) = f.(a,w) by A14,A16
        .= f2.(A,w) by A15,A16;
    end;
    hence thesis by BINOP_1:2;
  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 VectSpStr over K, W be VectSp of K;
  let f be additiveFAF homogeneousFAF Form of V,W;

func RQForm(f) -> additiveFAF homogeneousFAF Form of V,VectQuot(W,RKer f) means
  :Def22:
  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);
A1: C = the carrier of vq by VECTSP10:def 6;
    defpred P[set,set,set] means
    for w be Vector of W st $2 = w+L holds $3 = f.($1,w);
A2: now
      let v0 be Vector of V, A be Vector of vq;
      consider a be Vector of W such that
A3:   A = a+L by VECTSP10:23;
      take y = f.(v0,a);
      now
        let a1 be Vector of W;
        assume A = a1+L;
        then a in a1+L by A3,VECTSP_4:59;
        then consider w be Vector of W such that
A4:     w in L & a = a1 + w by VECTSP_4:57;
        w in the carrier of L by A4,STRUCT_0:def 5;
        then w in rightker f by Def20;
        then consider aa be Vector of W such that
A5:     aa=w & for vv be Vector of V holds f.(vv,aa) =0.K;
        thus y = f.(v0,a1)+f.(v0,w) by A4,Th28
          .= f.(v0,a1) +0.K by A5
          .= f.(v0,a1) by RLVECT_1:def 7;
      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(A2);
    reconsider ff as Form of V,vq;
    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
A7:     A = a+L by VECTSP10:23;
        consider b be Vector of W such that
A8:     B = b+L by VECTSP10:23;
A9:     the addF of vq = addCoset(W,L) by VECTSP10:def 6;
A10:    aC.(A,B) =a+b+L by A1,A7,A8,VECTSP10:def 3;
        thus ffw.(A+B) = ff.(v,A+B) by Th9
          .= f.(v,a+b) by A6,A9,A10,RLVECT_1:5
          .= f.(v,a) + f.(v,b) by Th28
          .= ff.(v,A) + f.(v,b) by A6,A7
          .= ff.(v,A) + ff.(v,B) by A6,A8
          .= ffw.A + ff.(v,B) by Th9
          .= ffw.A + ffw.B by Th9;
      end;
      hence ffw is additive by HAHNBAN1:def 11;
    end;
    then reconsider ff as additiveFAF Form of V,vq by Def12;
    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:23;
A12:    the lmult of vq = lmultCoset(W,L) by VECTSP10:def 6;
A13:    mC.(r,A) =r*a+L by A1,A11,VECTSP10:def 5;
        thus ffw.(r*A) = ff.(v,r*A) by Th9
          .= f.(v,r*a) by A6,A12,A13,VECTSP_1:def 24
          .= r*f.(v,a) by Th33
          .= r*ff.(v,A) by A6,A11
          .= r*ffw.A by Th9;
      end;
      hence ffw is homogeneous by HAHNBAN1:def 12;
    end;
    then reconsider ff as additiveFAF homogeneousFAF Form of V,vq by Def14;
    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
A14: 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
A15: 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
A16:  A = a + L by VECTSP10:23;
      thus f1.(v,A) = f.(v,a) by A14,A16
        .= f2.(v,A) by A15,A16;
    end;
    hence thesis by BINOP_1:2;
  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:23;
      let w,t be Vector of W;
      thus flf.(w+t) = lf.(A,w+t) by Th9
        .= f.(v,w+t) by A1,Def21
        .= f.(v,w)+f.(v,t) by Th28
        .= lf.(A,w)+ f.(v,t) by A1,Def21
        .= lf.(A,w)+ lf.(A,t) by A1,Def21
        .= flf.w+ lf.(A,t) by Th9
        .= flf.w + flf.t by Th9;
    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:23;
    let w be Vector of W, r be Scalar of W;
    thus flf.(r*w) = lf.(A,r*w) by Th9
      .= f.(v,r*w) by A2,Def21
      .= r*f.(v,w) by Th33
      .= r*lf.(A,w) by A2,Def21
      .= r*flf.w by Th9;
  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:23;
      let v,t be Vector of V;
      thus flf.(v+t) = lf.(v+t,A) by Th10
        .= f.(v+t,w) by A3,Def22
        .= f.(v,w)+f.(t,w) by Th27
        .= lf.(v,A)+ f.(t,w) by A3,Def22
        .= lf.(v,A)+ lf.(t,A) by A3,Def22
        .= flf.v+ lf.(t,A) by Th10
        .= flf.v + flf.t by Th10;
    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:23;
    let v be Vector of V, r be Scalar of V;
    thus flf.(r*v) = lf.(r*v,A) by Th10
      .= f.(r*v,w) by A4,Def22
      .= r*f.(v,w) by Th32
      .= r*lf.(v,A) by A4,Def22
      .= r*flf.v by Th10;
  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;

func QForm(f) -> bilinear-Form of VectQuot(V,LKer(f)),VectQuot(W,RKer(f)) means
  :Def23:
  for A be Vector of VectQuot(V,LKer f), B be Vector of VectQuot(W, RKer(f))
  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);
A1: Cv = the carrier of vq by VECTSP10:def 6;
A2: Cw = the carrier of wq by VECTSP10:def 6;
    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);
A3: now
      let A be Vector of vq, B be Vector of wq;
      consider a be Vector of V such that
A4:   A = a+L by VECTSP10:23;
      consider b be Vector of W such that
A5:   B = b+R by VECTSP10:23;
      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 A4,VECTSP_4:59;
        then consider vv be Vector of V such that
A6:     vv in L & a = a1 + vv by VECTSP_4:57;
        assume B = b1+R;
        then b in b1+R by A5,VECTSP_4:59;
        then consider ww be Vector of W such that
A7:     ww in R & b = b1 + ww by VECTSP_4:57;
        vv in the carrier of L by A6,STRUCT_0:def 5;
        then vv in leftker f by Def19;
        then consider aa be Vector of V such that
A8:     aa=vv & for w0 be Vector of W holds f.(aa,w0) =0.K;
        ww in the carrier of R by A7,STRUCT_0:def 5;
        then ww in rightker f by Def20;
        then consider bb be Vector of W such that
A9:     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 A6,A7,Th29
          .=f.(a1,b1)+0.K + (f.(vv,b1)+f.(vv,ww)) by A9
          .= f.(a1,b1) +0.K + (0.K+f.(vv,ww)) by A8
          .= f.(a1,b1) + (0.K+f.(vv,ww)) by RLVECT_1:def 7
          .= f.(a1,b1) + f.(vv,ww) by RLVECT_1:10
          .= f.(a1,b1) + 0.K by A8
          .= f.(a1,b1) by RLVECT_1:def 7;
      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(A3);
    reconsider ff as Form of vq,wq;
A11: now
      let ww be Vector of wq;
      consider w be Vector of W such that
A12:  ww= w+R by VECTSP10:23;
      set ffw = FunctionalSAF(ff,ww);
      now
        let A,B be Vector of vq;
        consider a be Vector of V such that
A13:    A = a+L by VECTSP10:23;
        consider b be Vector of V such that
A14:    B = b+L by VECTSP10:23;
A15:    the addF of vq = aCv by VECTSP10:def 6;
A16:    aCv.(A,B) =a+b+L by A1,A13,A14,VECTSP10:def 3;
        thus ffw.(A+B) = ff.(A+B,ww) by Th10
          .= f.(a+b,w) by A10,A12,A15,A16,RLVECT_1:5
          .= f.(a,w) + f.(b,w) by Th27
          .= ff.(A,ww) + f.(b,w) by A10,A12,A13
          .= ff.(A,ww) + ff.(B,ww) by A10,A12,A14
          .= ffw.A + ff.(B,ww) by Th10
          .= ffw.A + ffw.B by Th10;
      end;
      hence ffw is additive by HAHNBAN1:def 11;
    end;
A17: now
      let vv be Vector of vq;
      consider v be Vector of V such that
A18:  vv= v+L by VECTSP10:23;
      set ffv = FunctionalFAF(ff,vv);
      now
        let A,B be Vector of wq;
        consider a be Vector of W such that
A19:    A = a+R by VECTSP10:23;
        consider b be Vector of W such that
A20:    B = b+R by VECTSP10:23;
A21:    the addF of wq = aCw by VECTSP10:def 6;
A22:    aCw.(A,B) =a+b+R by A2,A19,A20,VECTSP10:def 3;
        thus ffv.(A+B) = ff.(vv,A+B) by Th9
          .= f.(v,a+b) by A10,A18,A21,A22,RLVECT_1:5
          .= f.(v,a) + f.(v,b) by Th28
          .= ff.(vv,A) + f.(v,b) by A10,A18,A19
          .= ff.(vv,A) + ff.(vv,B) by A10,A18,A20
          .= ffv.A + ff.(vv,B) by Th9
          .= ffv.A + ffv.B by Th9;
      end;
      hence ffv is additive by HAHNBAN1:def 11;
    end;
A23: now
      let ww be Vector of wq;
      consider w be Vector of W such that
A24:  ww= w+R by VECTSP10:23;
      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
A25:    A = a+L by VECTSP10:23;
A26:    the lmult of vq = mCv by VECTSP10:def 6;
A27:    mCv.(r,A) =r*a+L by A1,A25,VECTSP10:def 5;
        thus ffw.(r*A) = ff.(r*A,ww) by Th10
          .= f.(r*a,w) by A10,A24,A26,A27,VECTSP_1:def 24
          .= r*f.(a,w) by Th32
          .= r*ff.(A,ww) by A10,A24,A25
          .= r*ffw.A by Th10;
      end;
      hence ffw is homogeneous by HAHNBAN1:def 12;
    end;
    now
      let vv be Vector of vq;
      consider v be Vector of V such that
A28:  vv= v+L by VECTSP10:23;
      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
A29:    A = a+R by VECTSP10:23;
A30:    the lmult of wq = mCw by VECTSP10:def 6;
A31:    mCw.(r,A) =r*a+R by A2,A29,VECTSP10:def 5;
        thus ffv.(r*A) = ff.(vv,r*A) by Th9
          .= f.(v,r*a) by A10,A28,A30,A31,VECTSP_1:def 24
          .= r*f.(v,a) by Th33
          .= r*ff.(vv,A) by A10,A28,A29
          .= r*ffv.A by Th9;
      end;
      hence ffv is homogeneous by HAHNBAN1:def 12;
    end;
    then reconsider ff as bilinear-Form of vq,wq by A11,A17,A23,Def12,Def13
    ,Def14,Def15;
    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
A32: for A be Vector of vq, B be Vector of wq
    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
A33: for A be Vector of vq, B be Vector of wq
    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
A34:  A = a + L by VECTSP10:23;
      consider b be Vector of W such that
A35:  B = b + R by VECTSP10:23;
      thus f1.(A,B) = f.(a,b) by A32,A34,A35
        .= f2.(A,B) by A33,A34,A35;
    end;
    hence thesis by BINOP_1:2;
  end;
end;

theorem Th45:
  for K be add-associative right_zeroed right_complementable
  Abelian associative well-unital distributive (non empty doubleLoopStr)
  for V be VectSp of K, W be non empty VectSpStr over K
  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 VectSpStr 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 set;
    assume x in rightker f;
    then consider w be Vector of W such that
A1: x=w & 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
A2:   A = v+LKer f by VECTSP10:23;
      thus lf.(A,w) = f.(v,w) by A2,Def21
        .= 0.K by A1;
    end;
    hence x in rightker(LQForm f) by A1;
  end;
  let x be set;
  assume x in rightker lf;
  then consider w be Vector of W such that
A3: x=w & 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:24;
    thus f.(v,w) = lf.(A,w) by Def21
      .= 0.K by A3;
  end;
  hence thesis by A3;
end;

theorem Th46:
  for K be add-associative right_zeroed right_complementable
  Abelian associative well-unital distributive (non empty doubleLoopStr)
  for V be non empty VectSpStr over K, W be VectSp of K
  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 VectSpStr 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 set;
    assume x in leftker f;
    then consider v be Vector of V such that
A1: x=v & 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
A2:   A = w+RKer f by VECTSP10:23;
      thus rf.(v,A) = f.(v,w) by A2,Def22
        .= 0.K by A1;
    end;
    hence x in leftker(RQForm f) by A1;
  end;
  let x be set;
  assume x in leftker rf;
  then consider v be Vector of V such that
A3: x=v & 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:24;
    thus f.(v,w) = rf.(v,A) by Def22
      .= 0.K by A3;
  end;
  hence thesis by A3;
end;

theorem Th47:
  for K be add-associative right_zeroed right_complementable
  Abelian associative well-unital distributive (non empty doubleLoopStr)
  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 Def20
    .= rightker (LQForm f) by Th45
    .= the carrier of (RKer (LQForm f)) by Def20;
  hence thesis by VECTSP_4:37;
end;

theorem Th48:
  for K be add-associative right_zeroed right_complementable
  Abelian associative well-unital distributive (non empty doubleLoopStr)
  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 Def19
    .= leftker (RQForm f) by Th46
    .= the carrier of (LKer (RQForm f)) by Def19;
  hence thesis by VECTSP_4:37;
end;

theorem Th49:
  for K be add-associative right_zeroed right_complementable
  Abelian associative well-unital distributive (non empty doubleLoopStr)
  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: dom RQForm (LQForm(f))=
  [:the carrier of vq, the carrier of wqr:] by FUNCT_2:def 1;
A3: dom LQForm (RQForm(f))=
  [:the carrier of vql, the carrier of wq:] by FUNCT_2:def 1;
A4: the carrier of wqr = the carrier of wq by Th47;
A5: the carrier of vql = the carrier of vq by Th48;
  now
    let x be set;
    assume x in dom QForm(f);
    then consider A be Vector of vq, B be Vector of wq such that
A6: x=[A,B] by DOMAIN_1:9;
    consider v be Vector of V such that
A7: A = v + L by VECTSP10:23;
    consider w be Vector of W such that
A8: B = w + R by VECTSP10:23;
A9: R = RL by Th47;
    thus (QForm(f)).x = (QForm(f)).(A,B) by A6
      .= f.(v,w) by A7,A8,Def23
      .= (LQForm(f)).(A,w) by A7,Def21
      .=(RQForm(LQForm(f))).(A,B) by A8,A9,Def22
      .=(RQForm(LQForm(f))).x by A6;
  end;
  hence QForm(f) = RQForm(LQForm(f)) by A1,A2,A4,FUNCT_1:9;
  now
    let x be set;
    assume x in dom QForm(f);
    then consider A be Vector of vq, B be Vector of wq such that
A10: x=[A,B] by DOMAIN_1:9;
    consider v be Vector of V such that
A11: A = v + L by VECTSP10:23;
    consider w be Vector of W such that
A12: B = w + R by VECTSP10:23;
A13: L = LR by Th48;
    thus (QForm(f)).x = (QForm(f)).(A,B) by A10
      .= f.(v,w) by A11,A12,Def23
      .= (RQForm(f)).(v,B) by A12,Def22
      .=(LQForm(RQForm(f))).(A,B) by A11,A13,Def21
      .=(LQForm(RQForm(f))).x by A10;
  end;
  hence thesis by A1,A3,A5,FUNCT_1:9;
end;

theorem Th50:
  for K be add-associative right_zeroed right_complementable
  Abelian associative well-unital distributive (non empty doubleLoopStr)
  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 set;
    assume x in leftker qf;
    then consider vv be Vector of vq such that
A1: x=vv & 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 Th47;
      thus rlf.(vv,ww) = qf.(vv,w) by Th49
        .= 0.K by A1;
    end;
    hence x in leftker rlf by A1;
  end;
  thus leftker rlf c= leftker qf
  proof
    let x be set;
    assume x in leftker rlf;
    then consider vv be Vector of vq such that
A2: x=vv & 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 Th47;
      thus qf.(vv,ww) = rlf.(vv,w) by Th49
        .= 0.K by A2;
    end;
    hence x in leftker qf by A2;
  end;
  thus rightker qf c= rightker rlf
  proof
    let x be set;
    assume x in rightker qf;
    then consider ww be Vector of wq such that
A3: x=ww & for vv be Vector of vq holds qf.(vv,ww)=0.K;
    reconsider w = ww as Vector of wqr by Th47;
    now
      let vv be Vector of vq;
      thus rlf.(vv,w) = qf.(vv,ww) by Th49
        .= 0.K by A3;
    end;
    hence x in rightker rlf by A3;
  end;
  thus rightker rlf c= rightker qf
  proof
    let x be set;
    assume x in rightker rlf;
    then consider ww be Vector of wqr such that
A4: x=ww & for vv be Vector of vq holds rlf.(vv,ww)=0.K;
    reconsider w = ww as Vector of wq by Th47;
    now
      let vv be Vector of vq;
      thus qf.(vv,w) = rlf.(vv,ww) by Th49
        .= 0.K by A4;
    end;
    hence x in rightker qf by A4;
  end;
  thus leftker qf c= leftker lrf
  proof
    let x be set;
    assume x in leftker qf;
    then consider vv be Vector of vq such that
A5: x=vv & for ww be Vector of wq holds qf.(vv,ww)=0.K;
    reconsider v=vv as Vector of vql by Th48;
    now
      let ww be Vector of wq;
      thus lrf.(v,ww) = qf.(vv,ww) by Th49
        .= 0.K by A5;
    end;
    hence x in leftker lrf by A5;
  end;
  thus leftker lrf c= leftker qf
  proof
    let x be set;
    assume x in leftker lrf;
    then consider vv be Vector of vql such that
A6: x=vv & for ww be Vector of wq holds lrf.(vv,ww)=0.K;
    reconsider v=vv as Vector of vq by Th48;
    now
      let ww be Vector of wq;
      thus qf.(v,ww) = lrf.(vv,ww) by Th49
        .= 0.K by A6;
    end;
    hence x in leftker qf by A6;
  end;
  thus rightker qf c= rightker lrf
  proof
    let x be set;
    assume x in rightker qf;
    then consider ww be Vector of wq such that
A7: x=ww & 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 Th48;
      thus lrf.(vv,ww) = qf.(v,ww) by Th49
        .= 0.K by A7;
    end;
    hence x in rightker lrf by A7;
  end;
  let x be set;
  assume x in rightker lrf;
  then consider ww be Vector of wq such that
A8: x=ww & 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 Th48;
    thus qf.(vv,ww) = lrf.(v,ww) by Th49
      .= 0.K by A8;
  end;
  hence x in rightker qf by A8;
end;

theorem Th51:
  for K be add-associative right_zeroed right_complementable
  distributive (non empty doubleLoopStr) for V,W be non empty VectSpStr over K
  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 VectSpStr over K,
  f be Functional of V, g be Functional of W;
  set fg = FormFunctional(f,g);
A1: ker f = {v where v is Vector of V : f.v = 0.K} by VECTSP10:def 9;
  let x be set;
  assume x in ker f;
  then consider v be Vector of V such that
A2: x=v & f.v=0.K by A1;
  now
    let w be Vector of W;
    thus fg.(v,w) = f.v*g.w by Def11
      .= 0.K by A2,VECTSP_1:39;
  end;
  hence thesis by A2;
end;

theorem Th52:
  for K be add-associative right_zeroed right_complementable associative
  commutative well-unital almost_left_invertible distributive
  (non empty doubleLoopStr) for V, W be non empty VectSpStr over K
  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 VectSpStr over K,
  f be Functional of V, g be Functional of W;
  set fg = FormFunctional(f,g);
A1: ker f = {v where v is Vector of V : f.v = 0.K} by VECTSP10:def 9;
  assume
A2: g <> 0Functional(W);
  thus leftker fg c= ker f
  proof
    let x be set;
    assume x in leftker fg;
    then consider v be Vector of V such that
A3: x=v & for w be Vector of W holds fg.(v,w) = 0.K;
    assume not x in ker f;
    then
A4: f.v <> 0.K by A1,A3;
    now
      let w be Vector of W;
      f.v*g.w = fg.(v,w) by Def11
        .= 0.K by A3;
      hence g.w = 0.K by A4,VECTSP_1:44
        .= (0Functional(W)).w by HAHNBAN1:22;
    end;
    hence contradiction by A2,FUNCT_2:113;
  end;
  thus thesis by Th51;
end;

theorem Th53:
  for K be add-associative right_zeroed right_complementable distributive
  (non empty doubleLoopStr) for V,W be non empty VectSpStr over K
  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 VectSpStr over K,
  f be Functional of V, g be Functional of W;
  set fg = FormFunctional(f,g);
A1: ker g = {w where w is Vector of W : g.w = 0.K} by VECTSP10:def 9;
  let x be set;
  assume x in ker g;
  then consider w be Vector of W such that
A2: x=w & g.w=0.K by A1;
  now
    let v be Vector of V;
    thus fg.(v,w) = f.v*g.w by Def11
      .= 0.K by A2,VECTSP_1:36;
  end;
  hence thesis by A2;
end;

theorem Th54:
  for K be add-associative right_zeroed right_complementable associative
  commutative well-unital almost_left_invertible distributive
  (non empty doubleLoopStr) for V, W be non empty VectSpStr over K
  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 VectSpStr over K,
  f be Functional of V, g be Functional of W;
  set fg = FormFunctional(f,g);
A1: ker g = {w where w is Vector of W : g.w = 0.K} by VECTSP10:def 9;
  assume
A2: f <> 0Functional(V);
  thus rightker fg c= ker g
  proof
    let x be set;
    assume x in rightker fg;
    then consider w be Vector of W such that
A3: x=w & for v be Vector of V holds fg.(v,w) = 0.K;
    assume not x in ker g;
    then
A4: g.w <> 0.K by A1,A3;
    now
      let v be Vector of V;
      f.v*g.w = fg.(v,w) by Def11
        .= 0.K by A3;
      hence f.v = 0.K by A4,VECTSP_1:44
        .= (0Functional(V)).v by HAHNBAN1:22;
    end;
    hence contradiction by A2,FUNCT_2:113;
  end;
  thus thesis by Th53;
end;

theorem Th55:

for K be add-associative right_zeroed right_complementable commutative Abelian
  associative well-unital distributive almost_left_invertible
  (non empty doubleLoopStr)
  for V be VectSp of K, W be non empty VectSpStr over K
  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 VectSpStr over K,
  f be linear-Functional of V, g be Functional of W;
  assume
A1: g <> 0Functional(W);
  set fg = FormFunctional(f,g), cf = CQFunctional(f),
  fcfg = FormFunctional(CQFunctional(f),g),
  vql = VectQuot(V, LKer fg), vq =VectQuot(V, Ker f);
A2: the carrier of LKer fg = leftker fg by Def19;
  leftker fg = ker f by A1,Th52;
  hence
A3: LKer fg = Ker f by A2,VECTSP10:def 11;
A4: dom LQForm(fg) = [: the carrier of vql, the carrier of W:]
  by FUNCT_2:def 1;
A5: dom fcfg = [: the carrier of vq, the carrier of W:] by FUNCT_2:def 1;
  now
    let x be set;
    assume x in dom fcfg;
    then consider A be Vector of vq, B be Vector of W such that
A6: x=[A,B] by DOMAIN_1:9;
    consider v be Vector of V such that
A7: A = v + Ker f by VECTSP10:23;
    thus fcfg.x = fcfg.(A,B) by A6
      .= cf.A * g.B by Def11
      .=f.v *g.B by A7,VECTSP10:36
      .= fg.(v,B) by Def11
      .= (LQForm(fg)).(A,B) by A3,A7,Def21
      .= (LQForm(fg)).x by A6;
  end;
  hence thesis by A3,A4,A5,FUNCT_1:9;
end;

theorem Th56:

for K be add-associative right_zeroed right_complementable commutative Abelian
  associative well-unital distributive almost_left_invertible
  (non empty doubleLoopStr)
  for V be non empty VectSpStr over K, W be VectSp of K
  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 VectSpStr over K, W be VectSp of K,
  f be Functional of V, g be linear-Functional of W;
  assume
A1: f <> 0Functional(V);
  set fg = FormFunctional(f,g), cg = CQFunctional(g),
  fcfg = FormFunctional(f,CQFunctional(g)),
  wqr = VectQuot(W, RKer fg), wq =VectQuot(W, Ker g);
A2: the carrier of RKer fg = rightker fg by Def20;
  rightker fg = ker g by A1,Th54;
  hence
A3: RKer fg = Ker g by A2,VECTSP10:def 11;
A4: dom RQForm(fg) = [: the carrier of V, the carrier of wqr:]
  by FUNCT_2:def 1;
A5: dom fcfg = [: the carrier of V, the carrier of wq:] by FUNCT_2:def 1;
  now
    let x be set;
    assume x in dom fcfg;
    then consider A be Vector of V, B be Vector of wq such that
A6: x=[A,B] by DOMAIN_1:9;
    consider w be Vector of W such that
A7: B = w + Ker g by VECTSP10:23;
    thus fcfg.x = fcfg.(A,B) by A6
      .= f.A * cg.B by Def11
      .=f.A *g.w by A7,VECTSP10:36
      .= fg.(A,w) by Def11
      .= (RQForm(fg)).(A,B) by A3,A7,Def22
      .= (RQForm(fg)).x by A6;
  end;
  hence thesis by A3,A4,A5,FUNCT_1:9;
end;

theorem
  for K be Field, V,W be non trivial VectSp of K
  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: g <> 0Functional(W);
A2: CQFunctional(f) <> 0Functional(VectQuot(V,Ker f));
A3: LQForm(FormFunctional(f,g)) = FormFunctional(CQFunctional(f),g)
  by A1,Th55;
  thus QForm(FormFunctional(f,g))
  = RQForm(LQForm(FormFunctional(f,g))) by Th49
    .= RQForm(FormFunctional(CQFunctional(f),g)) by A1,A3,Th55
    .= FormFunctional(CQFunctional(f),CQFunctional(g)) by A2,Th56;
end;

definition
  let K be ZeroStr;
  let V,W be non empty VectSpStr over K;
  let f be Form of V,W;
  attr f is degenerated-on-left means
  :Def24:
  leftker f <> {0.V};
  attr f is degenerated-on-right means
  :Def25:
  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 VectSpStr 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 set;
      assume x in leftker qf;
      then consider vv be Vector of qV such that
A1:   x= vv & for w be Vector of W holds qf.(vv,w)=0.K;
      consider v be Vector of V such that
A2:   vv = v + L by VECTSP10:23;
      now
        let w be Vector of W;
        thus f.(v,w) = qf.(vv,w) by A2,Def21
          .= 0.K by A1;
      end;
      then v in leftker f;
      then v in the carrier of L by Def19;
      then v in L by STRUCT_0:def 5;
      then v+L = the carrier of L by VECTSP_4:64
        .= zeroCoset(V,L) by VECTSP10:def 4
        .= 0.qV by VECTSP10:22;
      hence thesis by A1,A2,TARSKI:def 1;
    end;
    let x be set;
    assume x in {0.qV};
    then
A3: x = 0.qV by TARSKI:def 1;
    for w be Vector of W holds qf.(0.qV,w) = 0.K by Th31;
    hence thesis by A3;
  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 VectSpStr 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 set;
      assume x in rightker qf;
      then consider ww be Vector of qW such that
A1:   x= ww & for v be Vector of V holds qf.(v,ww)=0.K;
      consider w be Vector of W such that
A2:   ww = w + R by VECTSP10:23;
      now
        let v be Vector of V;
        thus f.(v,w) = qf.(v,ww) by A2,Def22
          .= 0.K by A1;
      end;
      then w in rightker f;
      then w in the carrier of R by Def20;
      then w in R by STRUCT_0:def 5;
      then w+R = the carrier of R by VECTSP_4:64
        .= zeroCoset(W,R) by VECTSP10:def 4
        .= 0.qW by VECTSP10:22;
      hence thesis by A1,A2,TARSKI:def 1;
    end;
    let x be set;
    assume x in {0.qW};
    then
A3: x = 0.qW by TARSKI:def 1;
    for v be Vector of V holds qf.(v,0.qW) = 0.K by Th30;
    hence thesis by A3;
  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
A1: leftker RQForm(LQForm(f)) = leftker QForm(f) &
    rightker LQForm(RQForm(f)) = rightker QForm(f) by Th50;
    leftker LQForm(f) = {0.(VectQuot(V,LKer f))} by Def24;
    then
A2: leftker RQForm(LQForm(f)) = {0.(VectQuot(V,LKer f))} by Th46;
    rightker RQForm(f) = {0.(VectQuot(W,RKer f))} by Def25;
    then rightker LQForm(RQForm(f)) = {0.(VectQuot(W,RKer f))} by Th45;
    hence thesis by A1,A2,Def24,Def25;
  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 Def24;
    then leftker RQForm(LQForm(f)) = {0.(VectQuot(V,LKer f))} by Th46;
    hence thesis by Def24;
  end;

cluster LQForm(RQForm(f)) -> non degenerated-on-left non degenerated-on-right;
  coherence
  proof
    rightker RQForm(f) = {0.(VectQuot(W,RKer f))} by Def25;
    then rightker LQForm(RQForm(f)) = {0.(VectQuot(W,RKer f))} by Th45;
    hence thesis by Def25;
  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 Th41;
    reconsider A = v +LKer f as Vector of VectQuot(V,LKer(f)) by VECTSP10:24;
    reconsider B = w + RKer f as Vector of VectQuot(W,RKer(f)) by VECTSP10:24;
    (QForm(f)).(A,B) = f.(v,w) by Def23;
    hence thesis by A1,Th41;
  end;
end;

begin

:: Bilinear Symmetric and Alternating Forms

definition
  let K be 1-sorted;
  let V be VectSpStr over K;
  let f be Form of V,V;
  attr f is symmetric means
  :Def26:
  for v,w be Vector of V holds f.(v,w) = f.(w,v);
end;

definition
  let K be ZeroStr;
  let V be VectSpStr over K;
  let f be Form of V,V;
  attr f is alternating means
  :Def27:
  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 VectSpStr 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:85
      .= NulForm(V,V).(w,v) by FUNCOP_1:85;
  end;
  cluster NulForm(V,V) -> alternating;
  coherence
  proof
    let v be Vector of V;
    thus NulForm(V,V).(v,v) = 0.K by FUNCOP_1:85;
  end;
end;

registration
  let K be non empty ZeroStr;
  let V be non empty VectSpStr over K;
  cluster symmetric Form of V,V;
  existence
  proof
    take NulForm(V,V); thus thesis;
  end;
  cluster alternating 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 VectSpStr over K;
  cluster symmetric
    additiveFAF homogeneousFAF additiveSAF homogeneousSAF Form of V,V;
  existence
  proof
    take NulForm(V,V); thus thesis;
  end;
  cluster alternating
    additiveFAF homogeneousFAF additiveSAF homogeneousSAF 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 Form of V,V;
  existence
  proof
    consider f be 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 Def11
        .= ff.(w,v) by Def11;
    end;
    hence thesis by Def26;
  end;
end;

registration
  let K be add-associative right_zeroed right_complementable
  (non empty addLoopStr);
  let V be non empty VectSpStr over K;
  cluster alternating additiveFAF additiveSAF 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 VectSpStr 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 Def3
      .= f.(w,v) + g.(v,w) by Def26
      .= f.(w,v) + g.(w,v) by Def26
      .= (f+g).(w,v) by Def3;
  end;
end;

registration
  let K be non empty doubleLoopStr;
  let V be non empty VectSpStr 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 Def4
      .= a*f.(w,v) by Def26
      .= (a*f).(w,v) by Def4;
  end;
end;

registration
  let K be non empty addLoopStr;
  let V be non empty VectSpStr 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 Def5
      .= -f.(w,v) by Def26
      .= (-f).(w,v) by Def5;
  end;
end;

registration
  let K be non empty addLoopStr;
  let V be non empty VectSpStr 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 VectSpStr 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 Def3
      .= 0.K + g.(v,v) by Def27
      .= 0.K + 0.K by Def27
      .= 0.K by RLVECT_1:def 7;
  end;
end;

registration
  let K be add-associative right_zeroed right_complementable
  right-distributive (non empty doubleLoopStr);
  let V be non empty VectSpStr 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 Def4
      .= a*0.K by Def27
      .= 0.K by VECTSP_1:36;
  end;
end;

registration
  let K be add-associative right_zeroed right_complementable
  (non empty addLoopStr);
  let V be non empty VectSpStr 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 Def5
      .= -0.K by Def27
      .= 0.K by RLVECT_1:25;
  end;
end;

registration
  let K be add-associative right_zeroed right_complementable
  (non empty addLoopStr);
  let V be non empty VectSpStr over K;
  let f,g be alternating Form of V,V;
  cluster f-g -> alternating;
  coherence;
end;

theorem
  for K be add-associative right_zeroed right_complementable
  right-distributive (non empty doubleLoopStr)
  for V be non empty VectSpStr over K
  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 VectSpStr over K, f be symmetric bilinear-Form of V,V;
  thus leftker f c= rightker f
  proof
    let x be set;
    assume x in leftker f;
    then consider v be Vector of V such that
A1: v = x & 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 Def26
        .= 0.K by A1;
    end;
    hence thesis by A1;
  end;
  let x be set;
  assume x in rightker f;
  then consider w be Vector of V such that
A2: w = x & 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 Def26
      .= 0.K by A2;
  end;
  hence thesis by A2;
end;

theorem Th59:
  for K be add-associative right_zeroed right_complementable
  (non empty addLoopStr) for V be non empty VectSpStr over K
  for f be alternating additiveSAF additiveFAF Form of V,V
  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 VectSpStr 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 Def27
    .= f.(v,v) + f.(v,w) + (f.(w,v) + f.(w,w)) by Th29
    .= 0.K + f.(v,w) + (f.(w,v) + f.(w,w)) by Def27
    .= 0.K + f.(v,w) + (f.(w,v) + 0.K) by Def27
    .= 0.K + f.(v,w) + f.(w,v) by RLVECT_1:def 7
    .= f.(v,w) + f.(w,v) by RLVECT_1:10;
  hence f.(v,w)= - f.(w,v) by RLVECT_1:19;
end;

definition
  let K be Fanoian Field;
  let V be non empty VectSpStr over K;
  let f be additiveSAF additiveFAF Form of V,V;
  redefine 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 Th59;
    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:63;
    hence thesis by VECTSP_1:def 28;
  end;
end;

theorem
  for K be add-associative right_zeroed right_complementable
  right-distributive (non empty doubleLoopStr)
  for V be non empty VectSpStr over K
  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 VectSpStr over K, f be alternating bilinear-Form of V,V;
  thus leftker f c= rightker f
  proof
    let x be set;
    assume x in leftker f;
    then consider v be Vector of V such that
A1: v = x & 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 Th59
        .= -0.K by A1
        .= 0.K by RLVECT_1:25;
    end;
    hence thesis by A1;
  end;
  let x be set;
  assume x in rightker f;
  then consider w be Vector of V such that
A2: w = x & 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 Th59
      .= -0.K by A2
      .= 0.K by RLVECT_1:25;
  end;
  hence thesis by A2;
end;