let K be 1-sorted ;
let V, W be VectSpStr of K;
mode Form of V,W is Function of [:the carrier of V,the carrier of W:],the carrier of K;

let K be non empty ZeroStr ;
let V, W be VectSpStr of K;
canceled;
func NulForm V,W -> Form of V,W equals :: BILINEAR:def 2
[:the carrier of V,the carrier of W:] --> (0. K);
coherence
[:the carrier of V,the carrier of W:] --> (0. K) is Form of V,W ;

let K be non empty LoopStr ;
let V, W be non empty VectSpStr of K;
let f, g be Form of V,W;
func f + g -> Form of V,W means :Def3: :: BILINEAR:def 3
for v being Vector of V
for w being Vector of W holds it . v,w = (f . v,w) + (g . v,w);
existence
ex b₁ being Form of V,W st
for v being Vector of V
for w being Vector of W holds b₁ . v,w = (f . v,w) + (g . v,w) uniqueness
for b₁, b₂ being Form of V,W st ( for v being Vector of V
for w being Vector of W holds b₁ . v,w = (f . v,w) + (g . v,w) ) & ( for v being Vector of V
for w being Vector of W holds b₂ . v,w = (f . v,w) + (g . v,w) ) holds
b₁ = b₂

let K be non empty HGrStr ;
let V, W be non empty VectSpStr of K;
let f be Form of V,W;
let a be Element of K;
func a * f -> Form of V,W means :Def4: :: BILINEAR:def 4
for v being Vector of V
for w being Vector of W holds it . v,w = a * (f . v,w);
existence
ex b₁ being Form of V,W st
for v being Vector of V
for w being Vector of W holds b₁ . v,w = a * (f . v,w) uniqueness
for b₁, b₂ being Form of V,W st ( for v being Vector of V
for w being Vector of W holds b₁ . v,w = a * (f . v,w) ) & ( for v being Vector of V
for w being Vector of W holds b₂ . v,w = a * (f . v,w) ) holds
b₁ = b₂

let K be non empty LoopStr ;
let V, W be non empty VectSpStr of K;
let f be Form of V,W;
func - f -> Form of V,W means :Def5: :: BILINEAR:def 5
for v being Vector of V
for w being Vector of W holds it . v,w = - (f . v,w);
existence
ex b₁ being Form of V,W st
for v being Vector of V
for w being Vector of W holds b₁ . v,w = - (f . v,w) uniqueness
for b₁, b₂ being Form of V,W st ( for v being Vector of V
for w being Vector of W holds b₁ . v,w = - (f . v,w) ) & ( for v being Vector of V
for w being Vector of W holds b₂ . v,w = - (f . v,w) ) holds
b₁ = b₂

let K be non empty add-associative right_zeroed right_complementable left-distributive left_unital doubleLoopStr ;
let V, W be non empty VectSpStr of K;
let f be Form of V,W;
:: original: -
redefine func - f -> Form of V,W equals :: BILINEAR:def 6
(- (1. K)) * f;
coherence
- f is Form of V,W ;
compatibility
for b₁ being Form of V,W holds
( b₁ = - f iff b₁ = (- (1. K)) * f )

let K be non empty LoopStr ;
let V, W be non empty VectSpStr of K;
let f, g be Form of V,W;
func f - g -> Form of V,W equals :: BILINEAR:def 7
f + (- g);
correctness
coherence
f + (- g) is Form of V,W;
;

let K be non empty LoopStr ;
let V, W be non empty VectSpStr of K;
let f, g be Form of V,W;
:: original: -
redefine func f - g -> Form of V,W means :Def8: :: BILINEAR:def 8
for v being Vector of V
for w being Vector of W holds it . v,w = (f . v,w) - (g . v,w);
coherence
f - g is Form of V,W ;
compatibility
for b₁ being Form of V,W holds
( b₁ = f - g iff for v being Vector of V
for w being Vector of W holds b₁ . v,w = (f . v,w) - (g . v,w) )

let K be non empty Abelian LoopStr ;
let V, W be non empty VectSpStr of K;
let f, g be Form of V,W;
hence f + g = g + f by BINOP_1:2;

let K be non empty Abelian LoopStr ;
let V, W be non empty VectSpStr of K;
let f, g be Form of V,W;
:: original: +
redefine func f + g -> Form of V,W;
commutativity
for f, g being Form of V,W holds f + g = g + f by Lm1;

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

let K be non empty 1-sorted ;
let V, W be non empty VectSpStr of K;
let f be Form of V,W;
let v be Vector of V;
func FunctionalFAF f,v -> Functional of W equals :: BILINEAR:def 9
(curry f) . v;
correctness
coherence
(curry f) . v is Functional of W;
by Lm3;

let K be non empty 1-sorted ;
let V, W be non empty VectSpStr of K;
let f be Form of V,W;
let w be Vector of W;
func FunctionalSAF f,w -> Functional of V equals :: BILINEAR:def 10
(curry' f) . w;
correctness
coherence
(curry' f) . w is Functional of V;
by Lm3;

let K be non empty HGrStr ;
let V, W be non empty VectSpStr of K;
let f be Functional of V;
let g be Functional of W;
func FormFunctional f,g -> Form of V,W means :Def11: :: BILINEAR:def 11
for v being Vector of V
for w being Vector of W holds it . v,w = (f . v) * (g . w);
existence
ex b₁ being Form of V,W st
for v being Vector of V
for w being Vector of W holds b₁ . v,w = (f . v) * (g . w) uniqueness
for b₁, b₂ being Form of V,W st ( for v being Vector of V
for w being Vector of W holds b₁ . v,w = (f . v) * (g . w) ) & ( for v being Vector of V
for w being Vector of W holds b₂ . v,w = (f . v) * (g . w) ) holds
b₁ = b₂

let K be non empty LoopStr ;
let V, W be non empty VectSpStr of K;
let f be Form of V,W;
attr f is additiveFAF means :Def12: :: BILINEAR:def 12
for v being Vector of V holds FunctionalFAF f,v is additive;
attr f is additiveSAF me