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 addLoopStr ;
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 multMagma ;
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 addLoopStr ;
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 right_complementable add-associative right_zeroed 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 addLoopStr ;
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 addLoopStr ;
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 addLoopStr ; :: thesis: for V, W being non empty VectSpStr of K
for f, g being Form of V,W holds f + g = g + f
let V, W be non empty VectSpStr of K; :: thesis: for f, g being Form of V,W holds f + g = g + f
let f, g be Form of V,W; :: thesis: f + g = g + f
hence f + g = g + f by BINOP_1:2; :: thesis: verum

let K be non empty Abelian addLoopStr ;
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 ; :: thesis: for V, W being non empty VectSpStr of K
for f being Form of V,W
for v being Element of the carrier of V
for y being Element of W holds
( (curry f) . v is Functional of W & (curry' f) . y is Functional of V )
let V, W be non empty VectSpStr of K; :: thesis: for f being Form of V,W
for v being Element of the carrier of V
for y being Element of W holds
( (curry f) . v is Functional of W & (curry' f) . y is Functional of V )
let f be Form of V,W; :: thesis: for v being Element of the carrier of V
for y being Element of W holds
( (curry f) . v is Functional of W & (curry' f) . y is Functional of V )
let v be Element of the carrier of V; :: thesis: for y being Element of W holds
( (curry f) . v is Functional of W & (curry' f) . y is Functional of V )
let y be Element of W; :: thesis: ( (curry f) . v is Functional of W & (curry' f) . y is Functional of V )
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;
reconsider g = 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 ; :: thesis: (curry' f) . y is Functional of V
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;
reconsider h = 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 ; :: thesis: verum

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 Lm2;

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 Lm2;

let K be non empty multMagma ;
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₂