:: BILINEAR semantic presentation

begin

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;
func NulForm (V,W) ->  Form of V,W equals :: BILINEAR:def 1
[: 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 ;
end;

:: deftheorem  defines NulForm BILINEAR:def_1_:_
 for K being non empty ZeroStr
for V, W being VectSpStr over K holds NulForm (V,W) = [: the carrier of V, the carrier of W:] --> (0. K);

definition
let K be non empty addLoopStr ;
let V, W be non empty VectSpStr over K;
let f, g be Form of V,W;
funcf + g ->  Form of V,W means :Def2: :: BILINEAR:def 2
 for v being Vector of V
for w being Vector of W holds it . (v,w) = (f . (v,w)) + (g . (v,w));
existence
 ex b1 being Form of V,W st
for v being Vector of V
for w being Vector of W holds b1 . (v,w) = (f . (v,w)) + (g . (v,w))
proof
set X = the carrier of V;
set Y = the carrier of W;
set Z = the carrier of K;
deffunc H1( Element of the carrier of V, Element of the carrier of W) ->  Element of the carrier of K = (f . ($1,$2)) + (g . ($1,$2));
consider ff being Function of [: the carrier of V, the carrier of W:], the carrier of K such that
A1: for x being Element of the carrier of V
for y being Element of the carrier of W holds ff . (x,y) = H1(x,y) from BINOP_1:sch_4();
reconsider ff = ff as Form of V,W ;
take  ff ; ::_thesis: for v being Vector of V
for w being Vector of W holds ff . (v,w) = (f . (v,w)) + (g . (v,w))
thus  for v being Vector of V
for w being Vector of W holds ff . (v,w) = (f . (v,w)) + (g . (v,w)) by A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Form of V,W st ( for v being Vector of V
for w being Vector of W holds b1 . (v,w) = (f . (v,w)) + (g . (v,w)) ) & ( for v being Vector of V
for w being Vector of W holds b2 . (v,w) = (f . (v,w)) + (g . (v,w)) ) holds
b1 = b2
proof
let F, G be Form of V,W; ::_thesis: ( ( for v being Vector of V
for w being Vector of W holds F . (v,w) = (f . (v,w)) + (g . (v,w)) ) & ( for v being Vector of V
for w being Vector of W holds G . (v,w) = (f . (v,w)) + (g . (v,w)) ) implies F = G )
assume that
A2: for v being Vector of V
for w being Vector of W holds F . (v,w) = (f . (v,w)) + (g . (v,w)) and
A3: for v being Vector of V
for w being Vector of W holds G . (v,w) = (f . (v,w)) + (g . (v,w)) ; ::_thesis: F = G
now__::_thesis:_for_v_being_Vector_of_V
for_w_being_Vector_of_W_holds_F_._(v,w)_=_G_._(v,w)
let v be Vector of V; ::_thesis: for w being Vector of W holds F . (v,w) = G . (v,w)
let w be Vector of W; ::_thesis: F . (v,w) = G . (v,w)
thus F . (v,w) = (f . (v,w)) + (g . (v,w)) by A2
.= G . (v,w) by A3 ; ::_thesis: verum
end;
hence  F = G by BINOP_1:2; ::_thesis: verum
end;
end;

:: deftheorem Def2 defines + BILINEAR:def_2_:_
 for K being non empty addLoopStr
for V, W being non empty VectSpStr over K
for f, g, b6 being Form of V,W holds
( b6 = f + g iff for v being Vector of V
for w being Vector of W holds b6 . (v,w) = (f . (v,w)) + (g . (v,w)) );

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;
funca * f ->  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) = a * (f . (v,w));
existence
 ex b1 being Form of V,W st
for v being Vector of V
for w being Vector of W holds b1 . (v,w) = a * (f . (v,w))
proof
set X = the carrier of V;
set Y = the carrier of W;
set Z = the carrier of K;
deffunc H1( Element of the carrier of V, Element of the carrier of W) ->  Element of the carrier of K = a * (f . ($1,$2));
consider ff being Function of [: the carrier of V, the carrier of W:], the carrier of K such that
A1: for x being Element of the carrier of V
for y being Element of the carrier of W holds ff . (x,y) = H1(x,y) from BINOP_1:sch_4();
reconsider ff = ff as Form of V,W ;
take  ff ; ::_thesis: for v being Vector of V
for w being Vector of W holds ff . (v,w) = a * (f . (v,w))
thus  for v being Vector of V
for w being Vector of W holds ff . (v,w) = a * (f . (v,w)) by A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Form of V,W st ( for v being Vector of V
for w being Vector of W holds b1 . (v,w) = a * (f . (v,w)) ) & ( for v being Vector of V
for w being Vector of W holds b2 . (v,w) = a * (f . (v,w)) ) holds
b1 = b2
proof
let F, G be Form of V,W; ::_thesis: ( ( for v being Vector of V
for w being Vector of W holds F . (v,w) = a * (f . (v,w)) ) & ( for v being Vector of V
for w being Vector of W holds G . (v,w) = a * (f . (v,w)) ) implies F = G )
assume that
A2: for v being Vector of V
for w being Vector of W holds F . (v,w) = a * (f . (v,w)) and
A3: for v being Vector of V
for w being Vector of W holds G . (v,w) = a * (f . (v,w)) ; ::_thesis: F = G
now__::_thesis:_for_v_being_Vector_of_V
for_w_being_Vector_of_W_holds_F_._(v,w)_=_G_._(v,w)
let v be Vector of V; ::_thesis: for w being Vector of W holds F . (v,w) = G . (v,w)
let w be Vector of W; ::_thesis: F . (v,w) = G . (v,w)
thus F . (v,w) = a * (f . (v,w)) by A2
.= G . (v,w) by A3 ; ::_thesis: verum
end;
hence  F = G by BINOP_1:2; ::_thesis: verum
end;
end;

:: deftheorem Def3 defines * BILINEAR:def_3_:_
 for K being non empty multMagma
for V, W being non empty VectSpStr over K
for f being Form of V,W
for a being Element of K
for b6 being Form of V,W holds
( b6 = a * f iff for v being Vector of V
for w being Vector of W holds b6 . (v,w) = a * (f . (v,w)) );

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 :Def4: :: BILINEAR:def 4
 for v being Vector of V
for w being Vector of W holds it . (v,w) = - (f . (v,w));
existence
 ex b1 being Form of V,W st
for v being Vector of V
for w being Vector of W holds b1 . (v,w) = - (f . (v,w))
proof
set X = the carrier of V;
set Y = the carrier of W;
set Z = the carrier of K;
deffunc H1( Element of the carrier of V, Element of the carrier of W) ->  Element of the carrier of K = - (f . ($1,$2));
consider ff being Function of [: the carrier of V, the carrier of W:], the carrier of K such that
A1: for x being Element of the carrier of V
for y being Element of the carrier of W holds ff . (x,y) = H1(x,y) from BINOP_1:sch_4();
reconsider ff = ff as Form of V,W ;
take  ff ; ::_thesis: for v being Vector of V
for w being Vector of W holds ff . (v,w) = - (f . (v,w))
thus  for v being Vector of V
for w being Vector of W holds ff . (v,w) = - (f . (v,w)) by A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Form of V,W st ( for v being Vector of V
for w being Vector of W holds b1 . (v,w) = - (f . (v,w)) ) & ( for v being Vector of V
for w being Vector of W holds b2 . (v,w) = - (f . (v,w)) ) holds
b1 = b2
proof
let F, G be Form of V,W; ::_thesis: ( ( for v being Vector of V
for w being Vector of W holds F . (v,w) = - (f . (v,w)) ) & ( for v being Vector of V
for w being Vector of W holds G . (v,w) = - (f . (v,w)) ) implies F = G )
assume that
A2: for v being Vector of V
for w being Vector of W holds F . (v,w) = - (f . (v,w)) and
A3: for v being Vector of V
for w being Vector of W holds G . (v,w) = - (f . (v,w)) ; ::_thesis: F = G
now__::_thesis:_for_v_being_Vector_of_V
for_w_being_Vector_of_W_holds_F_._(v,w)_=_G_._(v,w)
let v be Vector of V; ::_thesis: for w being Vector of W holds F . (v,w) = G . (v,w)
let w be Vector of W; ::_thesis: F . (v,w) = G . (v,w)
thus F . (v,w) = - (f . (v,w)) by A2
.= G . (v,w) by A3 ; ::_thesis: verum
end;
hence  F = G by BINOP_1:2; ::_thesis: verum
end;
end;

:: deftheorem Def4 defines - BILINEAR:def_4_:_
 for K being non empty addLoopStr
for V, W being non empty VectSpStr over K
for f, b5 being Form of V,W holds
( b5 = - f iff for v being Vector of V
for w being Vector of W holds b5 . (v,w) = - (f . (v,w)) );

definition
let K be non empty right_complementable add-associative right_zeroed left-distributive left_unital doubleLoopStr ;
let V, W be non empty VectSpStr over K;
let f be Form of V,W;
redefine func - f equals :: BILINEAR:def 5
(- (1. K)) * f;
compatibility
 for b1 being Form of V,W holds
( b1 = - f iff b1 = (- (1. K)) * f )
proof
let g be Form of V,W; ::_thesis: ( g = - f iff g = (- (1. K)) * f )
thus  ( g = - f implies g = (- (1. K)) * f ) ::_thesis: ( g = (- (1. K)) * f implies g = - f )
proof
assume A1: g = - f ; ::_thesis: g = (- (1. K)) * f
now__::_thesis:_for_v_being_Vector_of_V
for_w_being_Vector_of_W_holds_g_._(v,w)_=_((-_(1._K))_*_f)_._(v,w)
let v be Vector of V; ::_thesis: for w being Vector of W holds g . (v,w) = ((- (1. K)) * f) . (v,w)
let w be Vector of W; ::_thesis: g . (v,w) = ((- (1. K)) * f) . (v,w)
thus g . (v,w) = - (f . (v,w)) by A1, Def4
.= (- (1. K)) * (f . (v,w)) by VECTSP_2:29
.= ((- (1. K)) * f) . (v,w) by Def3 ; ::_thesis: verum
end;
hence  g = (- (1. K)) * f by BINOP_1:2; ::_thesis: verum
end;
assume A2: g = (- (1. K)) * f ; ::_thesis: g = - f
now__::_thesis:_for_v_being_Vector_of_V
for_w_being_Vector_of_W_holds_g_._(v,w)_=_(-_f)_._(v,w)
let v be Vector of V; ::_thesis: for w being Vector of W holds g . (v,w) = (- f) . (v,w)
let w be Vector of W; ::_thesis: g . (v,w) = (- f) . (v,w)
thus g . (v,w) = (- (1. K)) * (f . (v,w)) by A2, Def3
.= - (f . (v,w)) by VECTSP_2:29
.= (- f) . (v,w) by Def4 ; ::_thesis: verum
end;
hence  g = - f by BINOP_1:2; ::_thesis: verum
end;
end;

:: deftheorem  defines - BILINEAR:def_5_:_
 for K being non empty right_complementable add-associative right_zeroed left-distributive left_unital doubleLoopStr
for V, W being non empty VectSpStr over K
for f being Form of V,W holds - f = (- (1. K)) * f;

definition
let K be non empty addLoopStr ;
let V, W be non empty VectSpStr over K;
let f, g be Form of V,W;
funcf - g ->  Form of V,W equals :: BILINEAR:def 6
f + (- g);
correctness
coherence
f + (- g) is Form of V,W;
;
end;

:: deftheorem  defines - BILINEAR:def_6_:_
 for K being non empty addLoopStr
for V, W being non empty VectSpStr over K
for f, g being Form of V,W holds f - g = f + (- g);

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 means :Def7: :: BILINEAR:def 7
 for v being Vector of V
for w being Vector of W holds it . (v,w) = (f . (v,w)) - (g . (v,w));
compatibility
 for b1 being Form of V,W holds
( b1 = f - g iff for v being Vector of V
for w being Vector of W holds b1 . (v,w) = (f . (v,w)) - (g . (v,w)) )
proof
let h be Form of V,W; ::_thesis: ( h = f - g iff for v being Vector of V
for w being Vector of W holds h . (v,w) = (f . (v,w)) - (g . (v,w)) )
thus  ( h = f - g implies for v being Vector of V
for w being Vector of W holds h . (v,w) = (f . (v,w)) - (g . (v,w)) ) ::_thesis: ( ( for v being Vector of V
for w being Vector of W holds h . (v,w) = (f . (v,w)) - (g . (v,w)) ) implies h = f - g )
proof
assume A1: h = f - g ; ::_thesis: for v being Vector of V
for w being Vector of W holds h . (v,w) = (f . (v,w)) - (g . (v,w))
let v be Vector of V; ::_thesis: for w being Vector of W holds h . (v,w) = (f . (v,w)) - (g . (v,w))
let w be Vector of W; ::_thesis: h . (v,w) = (f . (v,w)) - (g . (v,w))
thus h . (v,w) = (f . (v,w)) + ((- g) . (v,w)) by A1, Def2
.= (f . (v,w)) + (- (g . (v,w))) by Def4
.= (f . (v,w)) - (g . (v,w)) by RLVECT_1:def_11 ; ::_thesis: verum
end;
assume A2: for v being Vector of V
for w being Vector of W holds h . (v,w) = (f . (v,w)) - (g . (v,w)) ; ::_thesis: h = f - g
now__::_thesis:_for_v_being_Vector_of_V
for_w_being_Vector_of_W_holds_h_._(v,w)_=_(f_-_g)_._(v,w)
let v be Vector of V; ::_thesis: for w being Vector of W holds h . (v,w) = (f - g) . (v,w)
let w be Vector of W; ::_thesis: h . (v,w) = (f - g) . (v,w)
thus h . (v,w) = (f . (v,w)) - (g . (v,w)) by A2
.= (f . (v,w)) + (- (g . (v,w))) by RLVECT_1:def_11
.= (f . (v,w)) + ((- g) . (v,w)) by Def4
.= (f - g) . (v,w) by Def2 ; ::_thesis: verum
end;
hence  h = f - g by BINOP_1:2; ::_thesis: verum
end;
end;

:: deftheorem Def7 defines - BILINEAR:def_7_:_
 for K being non empty addLoopStr
for V, W being non empty VectSpStr over K
for f, g, b6 being Form of V,W holds
( b6 = f - g iff for v being Vector of V
for w being Vector of W holds b6 . (v,w) = (f . (v,w)) - (g . (v,w)) );

definition
let K be non empty Abelian addLoopStr ;
let V, W be non empty VectSpStr over K;
let f, g be Form of V,W;
:: original: +
redefine funcf + g ->  Form of V,W;
commutativity
 for f, g being Form of V,W holds f + g = g + f
proof
let f, g be Form of V,W; ::_thesis: f + g = g + f
now__::_thesis:_for_v_being_Vector_of_V
for_w_being_Vector_of_W_holds_(f_+_g)_._(v,w)_=_(g_+_f)_._(v,w)
let v be Vector of V; ::_thesis: for w being Vector of W holds (f + g) . (v,w) = (g + f) . (v,w)
let w be Vector of W; ::_thesis: (f + g) . (v,w) = (g + f) . (v,w)
thus (f + g) . (v,w) = (f . (v,w)) + (g . (v,w)) by Def2
.= (g + f) . (v,w) by Def2 ; ::_thesis: verum
end;
hence  f + g = g + f by BINOP_1:2; ::_thesis: verum
end;
end;

theorem :: BILINEAR:1
for K being non empty right_zeroed addLoopStr
for V, W being non empty VectSpStr over K
for f being Form of V,W holds f + (NulForm (V,W)) = f
proof
let K be non empty right_zeroed addLoopStr ; ::_thesis: for V, W being non empty VectSpStr over K
for f being Form of V,W holds f + (NulForm (V,W)) = f
let V, W be non empty VectSpStr over K; ::_thesis: for f being Form of V,W holds f + (NulForm (V,W)) = f
let f be Form of V,W; ::_thesis: f + (NulForm (V,W)) = f
set g = NulForm (V,W);
now__::_thesis:_for_v_being_Vector_of_V
for_w_being_Vector_of_W_holds_(f_+_(NulForm_(V,W)))_._(v,w)_=_f_._(v,w)
let v be Vector of V; ::_thesis: for w being Vector of W holds (f + (NulForm (V,W))) . (v,w) = f . (v,w)
let w be Vector of W; ::_thesis: (f + (NulForm (V,W))) . (v,w) = f . (v,w)
thus (f + (NulForm (V,W))) . (v,w) = (f . (v,w)) + ((NulForm (V,W)) . (v,w)) by Def2
.= (f . (v,w)) + (0. K) by FUNCOP_1:70
.= f . (v,w) by RLVECT_1:def_4 ; ::_thesis: verum
end;
hence  f + (NulForm (V,W)) = f by BINOP_1:2; ::_thesis: verum
end;

theorem :: BILINEAR:2
for K being non empty add-associative addLoopStr
for V, W being non empty VectSpStr over K
for f, g, h being Form of V,W holds (f + g) + h = f + (g + h)
proof
let K be non empty add-associative addLoopStr ; ::_thesis: for V, W being non empty VectSpStr over K
for f, g, h being Form of V,W holds (f + g) + h = f + (g + h)
let V, W be non empty VectSpStr over K; ::_thesis: for f, g, h being Form of V,W holds (f + g) + h = f + (g + h)
let f, g, h be Form of V,W; ::_thesis: (f + g) + h = f + (g + h)
now__::_thesis:_for_v_being_Vector_of_V
for_w_being_Vector_of_W_holds_((f_+_g)_+_h)_._(v,w)_=_(f_+_(g_+_h))_._(v,w)
let v be Vector of V; ::_thesis: for w being Vector of W holds ((f + g) + h) . (v,w) = (f + (g + h)) . (v,w)
let w be Vector of W; ::_thesis: ((f + g) + h) . (v,w) = (f + (g + h)) . (v,w)
thus ((f + g) + h) . (v,w) = ((f + g) . (v,w)) + (h . (v,w)) by Def2
.= ((f . (v,w)) + (g . (v,w))) + (h . (v,w)) by Def2
.= (f . (v,w)) + ((g . (v,w)) + (h . (v,w))) by RLVECT_1:def_3
.= (f . (v,w)) + ((g + h) . (v,w)) by Def2
.= (f + (g + h)) . (v,w) by Def2 ; ::_thesis: verum
end;
hence  (f + g) + h = f + (g + h) by BINOP_1:2; ::_thesis: verum
end;

theorem :: BILINEAR:3
for K being non empty right_complementable add-associative right_zeroed addLoopStr
for V, W being non empty VectSpStr over K
for f being Form of V,W holds f - f = NulForm (V,W)
proof
let K be non empty right_complementable add-associative right_zeroed addLoopStr ; ::_thesis: for V, W being non empty VectSpStr over K
for f being Form of V,W holds f - f = NulForm (V,W)
let V, W be non empty VectSpStr over K; ::_thesis: for f being Form of V,W holds f - f = NulForm (V,W)
let f be Form of V,W; ::_thesis: f - f = NulForm (V,W)
now__::_thesis:_for_v_being_Vector_of_V
for_w_being_Vector_of_W_holds_(f_-_f)_._(v,w)_=_(NulForm_(V,W))_._(v,w)
let v be Vector of V; ::_thesis: for w being Vector of W holds (f - f) . (v,w) = (NulForm (V,W)) . (v,w)
let w be Vector of W; ::_thesis: (f - f) . (v,w) = (NulForm (V,W)) . (v,w)
thus (f - f) . (v,w) = (f . (v,w)) - (f . (v,w)) by Def7
.= 0. K by RLVECT_1:15
.= (NulForm (V,W)) . (v,w) by FUNCOP_1:70 ; ::_thesis: verum
end;
hence  f - f = NulForm (V,W) by BINOP_1:2; ::_thesis: verum
end;

theorem :: BILINEAR:4
for K being non empty right-distributive doubleLoopStr
for V, W being non empty VectSpStr over K
for a being Element of K
for f, g being Form of V,W holds a * (f + g) = (a * f) + (a * g)
proof
let K be non empty right-distributive doubleLoopStr ; ::_thesis: for V, W being non empty VectSpStr over K
for a being Element of K
for f, g being Form of V,W holds a * (f + g) = (a * f) + (a * g)
let V, W be non empty VectSpStr over K; ::_thesis: for a being Element of K
for f, g being Form of V,W holds a * (f + g) = (a * f) + (a * g)
let r be Element of K; ::_thesis: for f, g being Form of V,W holds r * (f + g) = (r * f) + (r * g)
let f, g be Form of V,W; ::_thesis: r * (f + g) = (r * f) + (r * g)
now__::_thesis:_for_v_being_Vector_of_V
for_w_being_Vector_of_W_holds_(r_*_(f_+_g))_._(v,w)_=_((r_*_f)_+_(r_*_g))_._(v,w)
let v be Vector of V; ::_thesis: for w being Vector of W holds (r * (f + g)) . (v,w) = ((r * f) + (r * g)) . (v,w)
let w be Vector of W; ::_thesis: (r * (f + g)) . (v,w) = ((r * f) + (r * g)) . (v,w)
thus (r * (f + g)) . (v,w) = r * ((f + g) . (v,w)) by Def3
.= r * ((f . (v,w)) + (g . (v,w))) by Def2
.= (r * (f . (v,w))) + (r * (g . (v,w))) by VECTSP_1:def_2
.= ((r * f) . (v,w)) + (r * (g . (v,w))) by Def3
.= ((r * f) . (v,w)) + ((r * g) . (v,w)) by Def3
.= ((r * f) + (r * g)) . (v,w) by Def2 ; ::_thesis: verum
end;
hence  r * (f + g) = (r * f) + (r * g) by BINOP_1:2; ::_thesis: verum
end;

theorem :: BILINEAR:5
for K being non empty left-distributive doubleLoopStr
for V, W being non empty VectSpStr over K
for a, b being Element of K
for f being Form of V,W holds (a + b) * f = (a * f) + (b * f)
proof
let K be non empty left-distributive doubleLoopStr ; ::_thesis: for V, W being non empty VectSpStr over K
for a, b being Element of K
for f being Form of V,W holds (a + b) * f = (a * f) + (b * f)
let V, W be non empty VectSpStr over K; ::_thesis: for a, b being Element of K
for f being Form of V,W holds (a + b) * f = (a * f) + (b * f)
let r, s be Element of K; ::_thesis: for f being Form of V,W holds (r + s) * f = (r * f) + (s * f)
let f be Form of V,W; ::_thesis: (r + s) * f = (r * f) + (s * f)
now__::_thesis:_for_v_being_Vector_of_V
for_w_being_Vector_of_W_holds_((r_+_s)_*_f)_._(v,w)_=_((r_*_f)_+_(s_*_f))_._(v,w)
let v be Vector of V; ::_thesis: for w being Vector of W holds ((r + s) * f) . (v,w) = ((r * f) + (s * f)) . (v,w)
let w be Vector of W; ::_thesis: ((r + s) * f) . (v,w) = ((r * f) + (s * f)) . (v,w)
thus ((r + s) * f) . (v,w) = (r + s) * (f . (v,w)) by Def3
.= (r * (f . (v,w))) + (s * (f . (v,w))) by VECTSP_1:def_3
.= ((r * f) . (v,w)) + (s * (f . (v,w))) by Def3
.= ((r * f) . (v,w)) + ((s * f) . (v,w)) by Def3
.= ((r * f) + (s * f)) . (v,w) by Def2 ; ::_thesis: verum
end;
hence  (r + s) * f = (r * f) + (s * f) by BINOP_1:2; ::_thesis: verum
end;

theorem :: BILINEAR:6
for K being non empty associative doubleLoopStr
for V, W being non empty VectSpStr over K
for a, b being Element of K
for f being Form of V,W holds (a * b) * f = a * (b * f)
proof
let K be non empty associative doubleLoopStr ; ::_thesis: for V, W being non empty VectSpStr over K
for a, b being Element of K
for f being Form of V,W holds (a * b) * f = a * (b * f)
let V, W be non empty VectSpStr over K; ::_thesis: for a, b being Element of K
for f being Form of V,W holds (a * b) * f = a * (b * f)
let r, s be Element of K; ::_thesis: for f being Form of V,W holds (r * s) * f = r * (s * f)
let f be Form of V,W; ::_thesis: (r * s) * f = r * (s * f)
now__::_thesis:_for_v_being_Vector_of_V
for_w_being_Vector_of_W_holds_((r_*_s)_*_f)_._(v,w)_=_(r_*_(s_*_f))_._(v,w)
let v be Vector of V; ::_thesis: for w being Vector of W holds ((r * s) * f) . (v,w) = (r * (s * f)) . (v,w)
let w be Vector of W; ::_thesis: ((r * s) * f) . (v,w) = (r * (s * f)) . (v,w)
thus ((r * s) * f) . (v,w) = (r * s) * (f . (v,w)) by Def3
.= r * (s * (f . (v,w))) by GROUP_1:def_3
.= r * ((s * f) . (v,w)) by Def3
.= (r * (s * f)) . (v,w) by Def3 ; ::_thesis: verum
end;
hence  (r * s) * f = r * (s * f) by BINOP_1:2; ::_thesis: verum
end;

theorem :: BILINEAR:7
for K being non empty left_unital doubleLoopStr
for V, W being non empty VectSpStr over K
for f being Form of V,W holds (1. K) * f = f
proof
let K be non empty left_unital doubleLoopStr ; ::_thesis: for V, W being non empty VectSpStr over K
for f being Form of V,W holds (1. K) * f = f
let V, W be non empty VectSpStr over K; ::_thesis: for f being Form of V,W holds (1. K) * f = f
let f be Form of V,W; ::_thesis: (1. K) * f = f
now__::_thesis:_for_v_being_Vector_of_V
for_w_being_Vector_of_W_holds_((1._K)_*_f)_._(v,w)_=_f_._(v,w)
let v be Vector of V; ::_thesis: for w being Vector of W holds ((1. K) * f) . (v,w) = f . (v,w)
let w be Vector of W; ::_thesis: ((1. K) * f) . (v,w) = f . (v,w)
thus ((1. K) * f) . (v,w) = (1. K) * (f . (v,w)) by Def3
.= f . (v,w) by VECTSP_1:def_8 ; ::_thesis: verum
end;
hence  (1. K) * f = f by BINOP_1:2; ::_thesis: verum
end;

begin

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

:: deftheorem  defines FunctionalFAF BILINEAR:def_8_:_
 for K being non empty 1-sorted
for V, W being non empty VectSpStr over K
for f being Form of V,W
for v being Vector of V holds FunctionalFAF (f,v) = (curry f) . v;

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

:: deftheorem  defines FunctionalSAF BILINEAR:def_9_:_
 for K being non empty 1-sorted
for V, W being non empty VectSpStr over K
for f being Form of V,W
for w being Vector of W holds FunctionalSAF (f,w) = (curry' f) . w;

theorem Th8: :: BILINEAR:8
for K being non empty 1-sorted
for V, W being non empty VectSpStr over K
for f being Form of V,W
for v being Vector of V holds
( dom (FunctionalFAF (f,v)) = the carrier of W & rng (FunctionalFAF (f,v)) c= the carrier of K & ( for w being Vector of W holds (FunctionalFAF (f,v)) . w = f . (v,w) ) )
proof
let K be non empty 1-sorted ; ::_thesis: for V, W being non empty VectSpStr over K
for f being Form of V,W
for v being Vector of V holds
( dom (FunctionalFAF (f,v)) = the carrier of W & rng (FunctionalFAF (f,v)) c= the carrier of K & ( for w being Vector of W holds (FunctionalFAF (f,v)) . w = f . (v,w) ) )
let V, W be non empty VectSpStr over K; ::_thesis: for f being Form of V,W
for v being Vector of V holds
( dom (FunctionalFAF (f,v)) = the carrier of W & rng (FunctionalFAF (f,v)) c= the carrier of K & ( for w being Vector of W holds (FunctionalFAF (f,v)) . w = f . (v,w) ) )
let f be Form of V,W; ::_thesis: for v being Vector of V holds
( dom (FunctionalFAF (f,v)) = the carrier of W & rng (FunctionalFAF (f,v)) c= the carrier of K & ( for w being Vector of W holds (FunctionalFAF (f,v)) . w = f . (v,w) ) )
let v be Vector of V; ::_thesis: ( dom (FunctionalFAF (f,v)) = the carrier of W & rng (FunctionalFAF (f,v)) c= the carrier of K & ( for w being Vector of W holds (FunctionalFAF (f,v)) . w = f . (v,w) ) )
set F = FunctionalFAF (f,v);
 dom f = [: the carrier of V, the carrier of W:] by FUNCT_2:def_1;
then A1: ex g being Function st
( (curry f) . v = g & dom g = the carrier of W & rng g c= rng f & ( for y being set st y in the carrier of W holds
g . y = f . (v,y) ) ) by FUNCT_5:29;
hence  ( dom (FunctionalFAF (f,v)) = the carrier of W & rng (FunctionalFAF (f,v)) c= the carrier of K ) ; ::_thesis: for w being Vector of W holds (FunctionalFAF (f,v)) . w = f . (v,w)
let y be Vector of W; ::_thesis: (FunctionalFAF (f,v)) . y = f . (v,y)
thus  (FunctionalFAF (f,v)) . y = f . (v,y) by A1; ::_thesis: verum
end;

theorem Th9: :: BILINEAR:9
for K being non empty 1-sorted
for V, W being non empty VectSpStr over K
for f being Form of V,W
for w being Vector of W holds
( dom (FunctionalSAF (f,w)) = the carrier of V & rng (FunctionalSAF (f,w)) c= the carrier of K & ( for v being Vector of V holds (FunctionalSAF (f,w)) . v = f . (v,w) ) )
proof
let K be non empty 1-sorted ; ::_thesis: for V, W being non empty VectSpStr over K
for f being Form of V,W
for w being Vector of W holds
( dom (FunctionalSAF (f,w)) = the carrier of V & rng (FunctionalSAF (f,w)) c= the carrier of K & ( for v being Vector of V holds (FunctionalSAF (f,w)) . v = f . (v,w) ) )
let V, W be non empty VectSpStr over K; ::_thesis: for f being Form of V,W
for w being Vector of W holds
( dom (FunctionalSAF (f,w)) = the carrier of V & rng (FunctionalSAF (f,w)) c= the carrier of K & ( for v being Vector of V holds (FunctionalSAF (f,w)) . v = f . (v,w) ) )
let f be Form of V,W; ::_thesis: for w being Vector of W holds
( dom (FunctionalSAF (f,w)) = the carrier of V & rng (FunctionalSAF (f,w)) c= the carrier of K & ( for v being Vector of V holds (FunctionalSAF (f,w)) . v = f . (v,w) ) )
let w be Vector of W; ::_thesis: ( dom (FunctionalSAF (f,w)) = the carrier of V & rng (FunctionalSAF (f,w)) c= the carrier of K & ( for v being Vector of V holds (FunctionalSAF (f,w)) . v = f . (v,w) ) )
set F = FunctionalSAF (f,w);
 dom f = [: the carrier of V, the carrier of W:] by FUNCT_2:def_1;
then A1: ex g being Function st
( (curry' f) . w = g & dom g = the carrier of V & rng g c= rng f & ( for y being set st y in the carrier of V holds
g . y = f . (y,w) ) ) by FUNCT_5:32;
hence  ( dom (FunctionalSAF (f,w)) = the carrier of V & rng (FunctionalSAF (f,w)) c= the carrier of K ) ; ::_thesis: for v being Vector of V holds (FunctionalSAF (f,w)) . v = f . (v,w)
let v be Vector of V; ::_thesis: (FunctionalSAF (f,w)) . v = f . (v,w)
thus  (FunctionalSAF (f,w)) . v = f . (v,w) by A1; ::_thesis: verum
end;

theorem Th10: :: BILINEAR:10
for K being non empty ZeroStr
for V, W being non empty VectSpStr over K
for v being Vector of V holds FunctionalFAF ((NulForm (V,W)),v) = 0Functional W
proof
let K be non empty ZeroStr ; ::_thesis: for V, W being non empty VectSpStr over K
for v being Vector of V holds FunctionalFAF ((NulForm (V,W)),v) = 0Functional W
let V, W be non empty VectSpStr over K; ::_thesis: for v being Vector of V holds FunctionalFAF ((NulForm (V,W)),v) = 0Functional W
let v be Vector of V; ::_thesis: FunctionalFAF ((NulForm (V,W)),v) = 0Functional W
set N = NulForm (V,W);
now__::_thesis:_for_y_being_Vector_of_W_holds_(FunctionalFAF_((NulForm_(V,W)),v))_._y_=_(0Functional_W)_._y
let y be Vector of W; ::_thesis: (FunctionalFAF ((NulForm (V,W)),v)) . y = (0Functional W) . y
thus (FunctionalFAF ((NulForm (V,W)),v)) . y = (NulForm (V,W)) . (v,y) by Th8
.= 0. K by FUNCOP_1:70
.= (0Functional W) . y by HAHNBAN1:14 ; ::_thesis: verum
end;
hence  FunctionalFAF ((NulForm (V,W)),v) = 0Functional W by FUNCT_2:63; ::_thesis: verum
end;

theorem Th11: :: BILINEAR:11
for K being non empty ZeroStr
for V, W being non empty VectSpStr over K
for w being Vector of W holds FunctionalSAF ((NulForm (V,W)),w) = 0Functional V
proof
let K be non empty ZeroStr ; ::_thesis: for V, W being non empty VectSpStr over K
for w being Vector of W holds FunctionalSAF ((NulForm (V,W)),w) = 0Functional V
let V, W be non empty VectSpStr over K; ::_thesis: for w being Vector of W holds FunctionalSAF ((NulForm (V,W)),w) = 0Functional V
let y be Vector of W; ::_thesis: FunctionalSAF ((NulForm (V,W)),y) = 0Functional V
set N = NulForm (V,W);
now__::_thesis:_for_v_being_Vector_of_V_holds_(FunctionalSAF_((NulForm_(V,W)),y))_._v_=_(0Functional_V)_._v
let v be Vector of V; ::_thesis: (FunctionalSAF ((NulForm (V,W)),y)) . v = (0Functional V) . v
thus (FunctionalSAF ((NulForm (V,W)),y)) . v = (NulForm (V,W)) . (v,y) by Th9
.= 0. K by FUNCOP_1:70
.= (0Functional V) . v by HAHNBAN1:14 ; ::_thesis: verum
end;
hence  FunctionalSAF ((NulForm (V,W)),y) = 0Functional V by FUNCT_2:63; ::_thesis: verum
end;

theorem Th12: :: BILINEAR:12
for K being non empty addLoopStr
for V, W being non empty VectSpStr over K
for f, g being Form of V,W
for w being Vector of W holds FunctionalSAF ((f + g),w) = (FunctionalSAF (f,w)) + (FunctionalSAF (g,w))
proof
let K be non empty addLoopStr ; ::_thesis: for V, W being non empty VectSpStr over K
for f, g being Form of V,W
for w being Vector of W holds FunctionalSAF ((f + g),w) = (FunctionalSAF (f,w)) + (FunctionalSAF (g,w))
let V, W be non empty VectSpStr over K; ::_thesis: for f, g being Form of V,W
for w being Vector of W holds FunctionalSAF ((f + g),w) = (FunctionalSAF (f,w)) + (FunctionalSAF (g,w))
let f, g be Form of V,W; ::_thesis: for w being Vector of W holds FunctionalSAF ((f + g),w) = (FunctionalSAF (f,w)) + (FunctionalSAF (g,w))
let w be Vector of W; ::_thesis: FunctionalSAF ((f + g),w) = (FunctionalSAF (f,w)) + (FunctionalSAF (g,w))
now__::_thesis:_for_v_being_Vector_of_V_holds_(FunctionalSAF_((f_+_g),w))_._v_=_((FunctionalSAF_(f,w))_+_(FunctionalSAF_(g,w)))_._v
let v be Vector of V; ::_thesis: (FunctionalSAF ((f + g),w)) . v = ((FunctionalSAF (f,w)) + (FunctionalSAF (g,w))) . v
thus (FunctionalSAF ((f + g),w)) . v = (f + g) . (v,w) by Th9
.= (f . (v,w)) + (g . (v,w)) by Def2
.= ((FunctionalSAF (f,w)) . v) + (g . (v,w)) by Th9
.= ((FunctionalSAF (f,w)) . v) + ((FunctionalSAF (g,w)) . v) by Th9
.= ((FunctionalSAF (f,w)) + (FunctionalSAF (g,w))) . v by HAHNBAN1:def_3 ; ::_thesis: verum
end;
hence  FunctionalSAF ((f + g),w) = (FunctionalSAF (f,w)) + (FunctionalSAF (g,w)) by FUNCT_2:63; ::_thesis: verum
end;

theorem Th13: :: BILINEAR:13
for K being non empty addLoopStr
for V, W being non empty VectSpStr over K
for f, g being Form of V,W
for v being Vector of V holds FunctionalFAF ((f + g),v) = (FunctionalFAF (f,v)) + (FunctionalFAF (g,v))
proof
let K be non empty addLoopStr ; ::_thesis: for V, W being non empty VectSpStr over K
for f, g being Form of V,W
for v being Vector of V holds FunctionalFAF ((f + g),v) = (FunctionalFAF (f,v)) + (FunctionalFAF (g,v))
let V, W be non empty VectSpStr over K; ::_thesis: for f, g being Form of V,W
for v being Vector of V holds FunctionalFAF ((f + g),v) = (FunctionalFAF (f,v)) + (FunctionalFAF (g,v))
let f, g be Form of V,W; ::_thesis: for v being Vector of V holds FunctionalFAF ((f + g),v) = (FunctionalFAF (f,v)) + (FunctionalFAF (g,v))
let w be Vector of V; ::_thesis: FunctionalFAF ((f + g),w) = (FunctionalFAF (f,w)) + (FunctionalFAF (g,w))
now__::_thesis:_for_v_being_Vector_of_W_holds_(FunctionalFAF_((f_+_g),w))_._v_=_((FunctionalFAF_(f,w))_+_(FunctionalFAF_(g,w)))_._v
let v be Vector of W; ::_thesis: (FunctionalFAF ((f + g),w)) . v = ((FunctionalFAF (f,w)) + (FunctionalFAF (g,w))) . v
thus (FunctionalFAF ((f + g),w)) . v = (f + g) . (w,v) by Th8
.= (f . (w,v)) + (g . (w,v)) by Def2
.= ((FunctionalFAF (f,w)) . v) + (g . (w,v)) by Th8
.= ((FunctionalFAF (f,w)) . v) + ((FunctionalFAF (g,w)) . v) by Th8
.= ((FunctionalFAF (f,w)) + (FunctionalFAF (g,w))) . v by HAHNBAN1:def_3 ; ::_thesis: verum
end;
hence  FunctionalFAF ((f + g),w) = (FunctionalFAF (f,w)) + (FunctionalFAF (g,w)) by FUNCT_2:63; ::_thesis: verum
end;

theorem Th14: :: BILINEAR:14
for K being non empty doubleLoopStr
for V, W being non empty VectSpStr over K
for f being Form of V,W
for a being Element of K
for w being Vector of W holds FunctionalSAF ((a * f),w) = a * (FunctionalSAF (f,w))
proof
let K be non empty doubleLoopStr ; ::_thesis: for V, W being non empty VectSpStr over K
for f being Form of V,W
for a being Element of K
for w being Vector of W holds FunctionalSAF ((a * f),w) = a * (FunctionalSAF (f,w))
let V, W be non empty VectSpStr over K; ::_thesis: for f being Form of V,W
for a being Element of K
for w being Vector of W holds FunctionalSAF ((a * f),w) = a * (FunctionalSAF (f,w))
let f be Form of V,W; ::_thesis: for a being Element of K
for w being Vector of W holds FunctionalSAF ((a * f),w) = a * (FunctionalSAF (f,w))
let a be Element of K; ::_thesis: for w being Vector of W holds FunctionalSAF ((a * f),w) = a * (FunctionalSAF (f,w))
let w be Vector of W; ::_thesis: FunctionalSAF ((a * f),w) = a * (FunctionalSAF (f,w))
now__::_thesis:_for_v_being_Vector_of_V_holds_(FunctionalSAF_((a_*_f),w))_._v_=_(a_*_(FunctionalSAF_(f,w)))_._v
let v be Vector of V; ::_thesis: (FunctionalSAF ((a * f),w)) . v = (a * (FunctionalSAF (f,w))) . v
thus (FunctionalSAF ((a * f),w)) . v = (a * f) . (v,w) by Th9
.= a * (f . (v,w)) by Def3
.= a * ((FunctionalSAF (f,w)) . v) by Th9
.= (a * (FunctionalSAF (f,w))) . v by HAHNBAN1:def_6 ; ::_thesis: verum
end;
hence  FunctionalSAF ((a * f),w) = a * (FunctionalSAF (f,w)) by FUNCT_2:63; ::_thesis: verum
end;

theorem Th15: :: BILINEAR:15
for K being non empty doubleLoopStr
for V, W being non empty VectSpStr over K
for f being Form of V,W
for a being Element of K
for v being Vector of V holds FunctionalFAF ((a * f),v) = a * (FunctionalFAF (f,v))
proof
let K be non empty doubleLoopStr ; ::_thesis: for V, W being non empty VectSpStr over K
for f being Form of V,W
for a being Element of K
for v being Vector of V holds FunctionalFAF ((a * f),v) = a * (FunctionalFAF (f,v))
let V, W be non empty VectSpStr over K; ::_thesis: for f being Form of V,W
for a being Element of K
for v being Vector of V holds FunctionalFAF ((a * f),v) = a * (FunctionalFAF (f,v))
let f be Form of V,W; ::_thesis: for a being Element of K
for v being Vector of V holds FunctionalFAF ((a * f),v) = a * (FunctionalFAF (f,v))
let a be Element of K; ::_thesis: for v being Vector of V holds FunctionalFAF ((a * f),v) = a * (FunctionalFAF (f,v))
let w be Vector of V; ::_thesis: FunctionalFAF ((a * f),w) = a * (FunctionalFAF (f,w))
now__::_thesis:_for_v_being_Vector_of_W_holds_(FunctionalFAF_((a_*_f),w))_._v_=_(a_*_(FunctionalFAF_(f,w)))_._v
let v be Vector of W; ::_thesis: (FunctionalFAF ((a * f),w)) . v = (a * (FunctionalFAF (f,w))) . v
thus (FunctionalFAF ((a * f),w)) . v = (a * f) . (w,v) by Th8
.= a * (f . (w,v)) by Def3
.= a * ((FunctionalFAF (f,w)) . v) by Th8
.= (a * (FunctionalFAF (f,w))) . v by HAHNBAN1:def_6 ; ::_thesis: verum
end;
hence  FunctionalFAF ((a * f),w) = a * (FunctionalFAF (f,w)) by FUNCT_2:63; ::_thesis: verum
end;

theorem Th16: :: BILINEAR:16
for K being non empty addLoopStr
for V, W being non empty VectSpStr over K
for f being Form of V,W
for w being Vector of W holds FunctionalSAF ((- f),w) = - (FunctionalSAF (f,w))
proof
let K be non empty addLoopStr ; ::_thesis: for V, W being non empty VectSpStr over K
for f being Form of V,W
for w being Vector of W holds FunctionalSAF ((- f),w) = - (FunctionalSAF (f,w))
let V, W be non empty VectSpStr over K; ::_thesis: for f being Form of V,W
for w being Vector of W holds FunctionalSAF ((- f),w) = - (FunctionalSAF (f,w))
let f be Form of V,W; ::_thesis: for w being Vector of W holds FunctionalSAF ((- f),w) = - (FunctionalSAF (f,w))
let w be Vector of W; ::_thesis: FunctionalSAF ((- f),w) = - (FunctionalSAF (f,w))
now__::_thesis:_for_v_being_Vector_of_V_holds_(FunctionalSAF_((-_f),w))_._v_=_(-_(FunctionalSAF_(f,w)))_._v
let v be Vector of V; ::_thesis: (FunctionalSAF ((- f),w)) . v = (- (FunctionalSAF (f,w))) . v
thus (FunctionalSAF ((- f),w)) . v = (- f) . (v,w) by Th9
.= - (f . (v,w)) by Def4
.= - ((FunctionalSAF (f,w)) . v) by Th9
.= (- (FunctionalSAF (f,w))) . v by HAHNBAN1:def_4 ; ::_thesis: verum
end;
hence  FunctionalSAF ((- f),w) = - (FunctionalSAF (f,w)) by FUNCT_2:63; ::_thesis: verum
end;

theorem Th17: :: BILINEAR:17
for K being non empty addLoopStr
for V, W being non empty VectSpStr over K
for f being Form of V,W
for v being Vector of V holds FunctionalFAF ((- f),v) = - (FunctionalFAF (f,v))
proof
let K be non empty addLoopStr ; ::_thesis: for V, W being non empty VectSpStr over K
for f being Form of V,W
for v being Vector of V holds FunctionalFAF ((- f),v) = - (FunctionalFAF (f,v))
let V, W be non empty VectSpStr over K; ::_thesis: for f being Form of V,W
for v being Vector of V holds FunctionalFAF ((- f),v) = - (FunctionalFAF (f,v))
let f be Form of V,W; ::_thesis: for v being Vector of V holds FunctionalFAF ((- f),v) = - (FunctionalFAF (f,v))
let w be Vector of V; ::_thesis: FunctionalFAF ((- f),w) = - (FunctionalFAF (f,w))
now__::_thesis:_for_v_being_Vector_of_W_holds_(FunctionalFAF_((-_f),w))_._v_=_(-_(FunctionalFAF_(f,w)))_._v
let v be Vector of W; ::_thesis: (FunctionalFAF ((- f),w)) . v = (- (FunctionalFAF (f,w))) . v
thus (FunctionalFAF ((- f),w)) . v = (- f) . (w,v) by Th8
.= - (f . (w,v)) by Def4
.= - ((FunctionalFAF (f,w)) . v) by Th8
.= (- (FunctionalFAF (f,w))) . v by HAHNBAN1:def_4 ; ::_thesis: verum
end;
hence  FunctionalFAF ((- f),w) = - (FunctionalFAF (f,w)) by FUNCT_2:63; ::_thesis: verum
end;

theorem :: BILINEAR:18
for K being non empty addLoopStr
for V, W being non empty VectSpStr over K
for f, g being Form of V,W
for w being Vector of W holds FunctionalSAF ((f - g),w) = (FunctionalSAF (f,w)) - (FunctionalSAF (g,w))
proof
let K be non empty addLoopStr ; ::_thesis: for V, W being non empty VectSpStr over K
for f, g being Form of V,W
for w being Vector of W holds FunctionalSAF ((f - g),w) = (FunctionalSAF (f,w)) - (FunctionalSAF (g,w))
let V, W be non empty VectSpStr over K; ::_thesis: for f, g being Form of V,W
for w being Vector of W holds FunctionalSAF ((f - g),w) = (FunctionalSAF (f,w)) - (FunctionalSAF (g,w))
let f, g be Form of V,W; ::_thesis: for w being Vector of W holds FunctionalSAF ((f - g),w) = (FunctionalSAF (f,w)) - (FunctionalSAF (g,w))
let w be Vector of W; ::_thesis: FunctionalSAF ((f - g),w) = (FunctionalSAF (f,w)) - (FunctionalSAF (g,w))
now__::_thesis:_for_v_being_Vector_of_V_holds_(FunctionalSAF_((f_-_g),w))_._v_=_((FunctionalSAF_(f,w))_-_(FunctionalSAF_(g,w)))_._v
let v be Vector of V; ::_thesis: (FunctionalSAF ((f - g),w)) . v = ((FunctionalSAF (f,w)) - (FunctionalSAF (g,w))) . v
thus (FunctionalSAF ((f - g),w)) . v = (f - g) . (v,w) by Th9
.= (f . (v,w)) - (g . (v,w)) by Def7
.= ((FunctionalSAF (f,w)) . v) - (g . (v,w)) by Th9
.= ((FunctionalSAF (f,w)) . v) - ((FunctionalSAF (g,w)) . v) by Th9
.= ((FunctionalSAF (f,w)) . v) + (- ((FunctionalSAF (g,w)) . v)) by RLVECT_1:def_11
.= ((FunctionalSAF (f,w)) . v) + ((- (FunctionalSAF (g,w))) . v) by HAHNBAN1:def_4
.= ((FunctionalSAF (f,w)) - (FunctionalSAF (g,w))) . v by HAHNBAN1:def_3 ; ::_thesis: verum
end;
hence  FunctionalSAF ((f - g),w) = (FunctionalSAF (f,w)) - (FunctionalSAF (g,w)) by FUNCT_2:63; ::_thesis: verum
end;

theorem :: BILINEAR:19
for K being non empty addLoopStr
for V, W being non empty VectSpStr over K
for f, g being Form of V,W
for v being Vector of V holds FunctionalFAF ((f - g),v) = (FunctionalFAF (f,v)) - (FunctionalFAF (g,v))
proof
let K be non empty addLoopStr ; ::_thesis: for V, W being non empty VectSpStr over K
for f, g being Form of V,W
for v being Vector of V holds FunctionalFAF ((f - g),v) = (FunctionalFAF (f,v)) - (FunctionalFAF (g,v))
let V, W be non empty VectSpStr over K; ::_thesis: for f, g being Form of V,W
for v being Vector of V holds FunctionalFAF ((f - g),v) = (FunctionalFAF (f,v)) - (FunctionalFAF (g,v))
let f, g be Form of V,W; ::_thesis: for v being Vector of V holds FunctionalFAF ((f - g),v) = (FunctionalFAF (f,v)) - (FunctionalFAF (g,v))
let w be Vector of V; ::_thesis: FunctionalFAF ((f - g),w) = (FunctionalFAF (f,w)) - (FunctionalFAF (g,w))
now__::_thesis:_for_v_being_Vector_of_W_holds_(FunctionalFAF_((f_-_g),w))_._v_=_((FunctionalFAF_(f,w))_-_(FunctionalFAF_(g,w)))_._v
let v be Vector of W; ::_thesis: (FunctionalFAF ((f - g),w)) . v = ((FunctionalFAF (f,w)) - (FunctionalFAF (g,w))) . v
thus (FunctionalFAF ((f - g),w)) . v = (f - g) . (w,v) by Th8
.= (f . (w,v)) - (g . (w,v)) by Def7
.= ((FunctionalFAF (f,w)) . v) - (g . (w,v)) by Th8
.= ((FunctionalFAF (f,w)) . v) - ((FunctionalFAF (g,w)) . v) by Th8
.= ((FunctionalFAF (f,w)) . v) + (- ((FunctionalFAF (g,w)) . v)) by RLVECT_1:def_11
.= ((FunctionalFAF (f,w)) . v) + ((- (FunctionalFAF (g,w))) . v) by HAHNBAN1:def_4
.= ((FunctionalFAF (f,w)) - (FunctionalFAF (g,w))) . v by HAHNBAN1:def_3 ; ::_thesis: verum
end;
hence  FunctionalFAF ((f - g),w) = (FunctionalFAF (f,w)) - (FunctionalFAF (g,w)) by FUNCT_2:63; ::_thesis: verum
end;

begin

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 :Def10: :: BILINEAR:def 10
 for v being Vector of V
for w being Vector of W holds it . (v,w) = (f . v) * (g . w);
existence
 ex b1 being Form of V,W st
for v being Vector of V
for w being Vector of W holds b1 . (v,w) = (f . v) * (g . w)
proof
deffunc H1( Vector of V, Vector of W) ->  Element of the carrier of K = (f . $1) * (g . $2);
set c1 = the carrier of V;
set c2 = the carrier of W;
set k = the carrier of K;
consider i being Function of [: the carrier of V, the carrier of W:], the carrier of K such that
A1: for x being Element of the carrier of V
for y being Element of the carrier of W holds i . (x,y) = H1(x,y) from BINOP_1:sch_4();
reconsider i = i as Form of V,W ;
take  i ; ::_thesis: for v being Vector of V
for w being Vector of W holds i . (v,w) = (f . v) * (g . w)
thus  for v being Vector of V
for w being Vector of W holds i . (v,w) = (f . v) * (g . w) by A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Form of V,W st ( for v being Vector of V
for w being Vector of W holds b1 . (v,w) = (f . v) * (g . w) ) & ( for v being Vector of V
for w being Vector of W holds b2 . (v,w) = (f . v) * (g . w) ) holds
b1 = b2
proof
let F1, F2 be Form of V,W; ::_thesis: ( ( for v being Vector of V
for w being Vector of W holds F1 . (v,w) = (f . v) * (g . w) ) & ( for v being Vector of V
for w being Vector of W holds F2 . (v,w) = (f . v) * (g . w) ) implies F1 = F2 )
assume that
A2: for v being Vector of V
for y being Vector of W holds F1 . (v,y) = (f . v) * (g . y) and
A3: for v being Vector of V
for y being Vector of W holds F2 . (v,y) = (f . v) * (g . y) ; ::_thesis: F1 = F2
now__::_thesis:_for_v_being_Vector_of_V
for_y_being_Vector_of_W_holds_F1_._(v,y)_=_F2_._(v,y)
let v be Vector of V; ::_thesis: for y being Vector of W holds F1 . (v,y) = F2 . (v,y)
let y be Vector of W; ::_thesis: F1 . (v,y) = F2 . (v,y)
thus F1 . (v,y) = (f . v) * (g . y) by A2
.= F2 . (v,y) by A3 ; ::_thesis: verum
end;
hence  F1 = F2 by BINOP_1:2; ::_thesis: verum
end;
end;

:: deftheorem Def10 defines FormFunctional BILINEAR:def_10_:_
 for K being non empty multMagma
for V, W being non empty VectSpStr over K
for f being Functional of V
for g being Functional of W
for b6 being Form of V,W holds
( b6 = FormFunctional (f,g) iff for v being Vector of V
for w being Vector of W holds b6 . (v,w) = (f . v) * (g . w) );

theorem Th20: :: BILINEAR:20
for K being non empty right_complementable add-associative right_zeroed right-distributive doubleLoopStr
for V, W being non empty VectSpStr over K
for f being Functional of V
for v being Vector of V
for w being Vector of W holds (FormFunctional (f,(0Functional W))) . (v,w) = 0. K
proof
let K be non empty right_complementable add-associative right_zeroed right-distributive doubleLoopStr ; ::_thesis: for V, W being non empty VectSpStr over K
for f being Functional of V
for v being Vector of V
for w being Vector of W holds (FormFunctional (f,(0Functional W))) . (v,w) = 0. K
let V, W be non empty VectSpStr over K; ::_thesis: for f being Functional of V
for v being Vector of V
for w being Vector of W holds (FormFunctional (f,(0Functional W))) . (v,w) = 0. K
let f be Functional of V; ::_thesis: for v being Vector of V
for w being Vector of W holds (FormFunctional (f,(0Functional W))) . (v,w) = 0. K
let v be Vector of V; ::_thesis: for w being Vector of W holds (FormFunctional (f,(0Functional W))) . (v,w) = 0. K
let y be Vector of W; ::_thesis: (FormFunctional (f,(0Functional W))) . (v,y) = 0. K
set 0F = 0Functional W;
set F = FormFunctional (f,(0Functional W));
thus (FormFunctional (f,(0Functional W))) . (v,y) = (f . v) * ((0Functional W) . y) by Def10
.= (f . v) * (0. K) by FUNCOP_1:7
.= 0. K by VECTSP_1:6 ; ::_thesis: verum
end;

theorem Th21: :: BILINEAR:21
for K being non empty right_complementable add-associative right_zeroed left-distributive doubleLoopStr
for V, W being non empty VectSpStr over K
for g being Functional of W
for v being Vector of V
for w being Vector of W holds (FormFunctional ((0Functional V),g)) . (v,w) = 0. K
proof
let K be non empty right_complementable add-associative right_zeroed left-distributive doubleLoopStr ; ::_thesis: for V, W being non empty VectSpStr over K
for g being Functional of W
for v being Vector of V
for w being Vector of W holds (FormFunctional ((0Functional V),g)) . (v,w) = 0. K
let V, W be non empty VectSpStr over K; ::_thesis: for g being Functional of W
for v being Vector of V
for w being Vector of W holds (FormFunctional ((0Functional V),g)) . (v,w) = 0. K
let h be Functional of W; ::_thesis: for v being Vector of V
for w being Vector of W holds (FormFunctional ((0Functional V),h)) . (v,w) = 0. K
let v be Vector of V; ::_thesis: for w being Vector of W holds (FormFunctional ((0Functional V),h)) . (v,w) = 0. K
let y be Vector of W; ::_thesis: (FormFunctional ((0Functional V),h)) . (v,y) = 0. K
set 0F = 0Functional V;
set F = FormFunctional ((0Functional V),h);
thus (FormFunctional ((0Functional V),h)) . (v,y) = ((0Functional V) . v) * (h . y) by Def10
.= (0. K) * (h . y) by FUNCOP_1:7
.= 0. K by VECTSP_1:7 ; ::_thesis: verum
end;

theorem :: BILINEAR:22
for K being non empty right_complementable add-associative right_zeroed right-distributive doubleLoopStr
for V, W being non empty VectSpStr over K
for f being Functional of V holds FormFunctional (f,(0Functional W)) = NulForm (V,W)
proof
let K be non empty right_complementable add-associative right_zeroed right-distributive doubleLoopStr ; ::_thesis: for V, W being non empty VectSpStr over K
for f being Functional of V holds FormFunctional (f,(0Functional W)) = NulForm (V,W)
let V, W be non empty VectSpStr over K; ::_thesis: for f being Functional of V holds FormFunctional (f,(0Functional W)) = NulForm (V,W)
let f be Functional of V; ::_thesis: FormFunctional (f,(0Functional W)) = NulForm (V,W)
now__::_thesis:_for_v_being_Vector_of_V
for_y_being_Vector_of_W_holds_(FormFunctional_(f,(0Functional_W)))_._(v,y)_=_(NulForm_(V,W))_._(v,y)
let v be Vector of V; ::_thesis: for y being Vector of W holds (FormFunctional (f,(0Functional W))) . (v,y) = (NulForm (V,W)) . (v,y)
let y be Vector of W; ::_thesis: (FormFunctional (f,(0Functional W))) . (v,y) = (NulForm (V,W)) . (v,y)
thus (FormFunctional (f,(0Functional W))) . (v,y) = 0. K by Th20
.= (NulForm (V,W)) . (v,y) by FUNCOP_1:70 ; ::_thesis: verum
end;
hence  FormFunctional (f,(0Functional W)) = NulForm (V,W) by BINOP_1:2; ::_thesis: verum
end;

theorem :: BILINEAR:23
for K being non empty right_complementable add-associative right_zeroed left-distributive doubleLoopStr
for V, W being non empty VectSpStr over K
for g being Functional of W holds FormFunctional ((0Functional V),g) = NulForm (V,W)
proof
let K be non empty right_complementable add-associative right_zeroed left-distributive doubleLoopStr ; ::_thesis: for V, W being non empty VectSpStr over K
for g being Functional of W holds FormFunctional ((0Functional V),g) = NulForm (V,W)
let V, W be non empty VectSpStr over K; ::_thesis: for g being Functional of W holds FormFunctional ((0Functional V),g) = NulForm (V,W)
let h be Functional of W; ::_thesis: FormFunctional ((0Functional V),h) = NulForm (V,W)
now__::_thesis:_for_v_being_Vector_of_V
for_y_being_Vector_of_W_holds_(FormFunctional_((0Functional_V),h))_._(v,y)_=_(NulForm_(V,W))_._(v,y)
let v be Vector of V; ::_thesis: for y being Vector of W holds (FormFunctional ((0Functional V),h)) . (v,y) = (NulForm (V,W)) . (v,y)
let y be Vector of W; ::_thesis: (FormFunctional ((0Functional V),h)) . (v,y) = (NulForm (V,W)) . (v,y)
thus (FormFunctional ((0Functional V),h)) . (v,y) = 0. K by Th21
.= (NulForm (V,W)) . (v,y) by FUNCOP_1:70 ; ::_thesis: verum
end;
hence  FormFunctional ((0Functional V),h) = NulForm (V,W) by BINOP_1:2; ::_thesis: verum
end;

theorem Th24: :: BILINEAR:24
for K being non empty multMagma
for V, W being non empty VectSpStr over K
for f being Functional of V
for g being Functional of W
for v being Vector of V holds FunctionalFAF ((FormFunctional (f,g)),v) = (f . v) * g
proof
let K be non empty multMagma ; ::_thesis: for V, W being non empty VectSpStr over K
for f being Functional of V
for g being Functional of W
for v being Vector of V holds FunctionalFAF ((FormFunctional (f,g)),v) = (f . v) * g
let V, W be non empty VectSpStr over K; ::_thesis: for f being Functional of V
for g being Functional of W
for v being Vector of V holds FunctionalFAF ((FormFunctional (f,g)),v) = (f . v) * g
let f be Functional of V; ::_thesis: for g being Functional of W
for v being Vector of V holds FunctionalFAF ((FormFunctional (f,g)),v) = (f . v) * g
let h be Functional of W; ::_thesis: for v being Vector of V holds FunctionalFAF ((FormFunctional (f,h)),v) = (f . v) * h
let v be Vector of V; ::_thesis: FunctionalFAF ((FormFunctional (f,h)),v) = (f . v) * h
set F = FormFunctional (f,h);
set FF = FunctionalFAF ((FormFunctional (f,h)),v);
now__::_thesis:_for_y_being_Vector_of_W_holds_(FunctionalFAF_((FormFunctional_(f,h)),v))_._y_=_((f_._v)_*_h)_._y
let y be Vector of W; ::_thesis: (FunctionalFAF ((FormFunctional (f,h)),v)) . y = ((f . v) * h) . y
thus (FunctionalFAF ((FormFunctional (f,h)),v)) . y = (FormFunctional (f,h)) . (v,y) by Th8
.= (f . v) * (h . y) by Def10
.= ((f . v) * h) . y by HAHNBAN1:def_6 ; ::_thesis: verum
end;
hence  FunctionalFAF ((FormFunctional (f,h)),v) = (f . v) * h by FUNCT_2:63; ::_thesis: verum
end;

theorem Th25: :: BILINEAR:25
for K being non empty commutative multMagma
for V, W being non empty VectSpStr over K
for f being Functional of V
for g being Functional of W
for w being Vector of W holds FunctionalSAF ((FormFunctional (f,g)),w) = (g . w) * f
proof
let K be non empty commutative multMagma ; ::_thesis: for V, W being non empty VectSpStr over K
for f being Functional of V
for g being Functional of W
for w being Vector of W holds FunctionalSAF ((FormFunctional (f,g)),w) = (g . w) * f
let V, W be non empty VectSpStr over K; ::_thesis: for f being Functional of V
for g being Functional of W
for w being Vector of W holds FunctionalSAF ((FormFunctional (f,g)),w) = (g . w) * f
let f be Functional of V; ::_thesis: for g being Functional of W
for w being Vector of W holds FunctionalSAF ((FormFunctional (f,g)),w) = (g . w) * f
let h be Functional of W; ::_thesis: for w being Vector of W holds FunctionalSAF ((FormFunctional (f,h)),w) = (h . w) * f
let y be Vector of W; ::_thesis: FunctionalSAF ((FormFunctional (f,h)),y) = (h . y) * f
set F = FormFunctional (f,h);
set FF = FunctionalSAF ((FormFunctional (f,h)),y);
now__::_thesis:_for_v_being_Vector_of_V_holds_(FunctionalSAF_((FormFunctional_(f,h)),y))_._v_=_((h_._y)_*_f)_._v
let v be Vector of V; ::_thesis: (FunctionalSAF ((FormFunctional (f,h)),y)) . v = ((h . y) * f) . v
thus (FunctionalSAF ((FormFunctional (f,h)),y)) . v = (FormFunctional (f,h)) . (v,y) by Th9
.= (f . v) * (h . y) by Def10
.= ((h . y) * f) . v by HAHNBAN1:def_6 ; ::_thesis: verum
end;
hence  FunctionalSAF ((FormFunctional (f,h)),y) = (h . y) * f by FUNCT_2:63; ::_thesis: verum
end;

begin

definition
let K be non empty addLoopStr ;
let V, W be non empty VectSpStr over K;
let f be Form of V,W;
attrf is additiveFAF  means :Def11: :: BILINEAR:def 11
 for v being Vector of V holds FunctionalFAF (f,v) is additive ;
attrf is additiveSAF  means :Def12: :: BILINEAR:def 12
 for w being Vector of W holds FunctionalSAF (f,w) is additive ;
end;

:: deftheorem Def11 defines additiveFAF BILINEAR:def_11_:_
 for K being non empty addLoopStr
for V, W being non empty VectSpStr over K
for f being Form of V,W holds
( f is additiveFAF iff for v being Vector of V holds FunctionalFAF (f,v) is additive );

:: deftheorem Def12 defines additiveSAF BILINEAR:def_12_:_
 for K being non empty addLoopStr
for V, W being non empty VectSpStr over K
for f being Form of V,W holds
( f is additiveSAF iff for w being Vector of W holds FunctionalSAF (f,w) is additive );

definition
let K be non empty multMagma ;
let V, W be non empty VectSpStr over K;
let f be Form of V,W;
attrf is homogeneousFAF  means :Def13: :: BILINEAR:def 13
 for v being Vector of V holds FunctionalFAF (f,v) is homogeneous ;
attrf is homogeneousSAF  means :Def14: :: BILINEAR:def 14
 for w being Vector of W holds FunctionalSAF (f,w) is homogeneous ;
end;

:: deftheorem Def13 defines homogeneousFAF BILINEAR:def_13_:_
 for K being non empty multMagma
for V, W being non empty VectSpStr over K
for f being Form of V,W holds
( f is homogeneousFAF iff for v being Vector of V holds FunctionalFAF (f,v) is homogeneous );

:: deftheorem Def14 defines homogeneousSAF BILINEAR:def_14_:_
 for K being non empty multMagma
for V, W being non empty VectSpStr over K
for f being Form of V,W holds
( f is homogeneousSAF iff for w being Vector of W holds FunctionalSAF (f,w) is homogeneous );

registration
let K be non empty right_zeroed addLoopStr ;
let V, W be non empty VectSpStr over K;
cluster NulForm (V,W) ->  additiveFAF ;
coherence
 NulForm (V,W) is additiveFAF
proof
let v be Vector of V; :: according to BILINEAR:def_11 ::_thesis: FunctionalFAF ((NulForm (V,W)),v) is additive
 FunctionalFAF ((NulForm (V,W)),v) = 0Functional W by Th10;
hence  FunctionalFAF ((NulForm (V,W)),v) is additive ; ::_thesis: verum
end;
cluster NulForm (V,W) ->  additiveSAF ;
coherence
 NulForm (V,W) is additiveSAF
proof
let y be Vector of W; :: according to BILINEAR:def_12 ::_thesis: FunctionalSAF ((NulForm (V,W)),y) is additive
 FunctionalSAF ((NulForm (V,W)),y) = 0Functional V by Th11;
hence  FunctionalSAF ((NulForm (V,W)),y) is additive ; ::_thesis: verum
end;
end;

registration
let K be non empty right_zeroed addLoopStr ;
let V, W be non empty VectSpStr over K;
cluster non empty Relation-like [: the carrier of V, the carrier of W:] -defined the carrier of K -valued Function-like V20([: the carrier of V, the carrier of W:]) V21([: the carrier of V, the carrier of W:], the carrier of K) additiveFAF additiveSAF for Element of bool [:[: the carrier of V, the carrier of W:], the carrier of K:];
existence
 ex b1 being Form of V,W st
( b1 is additiveFAF & b1 is additiveSAF )
proof
take  NulForm (V,W) ; ::_thesis: ( NulForm (V,W) is additiveFAF & NulForm (V,W) is additiveSAF )
thus  ( NulForm (V,W) is additiveFAF & NulForm (V,W) is additiveSAF ) ; ::_thesis: verum
end;
end;

registration
let K be non empty right_complementable add-associative right_zeroed right-distributive doubleLoopStr ;
let V, W be non empty VectSpStr over K;
cluster NulForm (V,W) ->  homogeneousFAF ;
coherence
 NulForm (V,W) is homogeneousFAF
proof
let v be Vector of V; :: according to BILINEAR:def_13 ::_thesis: FunctionalFAF ((NulForm (V,W)),v) is homogeneous
 FunctionalFAF ((NulForm (V,W)),v) = 0Functional W by Th10;
hence  FunctionalFAF ((NulForm (V,W)),v) is homogeneous ; ::_thesis: verum
end;
cluster NulForm (V,W) ->  homogeneousSAF ;
coherence
 NulForm (V,W) is homogeneousSAF
proof
let y be Vector of W; :: according to BILINEAR:def_14 ::_thesis: FunctionalSAF ((NulForm (V,W)),y) is homogeneous
 FunctionalSAF ((NulForm (V,W)),y) = 0Functional V by Th11;
hence  FunctionalSAF ((NulForm (V,W)),y) is homogeneous ; ::_thesis: verum
end;
end;

registration
let K be non empty right_complementable add-associative right_zeroed right-distributive doubleLoopStr ;
let V, W be non empty VectSpStr over K;
cluster non empty Relation-like [: the carrier of V, the carrier of W:] -defined the carrier of K -valued Function-like V20([: the carrier of V, the carrier of W:]) V21([: the carrier of V, the carrier of W:], the carrier of K) additiveFAF additiveSAF homogeneousFAF homogeneousSAF for Element of bool [:[: the carrier of V, the carrier of W:], the carrier of K:];
existence
 ex b1 being Form of V,W st
( b1 is additiveFAF & b1 is homogeneousFAF & b1 is additiveSAF & b1 is homogeneousSAF )
proof
take  NulForm (V,W) ; ::_thesis: ( NulForm (V,W) is additiveFAF & NulForm (V,W) is homogeneousFAF & NulForm (V,W) is additiveSAF & NulForm (V,W) is homogeneousSAF )
thus  ( NulForm (V,W) is additiveFAF & NulForm (V,W) is homogeneousFAF & NulForm (V,W) is additiveSAF & NulForm (V,W) is homogeneousSAF ) ; ::_thesis: verum
end;
end;

definition
let K be non empty right_complementable add-associative right_zeroed right-distributive doubleLoopStr ;
let V, W be non empty VectSpStr over K;
mode bilinear-Form of V,W is additiveFAF additiveSAF homogeneousFAF homogeneousSAF Form of V,W;
end;

registration
let K be non empty right_complementable add-associative right_zeroed right-distributive doubleLoopStr ;
let V, W be non empty VectSpStr over K;
let f be additiveFAF Form of V,W;
let v be Vector of V;
cluster FunctionalFAF (f,v) ->  additive ;
coherence
 FunctionalFAF (f,v) is additive by Def11;
end;

registration
let K be non empty right_complementable add-associative right_zeroed right-distributive doubleLoopStr ;
let V, W be non empty VectSpStr over K;
let f be additiveSAF Form of V,W;
let w be Vector of W;
cluster FunctionalSAF (f,w) ->  additive ;
coherence
 FunctionalSAF (f,w) is additive by Def12;
end;

registration
let K be non empty right_complementable add-associative right_zeroed right-distributive doubleLoopStr ;
let V, W be non empty VectSpStr over K;
let f be homogeneousFAF Form of V,W;
let v be Vector of V;
cluster FunctionalFAF (f,v) ->  homogeneous ;
coherence
 FunctionalFAF (f,v) is homogeneous by Def13;
end;

registration
let K be non empty right_complementable add-associative right_zeroed right-distributive doubleLoopStr ;
let V, W be non empty VectSpStr over K;
let f be homogeneousSAF Form of V,W;
let w be Vector of W;
cluster FunctionalSAF (f,w) ->  homogeneous ;
coherence
 FunctionalSAF (f,w) is homogeneous by Def14;
end;

registration
let K be non empty right_complementable add-associative right_zeroed right-distributive doubleLoopStr ;
let V, W be non empty VectSpStr over K;
let f be Functional of V;
let g be additive Functional of W;
cluster FormFunctional (f,g) ->  additiveFAF ;
coherence
 FormFunctional (f,g) is additiveFAF
proof
let v be Vector of V; :: according to BILINEAR:def_11 ::_thesis: FunctionalFAF ((FormFunctional (f,g)),v) is additive
set fg = FormFunctional (f,g);
set F = FunctionalFAF ((FormFunctional (f,g)),v);
let y, y9 be Vector of W; :: according to VECTSP_1:def_20 ::_thesis: (FunctionalFAF ((FormFunctional (f,g)),v)) . (y + y9) = ((FunctionalFAF ((FormFunctional (f,g)),v)) . y) + ((FunctionalFAF ((FormFunctional (f,g)),v)) . y9)
A1: FunctionalFAF ((FormFunctional (f,g)),v) = (f . v) * g by Th24;
hence (FunctionalFAF ((FormFunctional (f,g)),v)) . (y + y9) = (f . v) * (g . (y + y9)) by HAHNBAN1:def_6
.= (f . v) * ((g . y) + (g . y9)) by VECTSP_1:def_20
.= ((f . v) * (g . y)) + ((f . v) * (g . y9)) by VECTSP_1:def_2
.= ((f . v) * (g . y)) + ((FunctionalFAF ((FormFunctional (f,g)),v)) . y9) by A1, HAHNBAN1:def_6
.= ((FunctionalFAF ((FormFunctional (f,g)),v)) . y) + ((FunctionalFAF ((FormFunctional (f,g)),v)) . y9) by A1, HAHNBAN1:def_6 ;
::_thesis: verum
end;
end;

registration
let K be non empty right_complementable add-associative right_zeroed commutative right-distributive doubleLoopStr ;
let V, W be non empty VectSpStr over K;
let f be additive Functional of V;
let g be Functional of W;
cluster FormFunctional (f,g) ->  additiveSAF ;
coherence
 FormFunctional (f,g) is additiveSAF
proof
let y be Vector of W; :: according to BILINEAR:def_12 ::_thesis: FunctionalSAF ((FormFunctional (f,g)),y) is additive
set fg = FormFunctional (f,g);
set F = FunctionalSAF ((FormFunctional (f,g)),y);
 FunctionalSAF ((FormFunctional (f,g)),y) = (g . y) * f by Th25;
hence  FunctionalSAF ((FormFunctional (f,g)),y) is additive ; ::_thesis: verum
end;
end;

registration
let K be non empty right_complementable add-associative right_zeroed associative commutative right-distributive doubleLoopStr ;
let V, W be non empty VectSpStr over K;
let f be Functional of V;
let g be homogeneous Functional of W;
cluster FormFunctional (f,g) ->  homogeneousFAF ;
coherence
 FormFunctional (f,g) is homogeneousFAF
proof
let v be Vector of V; :: according to BILINEAR:def_13 ::_thesis: FunctionalFAF ((FormFunctional (f,g)),v) is homogeneous
set fg = FormFunctional (f,g);
set F = FunctionalFAF ((FormFunctional (f,g)),v);
let y be Vector of W; :: according to HAHNBAN1:def_8 ::_thesis: for b1 being Element of the carrier of K holds (FunctionalFAF ((FormFunctional (f,g)),v)) . (b1 * y) = b1 * ((FunctionalFAF ((FormFunctional (f,g)),v)) . y)
let r be Scalar of ; ::_thesis: (FunctionalFAF ((FormFunctional (f,g)),v)) . (r * y) = r * ((FunctionalFAF ((FormFunctional (f,g)),v)) . y)
A1: FunctionalFAF ((FormFunctional (f,g)),v) = (f . v) * g by Th24;
hence (FunctionalFAF ((FormFunctional (f,g)),v)) . (r * y) = (f . v) * (g . (r * y)) by HAHNBAN1:def_6
.= (f . v) * (r * (g . y)) by HAHNBAN1:def_8
.= r * ((f . v) * (g . y)) by GROUP_1:def_3
.= r * ((FunctionalFAF ((FormFunctional (f,g)),v)) . y) by A1, HAHNBAN1:def_6 ;
::_thesis: verum
end;
end;

registration
let K be non empty right_complementable add-associative right_zeroed associative commutative right-distributive doubleLoopStr ;
let V, W be non empty VectSpStr over K;
let f be homogeneous Functional of V;
let g be Functional of W;
cluster FormFunctional (f,g) ->  homogeneousSAF ;
coherence
 FormFunctional (f,g) is homogeneousSAF
proof
let y be Vector of W; :: according to BILINEAR:def_14 ::_thesis: FunctionalSAF ((FormFunctional (f,g)),y) is homogeneous
set fg = FormFunctional (f,g);
set F = FunctionalSAF ((FormFunctional (f,g)),y);
let v be Vector of V; :: according to HAHNBAN1:def_8 ::_thesis: for b1 being Element of the carrier of K holds (FunctionalSAF ((FormFunctional (f,g)),y)) . (b1 * v) = b1 * ((FunctionalSAF ((FormFunctional (f,g)),y)) . v)
let r be Scalar of ; ::_thesis: (FunctionalSAF ((FormFunctional (f,g)),y)) . (r * v) = r * ((FunctionalSAF ((FormFunctional (f,g)),y)) . v)
A1: FunctionalSAF ((FormFunctional (f,g)),y) = (g . y) * f by Th25;
hence (FunctionalSAF ((FormFunctional (f,g)),y)) . (r * v) = (g . y) * (f . (r * v)) by HAHNBAN1:def_6
.= (g . y) * (r * (f . v)) by HAHNBAN1:def_8
.= r * ((g . y) * (f . v)) by GROUP_1:def_3
.= r * ((FunctionalSAF ((FormFunctional (f,g)),y)) . v) by A1, HAHNBAN1:def_6 ;
::_thesis: verum
end;
end;

registration
let K be non empty non degenerated doubleLoopStr ;
let V be non trivial VectSpStr over K;
let W be non empty VectSpStr over K;
let f be Functional of V;
let g be Functional of W;
cluster FormFunctional (f,g) ->  non trivial ;
coherence
 not FormFunctional (f,g) is trivial
proof
set fg = FormFunctional (f,g);
set w = the Vector of W;
consider v being Vector of V such that
A1: v <> 0. V by STRUCT_0:def_18;
A2: [(0. V),(0. W)] <> [v, the Vector of W] by A1, XTUPLE_0:1;
 dom (FormFunctional (f,g)) = [: the carrier of V, the carrier of W:] by FUNCT_2:def_1;
then A3: ( [[(0. V),(0. W)],((FormFunctional (f,g)) . ((0. V),(0. W)))] in FormFunctional (f,g) & [[v, the Vector of W],((FormFunctional (f,g)) . (v, the Vector of W))] in FormFunctional (f,g) ) by FUNCT_1:1;
assume A4: FormFunctional (f,g) is trivial ; ::_thesis: contradiction
percases ( FormFunctional (f,g) = {} or ex x being set st FormFunctional (f,g) = {x} ) by A4, ZFMISC_1:131;
suppose FormFunctional (f,g) = {} ; ::_thesis: contradiction
hence  contradiction ; ::_thesis: verum
end;
suppose ex x being set st FormFunctional (f,g) = {x} ; ::_thesis: contradiction
then consider x being set  such that
A5: FormFunctional (f,g) = {x} ;
 ( [[(0. V),(0. W)],((FormFunctional (f,g)) . ((0. V),(0. W)))] = x & x = [[v, the Vector of W],((FormFunctional (f,g)) . (v, the Vector of W))] ) by A3, A5, TARSKI:def_1;
hence  contradiction by A2, XTUPLE_0:1; ::_thesis: verum
end;
end;
end;
end;

registration
let K be non empty non degenerated doubleLoopStr ;
let V be non empty VectSpStr over K;
let W be non trivial VectSpStr over K;
let f be Functional of V;
let g be Functional of W;
cluster FormFunctional (f,g) ->  non trivial ;
coherence
 not FormFunctional (f,g) is trivial
proof
set fg = FormFunctional (f,g);
set v = the Vector of V;
consider w being Vector of W such that
A1: w <> 0. W by STRUCT_0:def_18;
A2: [(0. V),(0. W)] <> [ the Vector of V,w] by A1, XTUPLE_0:1;
 dom (FormFunctional (f,g)) = [: the carrier of V, the carrier of W:] by FUNCT_2:def_1;
then A3: ( [[(0. V),(0. W)],((FormFunctional (f,g)) . ((0. V),(0. W)))] in FormFunctional (f,g) & [[ the Vector of V,w],((FormFunctional (f,g)) . ( the Vector of V,w))] in FormFunctional (f,g) ) by FUNCT_1:1;
assume A4: FormFunctional (f,g) is trivial ; ::_thesis: contradiction
percases ( FormFunctional (f,g) = {} or ex x being set st FormFunctional (f,g) = {x} ) by A4, ZFMISC_1:131;
suppose FormFunctional (f,g) = {} ; ::_thesis: contradiction
hence  contradiction ; ::_thesis: verum
end;
suppose ex x being set st FormFunctional (f,g) = {x} ; ::_thesis: contradiction
then consider x being set  such that
A5: FormFunctional (f,g) = {x} ;
 ( [[(0. V),(0. W)],((FormFunctional (f,g)) . ((0. V),(0. W)))] = x & x = [[ the Vector of V,w],((FormFunctional (f,g)) . ( the Vector of V,w))] ) by A3, A5, TARSKI:def_1;
hence  contradiction by A2, XTUPLE_0:1; ::_thesis: verum
end;
end;
end;
end;

registration
let K be Field;
let V, W be non trivial VectSp of K;
let f be V17() 0-preserving Functional of V;
let g be V17() 0-preserving Functional of W;
cluster FormFunctional (f,g) ->  non constant ;
coherence
 not FormFunctional (f,g) is constant
proof
set fg = FormFunctional (f,g);
consider v being Vector of V such that
 v <> 0. V and
A1: f . v <> 0. K by VECTSP10:28;
consider w being Vector of W such that
 w <> 0. W and
A2: g . w <> 0. K by VECTSP10:28;
 (FormFunctional (f,g)) . (v,w) = (f . v) * (g . w) by Def10;
then A3: ( dom (FormFunctional (f,g)) = [: the carrier of V, the carrier of W:] & (FormFunctional (f,g)) . (v,w) <> 0. K ) by A1, A2, FUNCT_2:def_1, VECTSP_1:12;
(FormFunctional (f,g)) . ((0. V),(0. W)) = (f . (0. V)) * (g . (0. W)) by Def10
.= (0. K) * (g . (0. W)) by HAHNBAN1:def_9
.= 0. K by VECTSP_1:7 ;
hence  not FormFunctional (f,g) is constant by A3, BINOP_1:19; ::_thesis: verum
end;
end;

registration
let K be Field;
let V, W be non trivial VectSp of K;
cluster non empty non trivial Relation-like [: the carrier of V, the carrier of W:] -defined the carrier of K -valued Function-like non constant V20([: the carrier of V, the carrier of W:]) V21([: the carrier of V, the carrier of W:], the carrier of K) additiveFAF additiveSAF homogeneousFAF homogeneousSAF for Element of bool [:[: the carrier of V, the carrier of W:], the carrier of K:];
existence
 ex b1 being Form of V,W st
( not b1 is trivial & not b1 is constant & b1 is additiveFAF & b1 is homogeneousFAF & b1 is additiveSAF & b1 is homogeneousSAF )
proof
set f = the non trivial V17() linear-Functional of V;
set g = the non trivial V17() linear-Functional of W;
take  FormFunctional ( the non trivial V17() linear-Functional of V, the non trivial V17() linear-Functional of W) ; ::_thesis: ( not FormFunctional ( the non trivial V17() linear-Functional of V, the non trivial V17() linear-Functional of W) is trivial & not FormFunctional ( the non trivial V17() linear-Functional of V, the non trivial V17() linear-Functional of W) is constant & FormFunctional ( the non trivial V17() linear-Functional of V, the non trivial V17() linear-Functional of W) is additiveFAF & FormFunctional ( the non trivial V17() linear-Functional of V, the non trivial V17() linear-Functional of W) is homogeneousFAF & FormFunctional ( the non trivial V17() linear-Functional of V, the non trivial V17() linear-Functional of W) is additiveSAF & FormFunctional ( the non trivial V17() linear-Functional of V, the non trivial V17() linear-Functional of W) is homogeneousSAF )
thus  ( not FormFunctional ( the non trivial V17() linear-Functional of V, the non trivial V17() linear-Functional of W) is trivial & not FormFunctional ( the non trivial V17() linear-Functional of V, the non trivial V17() linear-Functional of W) is constant & FormFunctional ( the non trivial V17() linear-Functional of V, the non trivial V17() linear-Functional of W) is additiveFAF & FormFunctional ( the non trivial V17() linear-Functional of V, the non trivial V17() linear-Functional of W) is homogeneousFAF & FormFunctional ( the non trivial V17() linear-Functional of V, the non trivial V17() linear-Functional of W) is additiveSAF & FormFunctional ( the non trivial V17() linear-Functional of V, the non trivial V17() linear-Functional of W) is homogeneousSAF ) ; ::_thesis: verum
end;
end;

registration
let K be non empty Abelian add-associative right_zeroed addLoopStr ;
let V, W be non empty VectSpStr over K;
let f, g be additiveSAF Form of V,W;
clusterf + g ->  additiveSAF ;
correctness
coherence
f + g is additiveSAF ;
proof
let w be Vector of W; :: according to BILINEAR:def_12 ::_thesis: FunctionalSAF ((f + g),w) is additive
set Ffg = FunctionalSAF ((f + g),w);
set Ff = FunctionalSAF (f,w);
set Fg = FunctionalSAF (g,w);
let v, y be Vector of V; :: according to VECTSP_1:def_20 ::_thesis: (FunctionalSAF ((f + g),w)) . (v + y) = ((FunctionalSAF ((f + g),w)) . v) + ((FunctionalSAF ((f + g),w)) . y)
A1: FunctionalSAF (f,w) is additive by Def12;
A2: FunctionalSAF (g,w) is additive by Def12;
thus (FunctionalSAF ((f + g),w)) . (v + y) = ((FunctionalSAF (f,w)) + (FunctionalSAF (g,w))) . (v + y) by Th12
.= ((FunctionalSAF (f,w)) . (v + y)) + ((FunctionalSAF (g,w)) . (v + y)) by HAHNBAN1:def_3
.= (((FunctionalSAF (f,w)) . v) + ((FunctionalSAF (f,w)) . y)) + ((FunctionalSAF (g,w)) . (v + y)) by A1, VECTSP_1:def_20
.= (((FunctionalSAF (f,w)) . v) + ((FunctionalSAF (f,w)) . y)) + (((FunctionalSAF (g,w)) . v) + ((FunctionalSAF (g,w)) . y)) by A2, VECTSP_1:def_20
.= ((((FunctionalSAF (f,w)) . v) + ((FunctionalSAF (f,w)) . y)) + ((FunctionalSAF (g,w)) . v)) + ((FunctionalSAF (g,w)) . y) by RLVECT_1:def_3
.= ((((FunctionalSAF (f,w)) . v) + ((FunctionalSAF (g,w)) . v)) + ((FunctionalSAF (f,w)) . y)) + ((FunctionalSAF (g,w)) . y) by RLVECT_1:def_3
.= ((((FunctionalSAF (f,w)) + (FunctionalSAF (g,w))) . v) + ((FunctionalSAF (f,w)) . y)) + ((FunctionalSAF (g,w)) . y) by HAHNBAN1:def_3
.= (((FunctionalSAF (f,w)) + (FunctionalSAF (g,w))) . v) + (((FunctionalSAF (f,w)) . y) + ((FunctionalSAF (g,w)) . y)) by RLVECT_1:def_3
.= (((FunctionalSAF (f,w)) + (FunctionalSAF (g,w))) . v) + (((FunctionalSAF (f,w)) + (FunctionalSAF (g,w))) . y) by HAHNBAN1:def_3
.= ((FunctionalSAF ((f + g),w)) . v) + (((FunctionalSAF (f,w)) + (FunctionalSAF (g,w))) . y) by Th12
.= ((FunctionalSAF ((f + g),w)) . v) + ((FunctionalSAF ((f + g),w)) . y) by Th12 ; ::_thesis: verum
end;
end;

registration
let K be non empty Abelian add-associative right_zeroed addLoopStr ;
let V, W be non empty VectSpStr over K;
let f, g be additiveFAF Form of V,W;
clusterf + g ->  additiveFAF ;
correctness
coherence
f + g is additiveFAF ;
proof
let w be Vector of V; :: according to BILINEAR:def_11 ::_thesis: FunctionalFAF ((f + g),w) is additive
set Ffg = FunctionalFAF ((f + g),w);
set Ff = FunctionalFAF (f,w);
set Fg = FunctionalFAF (g,w);
let v, y be Vector of W; :: according to VECTSP_1:def_20 ::_thesis: (FunctionalFAF ((f + g),w)) . (v + y) = ((FunctionalFAF ((f + g),w)) . v) + ((FunctionalFAF ((f + g),w)) . y)
A1: FunctionalFAF (f,w) is additive by Def11;
A2: FunctionalFAF (g,w) is additive by Def11;
thus (FunctionalFAF ((f + g),w)) . (v + y) = ((FunctionalFAF (f,w)) + (FunctionalFAF (g,w))) . (v + y) by Th13
.= ((FunctionalFAF (f,w)) . (v + y)) + ((FunctionalFAF (g,w)) . (v + y)) by HAHNBAN1:def_3
.= (((FunctionalFAF (f,w)) . v) + ((FunctionalFAF (f,w)) . y)) + ((FunctionalFAF (g,w)) . (v + y)) by A1, VECTSP_1:def_20
.= (((FunctionalFAF (f,w)) . v) + ((FunctionalFAF (f,w)) . y)) + (((FunctionalFAF (g,w)) . v) + ((FunctionalFAF (g,w)) . y)) by A2, VECTSP_1:def_20
.= ((((FunctionalFAF (f,w)) . v) + ((FunctionalFAF (f,w)) . y)) + ((FunctionalFAF (g,w)) . v)) + ((FunctionalFAF (g,w)) . y) by RLVECT_1:def_3
.= ((((FunctionalFAF (f,w)) . v) + ((FunctionalFAF (g,w)) . v)) + ((FunctionalFAF (f,w)) . y)) + ((FunctionalFAF (g,w)) . y) by RLVECT_1:def_3
.= ((((FunctionalFAF (f,w)) + (FunctionalFAF (g,w))) . v) + ((FunctionalFAF (f,w)) . y)) + ((FunctionalFAF (g,w)) . y) by HAHNBAN1:def_3
.= (((FunctionalFAF (f,w)) + (FunctionalFAF (g,w))) . v) + (((FunctionalFAF (f,w)) . y) + ((FunctionalFAF (g,w)) . y)) by RLVECT_1:def_3
.= (((FunctionalFAF (f,w)) + (FunctionalFAF (g,w))) . v) + (((FunctionalFAF (f,w)) + (FunctionalFAF (g,w))) . y) by HAHNBAN1:def_3
.= ((FunctionalFAF ((f + g),w)) . v) + (((FunctionalFAF (f,w)) + (FunctionalFAF (g,w))) . y) by Th13
.= ((FunctionalFAF ((f + g),w)) . v) + ((FunctionalFAF ((f + g),w)) . y) by Th13 ; ::_thesis: verum
end;
end;

registration
let K be non empty right_zeroed right-distributive doubleLoopStr ;
let V, W be non empty VectSpStr over K;
let f be additiveSAF Form of V,W;
let a be Element of K;
clustera * f ->  additiveSAF ;
correctness
coherence
a * f is additiveSAF ;
proof
let w be Vector of W; :: according to BILINEAR:def_12 ::_thesis: FunctionalSAF ((a * f),w) is additive
set Ffg = FunctionalSAF ((a * f),w);
set Ff = FunctionalSAF (f,w);
let v, y be Vector of V; :: according to VECTSP_1:def_20 ::_thesis: (FunctionalSAF ((a * f),w)) . (v + y) = ((FunctionalSAF ((a * f),w)) . v) + ((FunctionalSAF ((a * f),w)) . y)
A1: FunctionalSAF (f,w) is additive by Def12;
thus (FunctionalSAF ((a * f),w)) . (v + y) = (a * (FunctionalSAF (f,w))) . (v + y) by Th14
.= a * ((FunctionalSAF (f,w)) . (v + y)) by HAHNBAN1:def_6
.= a * (((FunctionalSAF (f,w)) . v) + ((FunctionalSAF (f,w)) . y)) by A1, VECTSP_1:def_20
.= (a * ((FunctionalSAF (f,w)) . v)) + (a * ((FunctionalSAF (f,w)) . y)) by VECTSP_1:def_2
.= ((a * (FunctionalSAF (f,w))) . v) + (a * ((FunctionalSAF (f,w)) . y)) by HAHNBAN1:def_6
.= ((a * (FunctionalSAF (f,w))) . v) + ((a * (FunctionalSAF (f,w))) . y) by HAHNBAN1:def_6
.= ((FunctionalSAF ((a * f),w)) . v) + ((a * (FunctionalSAF (f,w))) . y) by Th14
.= ((FunctionalSAF ((a * f),w)) . v) + ((FunctionalSAF ((a * f),w)) . y) by Th14 ; ::_thesis: verum
end;
end;

registration
let K be non empty right_zeroed right-distributive doubleLoopStr ;
let V, W be non empty VectSpStr over K;
let f be additiveFAF Form of V,W;
let a be Element of K;
clustera * f ->  additiveFAF ;
correctness
coherence
a * f is additiveFAF ;
proof
let w be Vector of V; :: according to BILINEAR:def_11 ::_thesis: FunctionalFAF ((a * f),w) is additive
set Ffg = FunctionalFAF ((a * f),w);
set Ff = FunctionalFAF (f,w);
let v, y be Vector of W; :: according to VECTSP_1:def_20 ::_thesis: (FunctionalFAF ((a * f),w)) . (v + y) = ((FunctionalFAF ((a * f),w)) . v) + ((FunctionalFAF ((a * f),w)) . y)
A1: FunctionalFAF (f,w) is additive by Def11;
thus (FunctionalFAF ((a * f),w)) . (v + y) = (a * (FunctionalFAF (f,w))) . (v + y) by Th15
.= a * ((FunctionalFAF (f,w)) . (v + y)) by HAHNBAN1:def_6
.= a * (((FunctionalFAF (f,w)) . v) + ((FunctionalFAF (f,w)) . y)) by A1, VECTSP_1:def_20
.= (a * ((FunctionalFAF (f,w)) . v)) + (a * ((FunctionalFAF (f,w)) . y)) by VECTSP_1:def_2
.= ((a * (FunctionalFAF (f,w))) . v) + (a * ((FunctionalFAF (f,w)) . y)) by HAHNBAN1:def_6
.= ((a * (FunctionalFAF (f,w))) . v) + ((a * (FunctionalFAF (f,w))) . y) by HAHNBAN1:def_6
.= ((FunctionalFAF ((a * f),w)) . v) + ((a * (FunctionalFAF (f,w))) . y) by Th15
.= ((FunctionalFAF ((a * f),w)) . v) + ((FunctionalFAF ((a * f),w)) . y) by Th15 ; ::_thesis: verum
end;
end;

registration
let K be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ;
let V, W be non empty VectSpStr over K;
let f be additiveSAF Form of V,W;
cluster - f ->  additiveSAF ;
correctness
coherence
- f is additiveSAF ;
proof
let w be Vector of W; :: according to BILINEAR:def_12 ::_thesis: FunctionalSAF ((- f),w) is additive
set Ffg = FunctionalSAF ((- f),w);
set Ff = FunctionalSAF (f,w);
let v, y be Vector of V; :: according to VECTSP_1:def_20 ::_thesis: (FunctionalSAF ((- f),w)) . (v + y) = ((FunctionalSAF ((- f),w)) . v) + ((FunctionalSAF ((- f),w)) . y)
A1: FunctionalSAF (f,w) is additive by Def12;
thus (FunctionalSAF ((- f),w)) . (v + y) = (- (FunctionalSAF (f,w))) . (v + y) by Th16
.= - ((FunctionalSAF (f,w)) . (v + y)) by HAHNBAN1:def_4
.= - (((FunctionalSAF (f,w)) . v) + ((FunctionalSAF (f,w)) . y)) by A1, VECTSP_1:def_20
.= (- ((FunctionalSAF (f,w)) . v)) - ((FunctionalSAF (f,w)) . y) by RLVECT_1:30
.= ((- (FunctionalSAF (f,w))) . v) - ((FunctionalSAF (f,w)) . y) by HAHNBAN1:def_4
.= ((- (FunctionalSAF (f,w))) . v) + (- ((FunctionalSAF (f,w)) . y)) by RLVECT_1:def_11
.= ((- (FunctionalSAF (f,w))) . v) + ((- (FunctionalSAF (f,w))) . y) by HAHNBAN1:def_4
.= ((FunctionalSAF ((- f),w)) . v) + ((- (FunctionalSAF (f,w))) . y) by Th16
.= ((FunctionalSAF ((- f),w)) . v) + ((FunctionalSAF ((- f),w)) . y) by Th16 ; ::_thesis: verum
end;
end;

registration
let K be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ;
let V, W be non empty VectSpStr over K;
let f be additiveFAF Form of V,W;
cluster - f ->  additiveFAF ;
correctness
coherence
- f is additiveFAF ;
proof
let w be Vector of V; :: according to BILINEAR:def_11 ::_thesis: FunctionalFAF ((- f),w) is additive
set Ffg = FunctionalFAF ((- f),w);
set Ff = FunctionalFAF (f,w);
let v, y be Vector of W; :: according to VECTSP_1:def_20 ::_thesis: (FunctionalFAF ((- f),w)) . (v + y) = ((FunctionalFAF ((- f),w)) . v) + ((FunctionalFAF ((- f),w)) . y)
A1: FunctionalFAF (f,w) is additive by Def11;
thus (FunctionalFAF ((- f),w)) . (v + y) = (- (FunctionalFAF (f,w))) . (v + y) by Th17
.= - ((FunctionalFAF (f,w)) . (v + y)) by HAHNBAN1:def_4
.= - (((FunctionalFAF (f,w)) . v) + ((FunctionalFAF (f,w)) . y)) by A1, VECTSP_1:def_20
.= (- ((FunctionalFAF (f,w)) . v)) - ((FunctionalFAF (f,w)) . y) by RLVECT_1:30
.= ((- (FunctionalFAF (f,w))) . v) - ((FunctionalFAF (f,w)) . y) by HAHNBAN1:def_4
.= ((- (FunctionalFAF (f,w))) . v) + (- ((FunctionalFAF (f,w)) . y)) by RLVECT_1:def_11
.= ((- (FunctionalFAF (f,w))) . v) + ((- (FunctionalFAF (f,w))) . y) by HAHNBAN1:def_4
.= ((FunctionalFAF ((- f),w)) . v) + ((- (FunctionalFAF (f,w))) . y) by Th17
.= ((FunctionalFAF ((- f),w)) . v) + ((FunctionalFAF ((- f),w)) . y) by Th17 ; ::_thesis: verum
end;
end;

registration
let K be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ;
let V, W be non empty VectSpStr over K;
let f, g be additiveSAF Form of V,W;
clusterf - g ->  additiveSAF ;
correctness
coherence
f - g is additiveSAF ;
;
end;

registration
let K be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ;
let V, W be non empty VectSpStr over K;
let f, g be additiveFAF Form of V,W;
clusterf - g ->  additiveFAF ;
correctness
coherence
f - g is additiveFAF ;
;
end;

registration
let K be non empty right_complementable add-associative right_zeroed right-distributive doubleLoopStr ;
let V, W be non empty VectSpStr over K;
let f, g be homogeneousSAF Form of V,W;
clusterf + g ->  homogeneousSAF ;
correctness
coherence
f + g is homogeneousSAF ;
proof
let w be Vector of W; :: according to BILINEAR:def_14 ::_thesis: FunctionalSAF ((f + g),w) is homogeneous
set Ffg = FunctionalSAF ((f + g),w);
set Ff = FunctionalSAF (f,w);
set Fg = FunctionalSAF (g,w);
let v be Vector of V; :: according to HAHNBAN1:def_8 ::_thesis: for b1 being Element of the carrier of K holds (FunctionalSAF ((f + g),w)) . (b1 * v) = b1 * ((FunctionalSAF ((f + g),w)) . v)
let a be Scalar of ; ::_thesis: (FunctionalSAF ((f + g),w)) . (a * v) = a * ((FunctionalSAF ((f + g),w)) . v)
thus (FunctionalSAF ((f + g),w)) . (a * v) = ((FunctionalSAF (f,w)) + (FunctionalSAF (g,w))) . (a * v) by Th12
.= ((FunctionalSAF (f,w)) . (a * v)) + ((FunctionalSAF (g,w)) . (a * v)) by HAHNBAN1:def_3
.= (a * ((FunctionalSAF (f,w)) . v)) + ((FunctionalSAF (g,w)) . (a * v)) by HAHNBAN1:def_8
.= (a * ((FunctionalSAF (f,w)) . v)) + (a * ((FunctionalSAF (g,w)) . v)) by HAHNBAN1:def_8
.= a * (((FunctionalSAF (f,w)) . v) + ((FunctionalSAF (g,w)) . v)) by VECTSP_1:def_2
.= a * (((FunctionalSAF (f,w)) + (FunctionalSAF (g,w))) . v) by HAHNBAN1:def_3
.= a * ((FunctionalSAF ((f + g),w)) . v) by Th12 ; ::_thesis: verum
end;
end;

registration
let K be non empty right_complementable add-associative right_zeroed right-distributive doubleLoopStr ;
let V, W be non empty VectSpStr over K;
let f, g be homogeneousFAF Form of V,W;
clusterf + g ->  homogeneousFAF ;
correctness
coherence
f + g is homogeneousFAF ;
proof
let w be Vector of V; :: according to BILINEAR:def_13 ::_thesis: FunctionalFAF ((f + g),w) is homogeneous
set Ffg = FunctionalFAF ((f + g),w);
set Ff = FunctionalFAF (f,w);
set Fg = FunctionalFAF (g,w);
let v be Vector of W; :: according to HAHNBAN1:def_8 ::_thesis: for b1 being Element of the carrier of K holds (FunctionalFAF ((f + g),w)) . (b1 * v) = b1 * ((FunctionalFAF ((f + g),w)) . v)
let a be Scalar of ; ::_thesis: (FunctionalFAF ((f + g),w)) . (a * v) = a * ((FunctionalFAF ((f + g),w)) . v)
thus (FunctionalFAF ((f + g),w)) . (a * v) = ((FunctionalFAF (f,w)) + (FunctionalFAF (g,w))) . (a * v) by Th13
.= ((FunctionalFAF (f,w)) . (a * v)) + ((FunctionalFAF (g,w)) . (a * v)) by HAHNBAN1:def_3
.= (a * ((FunctionalFAF (f,w)) . v)) + ((FunctionalFAF (g,w)) . (a * v)) by HAHNBAN1:def_8
.= (a * ((FunctionalFAF (f,w)) . v)) + (a * ((FunctionalFAF (g,w)) . v)) by HAHNBAN1:def_8
.= a * (((FunctionalFAF (f,w)) . v) + ((FunctionalFAF (g,w)) . v)) by VECTSP_1:def_2
.= a * (((FunctionalFAF (f,w)) + (FunctionalFAF (g,w))) . v) by HAHNBAN1:def_3
.= a * ((FunctionalFAF ((f + g),w)) . v) by Th13 ; ::_thesis: verum
end;
end;

registration
let K be non empty right_complementable add-associative right_zeroed associative commutative right-distributive doubleLoopStr ;
let V, W be non empty VectSpStr over K;
let f be homogeneousSAF Form of V,W;
let a be Element of K;
clustera * f ->  homogeneousSAF ;
correctness
coherence
a * f is homogeneousSAF ;
proof
let w be Vector of W; :: according to BILINEAR:def_14 ::_thesis: FunctionalSAF ((a * f),w) is homogeneous
set Ffg = FunctionalSAF ((a * f),w);
set Ff = FunctionalSAF (f,w);
let v be Vector of V; :: according to HAHNBAN1:def_8 ::_thesis: for b1 being Element of the carrier of K holds (FunctionalSAF ((a * f),w)) . (b1 * v) = b1 * ((FunctionalSAF ((a * f),w)) . v)
let b be Scalar of ; ::_thesis: (FunctionalSAF ((a * f),w)) . (b * v) = b * ((FunctionalSAF ((a * f),w)) . v)
thus (FunctionalSAF ((a * f),w)) . (b * v) = (a * (FunctionalSAF (f,w))) . (b * v) by Th14
.= a * ((FunctionalSAF (f,w)) . (b * v)) by HAHNBAN1:def_6
.= a * (b * ((FunctionalSAF (f,w)) . v)) by HAHNBAN1:def_8
.= b * (a * ((FunctionalSAF (f,w)) . v)) by GROUP_1:def_3
.= b * ((a * (FunctionalSAF (f,w))) . v) by HAHNBAN1:def_6
.= b * ((FunctionalSAF ((a * f),w)) . v) by Th14 ; ::_thesis: verum
end;
end;

registration
let K be non empty right_complementable add-associative right_zeroed associative commutative right-distributive doubleLoopStr ;
let V, W be non empty VectSpStr over K;
let f be homogeneousFAF Form of V,W;
let a be Element of K;
clustera * f ->  homogeneousFAF ;
correctness
coherence
a * f is homogeneousFAF ;
proof
let w be Vector of V; :: according to BILINEAR:def_13 ::_thesis: FunctionalFAF ((a * f),w) is homogeneous
set Ffg = FunctionalFAF ((a * f),w);
set Ff = FunctionalFAF (f,w);
let v be Vector of W; :: according to HAHNBAN1:def_8 ::_thesis: for b1 being Element of the carrier of K holds (FunctionalFAF ((a * f),w)) . (b1 * v) = b1 * ((FunctionalFAF ((a * f),w)) . v)
let b be Scalar of ; ::_thesis: (FunctionalFAF ((a * f),w)) . (b * v) = b * ((FunctionalFAF ((a * f),w)) . v)
thus (FunctionalFAF ((a * f),w)) . (b * v) = (a * (FunctionalFAF (f,w))) . (b * v) by Th15
.= a * ((FunctionalFAF (f,w)) . (b * v)) by HAHNBAN1:def_6
.= a * (b * ((FunctionalFAF (f,w)) . v)) by HAHNBAN1:def_8
.= b * (a * ((FunctionalFAF (f,w)) . v)) by GROUP_1:def_3
.= b * ((a * (FunctionalFAF (f,w))) . v) by HAHNBAN1:def_6
.= b * ((FunctionalFAF ((a * f),w)) . v) by Th15 ; ::_thesis: verum
end;
end;

registration
let K be non empty right_complementable add-associative right_zeroed right-distributive doubleLoopStr ;
let V, W be non empty VectSpStr over K;
let f be homogeneousSAF Form of V,W;
cluster - f ->  homogeneousSAF ;
correctness
coherence
- f is homogeneousSAF ;
proof
let w be Vector of W; :: according to BILINEAR:def_14 ::_thesis: FunctionalSAF ((- f),w) is homogeneous
set Ffg = FunctionalSAF ((- f),w);
set Ff = FunctionalSAF (f,w);
let v be Vector of V; :: according to HAHNBAN1:def_8 ::_thesis: for b1 being Element of the carrier of K holds (FunctionalSAF ((- f),w)) . (b1 * v) = b1 * ((FunctionalSAF ((- f),w)) . v)
let a be Scalar of ; ::_thesis: (FunctionalSAF ((- f),w)) . (a * v) = a * ((FunctionalSAF ((- f),w)) . v)
thus (FunctionalSAF ((- f),w)) . (a * v) = (- (FunctionalSAF (f,w))) . (a * v) by Th16
.= - ((FunctionalSAF (f,w)) . (a * v)) by HAHNBAN1:def_4
.= - (a * ((FunctionalSAF (f,w)) . v)) by HAHNBAN1:def_8
.= a * (- ((FunctionalSAF (f,w)) . v)) by VECTSP_1:8
.= a * ((- (FunctionalSAF (f,w))) . v) by HAHNBAN1:def_4
.= a * ((FunctionalSAF ((- f),w)) . v) by Th16 ; ::_thesis: verum
end;
end;

registration
let K be non empty right_complementable add-associative right_zeroed right-distributive doubleLoopStr ;
let V, W be non empty VectSpStr over K;
let f be homogeneousFAF Form of V,W;
cluster - f ->  homogeneousFAF ;
correctness
coherence
- f is homogeneousFAF ;
proof
let w be Vector of V; :: according to BILINEAR:def_13 ::_thesis: FunctionalFAF ((- f),w) is homogeneous
set Ffg = FunctionalFAF ((- f),w);
set Ff = FunctionalFAF (f,w);
let v be Vector of W; :: according to HAHNBAN1:def_8 ::_thesis: for b1 being Element of the carrier of K holds (FunctionalFAF ((- f),w)) . (b1 * v) = b1 * ((FunctionalFAF ((- f),w)) . v)
let a be Scalar of ; ::_thesis: (FunctionalFAF ((- f),w)) . (a * v) = a * ((FunctionalFAF ((- f),w)) . v)
thus (FunctionalFAF ((- f),w)) . (a * v) = (- (FunctionalFAF (f,w))) . (a * v) by Th17
.= - ((FunctionalFAF (f,w)) . (a * v)) by HAHNBAN1:def_4
.= - (a * ((FunctionalFAF (f,w)) . v)) by HAHNBAN1:def_8
.= a * (- ((FunctionalFAF (f,w)) . v)) by VECTSP_1:8
.= a * ((- (FunctionalFAF (f,w))) . v) by HAHNBAN1:def_4
.= a * ((FunctionalFAF ((- f),w)) . v) by Th17 ; ::_thesis: verum
end;
end;

registration
let K be non empty right_complementable add-associative right_zeroed right-distributive doubleLoopStr ;
let V, W be non empty VectSpStr over K;
let f, g be homogeneousSAF Form of V,W;
clusterf - g ->  homogeneousSAF ;
correctness
coherence
f - g is homogeneousSAF ;
;
end;

registration
let K be non empty right_complementable add-associative right_zeroed right-distributive doubleLoopStr ;
let V, W be non empty VectSpStr over K;
let f, g be homogeneousFAF Form of V,W;
clusterf - g ->  homogeneousFAF ;
correctness
coherence
f - g is homogeneousFAF ;
;
end;

theorem Th26: :: BILINEAR:26
for K being non empty addLoopStr
for V, W being non empty VectSpStr over K
for v, u being Vector of V
for w being Vector of W
for f being 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 ; ::_thesis: for V, W being non empty VectSpStr over K
for v, u being Vector of V
for w being Vector of W
for f being Form of V,W st f is additiveSAF holds
f . ((v + u),w) = (f . (v,w)) + (f . (u,w))
let V, W be non empty VectSpStr over K; ::_thesis: for v, u being Vector of V
for w being Vector of W
for f being Form of V,W st f is additiveSAF holds
f . ((v + u),w) = (f . (v,w)) + (f . (u,w))
let v, w be Vector of V; ::_thesis: for w being Vector of W
for f being Form of V,W st f is additiveSAF holds
f . ((v + w),w) = (f . (v,w)) + (f . (w,w))
let y be Vector of W; ::_thesis: for f being Form of V,W st f is additiveSAF holds
f . ((v + w),y) = (f . (v,y)) + (f . (w,y))
let f be Form of V,W; ::_thesis: ( f is additiveSAF implies f . ((v + w),y) = (f . (v,y)) + (f . (w,y)) )
set F = FunctionalSAF (f,y);
assume  f is additiveSAF ; ::_thesis: f . ((v + w),y) = (f . (v,y)) + (f . (w,y))
then A1: FunctionalSAF (f,y) is additive by Def12;
thus f . ((v + w),y) = (FunctionalSAF (f,y)) . (v + w) by Th9
.= ((FunctionalSAF (f,y)) . v) + ((FunctionalSAF (f,y)) . w) by A1, VECTSP_1:def_20
.= (f . (v,y)) + ((FunctionalSAF (f,y)) . w) by Th9
.= (f . (v,y)) + (f . (w,y)) by Th9 ; ::_thesis: verum
end;

theorem Th27: :: BILINEAR:27
for K being non empty addLoopStr
for V, W being non empty VectSpStr over K
for v being Vector of V
for u, w being Vector of W
for f being 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 ; ::_thesis: for V, W being non empty VectSpStr over K
for v being Vector of V
for u, w being Vector of W
for f being Form of V,W st f is additiveFAF holds
f . (v,(u + w)) = (f . (v,u)) + (f . (v,w))
let V, W be non empty VectSpStr over K; ::_thesis: for v being Vector of V
for u, w being Vector of W
for f being Form of V,W st f is additiveFAF holds
f . (v,(u + w)) = (f . (v,u)) + (f . (v,w))
let v be Vector of V; ::_thesis: for u, w being Vector of W
for f being Form of V,W st f is additiveFAF holds
f . (v,(u + w)) = (f . (v,u)) + (f . (v,w))
let y, z be Vector of W; ::_thesis: for f being Form of V,W st f is additiveFAF holds
f . (v,(y + z)) = (f . (v,y)) + (f . (v,z))
let f be Form of V,W; ::_thesis: ( f is additiveFAF implies f . (v,(y + z)) = (f . (v,y)) + (f . (v,z)) )
set F = FunctionalFAF (f,v);
assume  f is additiveFAF ; ::_thesis: f . (v,(y + z)) = (f . (v,y)) + (f . (v,z))
then A1: FunctionalFAF (f,v) is additive by Def11;
thus f . (v,(y + z)) = (FunctionalFAF (f,v)) . (y + z) by Th8
.= ((FunctionalFAF (f,v)) . y) + ((FunctionalFAF (f,v)) . z) by A1, VECTSP_1:def_20
.= (f . (v,y)) + ((FunctionalFAF (f,v)) . z) by Th8
.= (f . (v,y)) + (f . (v,z)) by Th8 ; ::_thesis: verum
end;

theorem Th28: :: BILINEAR:28
for K being non empty right_zeroed addLoopStr
for V, W being non empty VectSpStr over K
for v, u being Vector of V
for w, t being Vector of W
for f being additiveFAF additiveSAF 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 non empty right_zeroed addLoopStr ; ::_thesis: for V, W being non empty VectSpStr over K
for v, u being Vector of V
for w, t being Vector of W
for f being additiveFAF additiveSAF Form of V,W holds f . ((v + u),(w + t)) = ((f . (v,w)) + (f . (v,t))) + ((f . (u,w)) + (f . (u,t)))
let V, W be non empty VectSpStr over K; ::_thesis: for v, u being Vector of V
for w, t being Vector of W
for f being additiveFAF additiveSAF Form of V,W holds f . ((v + u),(w + t)) = ((f . (v,w)) + (f . (v,t))) + ((f . (u,w)) + (f . (u,t)))
let v, w be Vector of V; ::_thesis: for w, t being Vector of W
for f being additiveFAF additiveSAF Form of V,W holds f . ((v + w),(w + t)) = ((f . (v,w)) + (f . (v,t))) + ((f . (w,w)) + (f . (w,t)))
let y, z be Vector of W; ::_thesis: for f being additiveFAF additiveSAF Form of V,W holds f . ((v + w),(y + z)) = ((f . (v,y)) + (f . (v,z))) + ((f . (w,y)) + (f . (w,z)))
let f be additiveFAF additiveSAF Form of V,W; ::_thesis: f . ((v + w),(y + z)) = ((f . (v,y)) + (f . (v,z))) + ((f . (w,y)) + (f . (w,z)))
set v1 = f . (v,y);
set v3 = f . (v,z);
set v4 = f . (w,y);
set v5 = f . (w,z);
thus f . ((v + w),(y + z)) = (f . (v,(y + z))) + (f . (w,(y + z))) by Th26
.= ((f . (v,y)) + (f . (v,z))) + (f . (w,(y + z))) by Th27
.= ((f . (v,y)) + (f . (v,z))) + ((f . (w,y)) + (f . (w,z))) by Th27 ; ::_thesis: verum
end;

theorem Th29: :: BILINEAR:29
for K being non empty right_complementable add-associative right_zeroed doubleLoopStr
for V, W being non empty right_zeroed VectSpStr over K
for f being additiveFAF Form of V,W
for v being Vector of V holds f . (v,(0. W)) = 0. K
proof
let F be non empty right_complementable add-associative right_zeroed doubleLoopStr ; ::_thesis: for V, W being non empty right_zeroed VectSpStr over F
for f being additiveFAF Form of V,W
for v being Vector of V holds f . (v,(0. W)) = 0. F
let V, W be non empty right_zeroed VectSpStr over F; ::_thesis: for f being additiveFAF Form of V,W
for v being Vector of V holds f . (v,(0. W)) = 0. F
let f be additiveFAF Form of V,W; ::_thesis: for v being Vector of V holds f . (v,(0. W)) = 0. F
let v be Vector of V; ::_thesis: f . (v,(0. W)) = 0. F
f . (v,(0. W)) = f . (v,((0. W) + (0. W))) by RLVECT_1:def_4
.= (f . (v,(0. W))) + (f . (v,(0. W))) by Th27 ;
hence  f . (v,(0. W)) = 0. F by RLVECT_1:9; ::_thesis: verum
end;

theorem Th30: :: BILINEAR:30
for K being non empty right_complementable add-associative right_zeroed doubleLoopStr
for V, W being non empty right_zeroed VectSpStr over K
for f being additiveSAF Form of V,W
for w being Vector of W holds f . ((0. V),w) = 0. K
proof
let F be non empty right_complementable add-associative right_zeroed doubleLoopStr ; ::_thesis: for V, W being non empty right_zeroed VectSpStr over F
for f being additiveSAF Form of V,W
for w being Vector of W holds f . ((0. V),w) = 0. F
let V, W be non empty right_zeroed VectSpStr over F; ::_thesis: for f being additiveSAF Form of V,W
for w being Vector of W holds f . ((0. V),w) = 0. F
let f be additiveSAF Form of V,W; ::_thesis: for w being Vector of W holds f . ((0. V),w) = 0. F
let v be Vector of W; ::_thesis: f . ((0. V),v) = 0. F
f . ((0. V),v) = f . (((0. V) + (0. V)),v) by RLVECT_1:def_4
.= (f . ((0. V),v)) + (f . ((0. V),v)) by Th26 ;
hence  f . ((0. V),v) = 0. F by RLVECT_1:9; ::_thesis: verum
end;

theorem Th31: :: BILINEAR:31
for K being non empty multMagma
for V, W being non empty VectSpStr over K
for v being Vector of V
for w being Vector of W
for a being Element of K
for f being Form of V,W st f is homogeneousSAF holds
f . ((a * v),w) = a * (f . (v,w))
proof
let K be non empty multMagma ; ::_thesis: for V, W being non empty VectSpStr over K
for v being Vector of V
for w being Vector of W
for a being Element of K
for f being Form of V,W st f is homogeneousSAF holds
f . ((a * v),w) = a * (f . (v,w))
let V, W be non empty VectSpStr over K; ::_thesis: for v being Vector of V
for w being Vector of W
for a being Element of K
for f being Form of V,W st f is homogeneousSAF holds
f . ((a * v),w) = a * (f . (v,w))
let v be Vector of V; ::_thesis: for w being Vector of W
for a being Element of K
for f being Form of V,W st f is homogeneousSAF holds
f . ((a * v),w) = a * (f . (v,w))
let y be Vector of W; ::_thesis: for a being Element of K
for f being Form of V,W st f is homogeneousSAF holds
f . ((a * v),y) = a * (f . (v,y))
let r be Element of K; ::_thesis: for f being Form of V,W st f is homogeneousSAF holds
f . ((r * v),y) = r * (f . (v,y))
let f be Form of V,W; ::_thesis: ( f is homogeneousSAF implies f . ((r * v),y) = r * (f . (v,y)) )
set F = FunctionalSAF (f,y);
assume  f is homogeneousSAF ; ::_thesis: f . ((r * v),y) = r * (f . (v,y))
then A1: FunctionalSAF (f,y) is homogeneous by Def14;
thus f . ((r * v),y) = (FunctionalSAF (f,y)) . (r * v) by Th9
.= r * ((FunctionalSAF (f,y)) . v) by A1, HAHNBAN1:def_8
.= r * (f . (v,y)) by Th9 ; ::_thesis: verum
end;

theorem Th32: :: BILINEAR:32
for K being non empty multMagma
for V, W being non empty VectSpStr over K
for v being Vector of V
for w being Vector of W
for a being Element of K
for f being Form of V,W st f is homogeneousFAF holds
f . (v,(a * w)) = a * (f . (v,w))
proof
let K be non empty multMagma ; ::_thesis: for V, W being non empty VectSpStr over K
for v being Vector of V
for w being Vector of W
for a being Element of K
for f being Form of V,W st f is homogeneousFAF holds
f . (v,(a * w)) = a * (f . (v,w))
let V, W be non empty VectSpStr over K; ::_thesis: for v being Vector of V
for w being Vector of W
for a being Element of K
for f being Form of V,W st f is homogeneousFAF holds
f . (v,(a * w)) = a * (f . (v,w))
let v be Vector of V; ::_thesis: for w being Vector of W
for a being Element of K
for f being Form of V,W st f is homogeneousFAF holds
f . (v,(a * w)) = a * (f . (v,w))
let y be Vector of W; ::_thesis: for a being Element of K
for f being Form of V,W st f is homogeneousFAF holds
f . (v,(a * y)) = a * (f . (v,y))
let r be Element of K; ::_thesis: for f being Form of V,W st f is homogeneousFAF holds
f . (v,(r * y)) = r * (f . (v,y))
let f be Form of V,W; ::_thesis: ( f is homogeneousFAF implies f . (v,(r * y)) = r * (f . (v,y)) )
set F = FunctionalFAF (f,v);
assume  f is homogeneousFAF ; ::_thesis: f . (v,(r * y)) = r * (f . (v,y))
then A1: FunctionalFAF (f,v) is homogeneous by Def13;
thus f . (v,(r * y)) = (FunctionalFAF (f,v)) . (r * y) by Th8
.= r * ((FunctionalFAF (f,v)) . y) by A1, HAHNBAN1:def_8
.= r * (f . (v,y)) by Th8 ; ::_thesis: verum
end;

theorem Th33: :: BILINEAR:33
for K being non empty right_complementable add-associative right_zeroed associative distributive left_unital doubleLoopStr
for V, W being non empty right_complementable add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over K
for f being homogeneousSAF Form of V,W
for w being Vector of W holds f . ((0. V),w) = 0. K
proof
let F be non empty right_complementable add-associative right_zeroed associative distributive left_unital doubleLoopStr ; ::_thesis: for V, W being non empty right_complementable add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over F
for f being homogeneousSAF Form of V,W
for w being Vector of W holds f . ((0. V),w) = 0. F
let V, W be non empty right_complementable add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over F; ::_thesis: for f being homogeneousSAF Form of V,W
for w being Vector of W holds f . ((0. V),w) = 0. F
let f be homogeneousSAF Form of V,W; ::_thesis: for w being Vector of W holds f . ((0. V),w) = 0. F
let v be Vector of W; ::_thesis: f . ((0. V),v) = 0. F
thus f . ((0. V),v) = f . (((0. F) * (0. V)),v) by VECTSP10:1
.= (0. F) * (f . ((0. V),v)) by Th31
.= 0. F by VECTSP_1:7 ; ::_thesis: verum
end;

theorem Th34: :: BILINEAR:34
for K being non empty right_complementable add-associative right_zeroed associative distributive left_unital doubleLoopStr
for V, W being non empty right_complementable add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over K
for f being homogeneousFAF Form of V,W
for v being Vector of V holds f . (v,(0. W)) = 0. K
proof
let F be non empty right_complementable add-associative right_zeroed associative distributive left_unital doubleLoopStr ; ::_thesis: for V, W being non empty right_complementable add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over F
for f being homogeneousFAF Form of V,W
for v being Vector of V holds f . (v,(0. W)) = 0. F
let V, W be non empty right_complementable add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over F; ::_thesis: for f being homogeneousFAF Form of V,W
for v being Vector of V holds f . (v,(0. W)) = 0. F
let f be homogeneousFAF Form of V,W; ::_thesis: for v being Vector of V holds f . (v,(0. W)) = 0. F
let v be Vector of V; ::_thesis: f . (v,(0. W)) = 0. F
thus f . (v,(0. W)) = f . (v,((0. F) * (0. W))) by VECTSP10:1
.= (0. F) * (f . (v,(0. W))) by Th32
.= 0. F by VECTSP_1:7 ; ::_thesis: verum
end;

theorem Th35: :: BILINEAR:35
for K being non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr
for V, W being VectSp of K
for v, u being Vector of V
for w being Vector of W
for f being additiveSAF homogeneousSAF Form of V,W holds f . ((v - u),w) = (f . (v,w)) - (f . (u,w))
proof
let K be non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr ; ::_thesis: for V, W being VectSp of K
for v, u being Vector of V
for w being Vector of W
for f being additiveSAF homogeneousSAF Form of V,W holds f . ((v - u),w) = (f . (v,w)) - (f . (u,w))
let V, W be VectSp of K; ::_thesis: for v, u being Vector of V
for w being Vector of W
for f being additiveSAF homogeneousSAF Form of V,W holds f . ((v - u),w) = (f . (v,w)) - (f . (u,w))
let v, w be Vector of V; ::_thesis: for w being Vector of W
for f being additiveSAF homogeneousSAF Form of V,W holds f . ((v - w),w) = (f . (v,w)) - (f . (w,w))
let y be Vector of W; ::_thesis: for f being additiveSAF homogeneousSAF Form of V,W holds f . ((v - w),y) = (f . (v,y)) - (f . (w,y))
let f be additiveSAF homogeneousSAF Form of V,W; ::_thesis: f . ((v - w),y) = (f . (v,y)) - (f . (w,y))
thus f . ((v - w),y) = f . ((v + (- w)),y) by RLVECT_1:def_11
.= (f . (v,y)) + (f . ((- w),y)) by Th26
.= (f . (v,y)) + (f . (((- (1. K)) * w),y)) by VECTSP_1:14
.= (f . (v,y)) + ((- (1. K)) * (f . (w,y))) by Th31
.= (f . (v,y)) + (- ((1. K) * (f . (w,y)))) by VECTSP_1:9
.= (f . (v,y)) - ((1. K) * (f . (w,y))) by RLVECT_1:def_11
.= (f . (v,y)) - (f . (w,y)) by VECTSP_1:def_8 ; ::_thesis: verum
end;

theorem Th36: :: BILINEAR:36
for K being non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr
for V, W being VectSp of K
for v being Vector of V
for w, t being Vector of W
for f being additiveFAF homogeneousFAF Form of V,W holds f . (v,(w - t)) = (f . (v,w)) - (f . (v,t))
proof
let K be non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr ; ::_thesis: for V, W being VectSp of K
for v being Vector of V
for w, t being Vector of W
for f being additiveFAF homogeneousFAF Form of V,W holds f . (v,(w - t)) = (f . (v,w)) - (f . (v,t))
let V, W be VectSp of K; ::_thesis: for v being Vector of V
for w, t being Vector of W
for f being additiveFAF homogeneousFAF Form of V,W holds f . (v,(w - t)) = (f . (v,w)) - (f . (v,t))
let v be Vector of V; ::_thesis: for w, t being Vector of W
for f being additiveFAF homogeneousFAF Form of V,W holds f . (v,(w - t)) = (f . (v,w)) - (f . (v,t))
let y, z be Vector of W; ::_thesis: for f being additiveFAF homogeneousFAF Form of V,W holds f . (v,(y - z)) = (f . (v,y)) - (f . (v,z))
let f be additiveFAF homogeneousFAF Form of V,W; ::_thesis: f . (v,(y - z)) = (f . (v,y)) - (f . (v,z))
thus f . (v,(y - z)) = f . (v,(y + (- z))) by RLVECT_1:def_11
.= (f . (v,y)) + (f . (v,(- z))) by Th27
.= (f . (v,y)) + (f . (v,((- (1. K)) * z))) by VECTSP_1:14
.= (f . (v,y)) + ((- (1. K)) * (f . (v,z))) by Th32
.= (f . (v,y)) + (- ((1. K) * (f . (v,z)))) by VECTSP_1:9
.= (f . (v,y)) - ((1. K) * (f . (v,z))) by RLVECT_1:def_11
.= (f . (v,y)) - (f . (v,z)) by VECTSP_1:def_8 ; ::_thesis: verum
end;

theorem Th37: :: BILINEAR:37
for K being non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr
for V, W being VectSp of K
for v, u being Vector of V
for w, t being Vector of W
for f being 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 non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr ; ::_thesis: for V, W being VectSp of K
for v, u being Vector of V
for w, t being Vector of W
for f being bilinear-Form of V,W holds f . ((v - u),(w - t)) = ((f . (v,w)) - (f . (v,t))) - ((f . (u,w)) - (f . (u,t)))
let V, W be VectSp of K; ::_thesis: for v, u being Vector of V
for w, t being Vector of W
for f being bilinear-Form of V,W holds f . ((v - u),(w - t)) = ((f . (v,w)) - (f . (v,t))) - ((f . (u,w)) - (f . (u,t)))
let v, w be Vector of V; ::_thesis: for w, t being Vector of W
for f being bilinear-Form of V,W holds f . ((v - w),(w - t)) = ((f . (v,w)) - (f . (v,t))) - ((f . (w,w)) - (f . (w,t)))
let y, z be Vector of W; ::_thesis: for f being bilinear-Form of V,W holds f . ((v - w),(y - z)) = ((f . (v,y)) - (f . (v,z))) - ((f . (w,y)) - (f . (w,z)))
let f be bilinear-Form of V,W; ::_thesis: f . ((v - w),(y - z)) = ((f . (v,y)) - (f . (v,z))) - ((f . (w,y)) - (f . (w,z)))
set v1 = f . (v,y);
set v3 = f . (v,z);
set v4 = f . (w,y);
set v5 = f . (w,z);
thus f . ((v - w),(y - z)) = (f . (v,(y - z))) - (f . (w,(y - z))) by Th35
.= ((f . (v,y)) - (f . (v,z))) - (f . (w,(y - z))) by Th36
.= ((f . (v,y)) - (f . (v,z))) - ((f . (w,y)) - (f . (w,z))) by Th36 ; ::_thesis: verum
end;

theorem :: BILINEAR:38
for K being non empty right_complementable add-associative right_zeroed associative well-unital distributive doubleLoopStr
for V, W being non empty right_complementable add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over K
for v, u being Vector of V
for w, t being Vector of W
for a, b being Element of K
for f being 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 non empty right_complementable add-associative right_zeroed associative well-unital distributive doubleLoopStr ; ::_thesis: for V, W being non empty right_complementable add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over K
for v, u being Vector of V
for w, t being Vector of W
for a, b being Element of K
for f being 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)))))
let V, W be non empty right_complementable add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over K; ::_thesis: for v, u being Vector of V
for w, t being Vector of W
for a, b being Element of K
for f being 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)))))
let v, w be Vector of V; ::_thesis: for w, t being Vector of W
for a, b being Element of K
for f being bilinear-Form of V,W holds f . ((v + (a * w)),(w + (b * t))) = ((f . (v,w)) + (b * (f . (v,t)))) + ((a * (f . (w,w))) + (a * (b * (f . (w,t)))))
let y, z be Vector of W; ::_thesis: for a, b being Element of K
for f being bilinear-Form of V,W holds f . ((v + (a * w)),(y + (b * z))) = ((f . (v,y)) + (b * (f . (v,z)))) + ((a * (f . (w,y))) + (a * (b * (f . (w,z)))))
let a, b be Element of K; ::_thesis: for f being bilinear-Form of V,W holds f . ((v + (a * w)),(y + (b * z))) = ((f . (v,y)) + (b * (f . (v,z)))) + ((a * (f . (w,y))) + (a * (b * (f . (w,z)))))
let f be bilinear-Form of V,W; ::_thesis: f . ((v + (a * w)),(y + (b * z))) = ((f . (v,y)) + (b * (f . (v,z)))) + ((a * (f . (w,y))) + (a * (b * (f . (w,z)))))
set v1 = f . (v,y);
set v3 = f . (v,z);
set v4 = f . (w,y);
set v5 = f . (w,z);
thus f . ((v + (a * w)),(y + (b * z))) = ((f . (v,y)) + (f . (v,(b * z)))) + ((f . ((a * w),y)) + (f . ((a * w),(b * z)))) by Th28
.= ((f . (v,y)) + (b * (f . (v,z)))) + ((f . ((a * w),y)) + (f . ((a * w),(b * z)))) by Th32
.= ((f . (v,y)) + (b * (f . (v,z)))) + ((a * (f . (w,y))) + (f . ((a * w),(b * z)))) by Th31
.= ((f . (v,y)) + (b * (f . (v,z)))) + ((a * (f . (w,y))) + (a * (f . (w,(b * z))))) by Th31
.= ((f . (v,y)) + (b * (f . (v,z)))) + ((a * (f . (w,y))) + (a * (b * (f . (w,z))))) by Th32 ; ::_thesis: verum
end;

theorem :: BILINEAR:39
for K being non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr
for V, W being VectSp of K
for v, u being Vector of V
for w, t being Vector of W
for a, b being Element of K
for f being 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 non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr ; ::_thesis: for V, W being VectSp of K
for v, u being Vector of V
for w, t being Vector of W
for a, b being Element of K
for f being 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)))))
let V, W be VectSp of K; ::_thesis: for v, u being Vector of V
for w, t being Vector of W
for a, b being Element of K
for f being 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)))))
let v, w be Vector of V; ::_thesis: for w, t being Vector of W
for a, b being Element of K
for f being bilinear-Form of V,W holds f . ((v - (a * w)),(w - (b * t))) = ((f . (v,w)) - (b * (f . (v,t)))) - ((a * (f . (w,w))) - (a * (b * (f . (w,t)))))
let y, z be Vector of W; ::_thesis: for a, b being Element of K
for f being bilinear-Form of V,W holds f . ((v - (a * w)),(y - (b * z))) = ((f . (v,y)) - (b * (f . (v,z)))) - ((a * (f . (w,y))) - (a * (b * (f . (w,z)))))
let a, b be Element of K; ::_thesis: for f being bilinear-Form of V,W holds f . ((v - (a * w)),(y - (b * z))) = ((f . (v,y)) - (b * (f . (v,z)))) - ((a * (f . (w,y))) - (a * (b * (f . (w,z)))))
let f be bilinear-Form of V,W; ::_thesis: f . ((v - (a * w)),(y - (b * z))) = ((f . (v,y)) - (b * (f . (v,z)))) - ((a * (f . (w,y))) - (a * (b * (f . (w,z)))))
set v1 = f . (v,y);
set v3 = f . (v,z);
set v4 = f . (w,y);
set v5 = f . (w,z);
thus f . ((v - (a * w)),(y - (b * z))) = ((f . (v,y)) - (f . (v,(b * z)))) - ((f . ((a * w),y)) - (f . ((a * w),(b * z)))) by Th37
.= ((f . (v,y)) - (b * (f . (v,z)))) - ((f . ((a * w),y)) - (f . ((a * w),(b * z)))) by Th32
.= ((f . (v,y)) - (b * (f . (v,z)))) - ((a * (f . (w,y))) - (f . ((a * w),(b * z)))) by Th31
.= ((f . (v,y)) - (b * (f . (v,z)))) - ((a * (f . (w,y))) - (a * (f . (w,(b * z))))) by Th31
.= ((f . (v,y)) - (b * (f . (v,z)))) - ((a * (f . (w,y))) - (a * (b * (f . (w,z))))) by Th32 ; ::_thesis: verum
end;

theorem Th40: :: BILINEAR:40
for K being non empty right_complementable add-associative right_zeroed doubleLoopStr
for V, W being non empty right_zeroed VectSpStr over K
for f being Form of V,W st ( f is additiveFAF or f is additiveSAF ) holds
( f is constant iff for v being Vector of V
for w being Vector of W holds f . (v,w) = 0. K )
proof
let K be non empty right_complementable add-associative right_zeroed doubleLoopStr ; ::_thesis: for V, W being non empty right_zeroed VectSpStr over K
for f being Form of V,W st ( f is additiveFAF or f is additiveSAF ) holds
( f is constant iff for v being Vector of V
for w being Vector of W holds f . (v,w) = 0. K )
let V, W be non empty right_zeroed VectSpStr over K; ::_thesis: for f being Form of V,W st ( f is additiveFAF or f is additiveSAF ) holds
( f is constant iff for v being Vector of V
for w being Vector of W holds f . (v,w) = 0. K )
let f be Form of V,W; ::_thesis: ( ( f is additiveFAF or f is additiveSAF ) implies ( f is constant iff for v being Vector of V
for w being Vector of W holds f . (v,w) = 0. K ) )
A1: dom f = [: the carrier of V, the carrier of W:] by FUNCT_2:def_1;
assume A2: ( f is additiveFAF or f is additiveSAF ) ; ::_thesis: ( f is constant iff for v being Vector of V
for w being Vector of W holds f . (v,w) = 0. K )
hereby  ::_thesis: ( ( for v being Vector of V
for w being Vector of W holds f . (v,w) = 0. K ) implies f is constant )
assume A3: f is constant ; ::_thesis: for v being Vector of V
for w being Vector of W holds f . (b3,b4) = 0. K
let v be Vector of V; ::_thesis: for w being Vector of W holds f . (b2,b3) = 0. K
let w be Vector of W; ::_thesis: f . (b1,b2) = 0. K
percases ( f is additiveFAF or f is additiveSAF ) by A2;
supposeA4: f is additiveFAF ; ::_thesis: f . (b1,b2) = 0. K
thus f . (v,w) = f . (v,(0. W)) by A1, A3, BINOP_1:19
.= 0. K by A4, Th29 ; ::_thesis: verum
end;
supposeA5: f is additiveSAF ; ::_thesis: f . (b1,b2) = 0. K
thus f . (v,w) = f . ((0. V),w) by A1, A3, BINOP_1:19
.= 0. K by A5, Th30 ; ::_thesis: verum
end;
end;
end;
hereby  ::_thesis: verum
assume A6: for v being Vector of V
for w being Vector of W holds f . (v,w) = 0. K ; ::_thesis: f is constant
now__::_thesis:_for_x,_y_being_set_st_x_in_dom_f_&_y_in_dom_f_holds_
f_._x_=_f_._y
let x, y be set ; ::_thesis: ( x in dom f & y in dom f implies f . x = f . y )
assume that
A7: x in dom f and
A8: y in dom f ; ::_thesis: f . x = f . y
consider v being Vector of V, w being Vector of W such that
A9: x = [v,w] by A7, DOMAIN_1:1;
consider s being Vector of V, t being Vector of W such that
A10: y = [s,t] by A8, DOMAIN_1:1;
thus f . x = f . (v,w) by A9
.= 0. K by A6
.= f . (s,t) by A6
.= f . y by A10 ; ::_thesis: verum
end;
hence  f is constant by FUNCT_1:def_10; ::_thesis: verum
end;
end;

begin

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 :: BILINEAR:def 15
 {  v where v is Vector of V : for w being Vector of W holds f . (v,w) = 0. K  }  ;
correctness
coherence
{  v where v is Vector of V : for w being Vector of W holds f . (v,w) = 0. K  }  is Subset of V;
proof
set A =  {  v where v is Vector of V : for w being Vector of W holds f . (v,w) = 0. K  }  ;
  {  v where v is Vector of V : for w being Vector of W holds f . (v,w) = 0. K  }  c= the carrier of V
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  v where v is Vector of V : for w being Vector of W holds f . (v,w) = 0. K  }  or x in the carrier of V )
assume  x in  {  v where v is Vector of V : for w being Vector of W holds f . (v,w) = 0. K  }  ; ::_thesis: x in the carrier of V
then  ex v being Vector of V st
( v = x & ( for w being Vector of W holds f . (v,w) = 0. K ) ) ;
hence  x in the carrier of V ; ::_thesis: verum
end;
hence   {  v where v is Vector of V : for w being Vector of W holds f . (v,w) = 0. K  }  is Subset of V ; ::_thesis: verum
end;
end;

:: deftheorem  defines leftker BILINEAR:def_15_:_
 for K being ZeroStr
for V, W being non empty VectSpStr over K
for f being Form of V,W holds leftker f =  {  v where v is Vector of V : for w being Vector of W holds f . (v,w) = 0. K  }  ;

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 :: BILINEAR:def 16
 {  w where w is Vector of W : for v being Vector of V holds f . (v,w) = 0. K  }  ;
correctness
coherence
{  w where w is Vector of W : for v being Vector of V holds f . (v,w) = 0. K  }  is Subset of W;
proof
set A =  {  w where w is Vector of W : for v being Vector of V holds f . (v,w) = 0. K  }  ;
  {  w where w is Vector of W : for v being Vector of V holds f . (v,w) = 0. K  }  c= the carrier of W
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  w where w is Vector of W : for v being Vector of V holds f . (v,w) = 0. K  }  or x in the carrier of W )
assume  x in  {  w where w is Vector of W : for v being Vector of V holds f . (v,w) = 0. K  }  ; ::_thesis: x in the carrier of W
then  ex w being Vector of W st
( w = x & ( for v being Vector of V holds f . (v,w) = 0. K ) ) ;
hence  x in the carrier of W ; ::_thesis: verum
end;
hence   {  w where w is Vector of W : for v being Vector of V holds f . (v,w) = 0. K  }  is Subset of W ; ::_thesis: verum
end;
end;

:: deftheorem  defines rightker BILINEAR:def_16_:_
 for K being ZeroStr
for V, W being non empty VectSpStr over K
for f being Form of V,W holds rightker f =  {  w where w is Vector of W : for v being Vector of V holds f . (v,w) = 0. K  }  ;

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 :: BILINEAR:def 17
 {  v where v is Vector of V : f . (v,v) = 0. K  }  ;
correctness
coherence
{  v where v is Vector of V : f . (v,v) = 0. K  }  is Subset of V;
proof
set A =  {  v where v is Vector of V : f . (v,v) = 0. K  }  ;
  {  v where v is Vector of V : f . (v,v) = 0. K  }  c= the carrier of V
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  v where v is Vector of V : f . (v,v) = 0. K  }  or x in the carrier of V )
assume  x in  {  v where v is Vector of V : f . (v,v) = 0. K  }  ; ::_thesis: x in the carrier of V
then  ex v being Vector of V st
( v = x & f . (v,v) = 0. K ) ;
hence  x in the carrier of V ; ::_thesis: verum
end;
hence   {  v where v is Vector of V : f . (v,v) = 0. K  }  is Subset of V ; ::_thesis: verum
end;
end;

:: deftheorem  defines diagker BILINEAR:def_17_:_
 for K being ZeroStr
for V being non empty VectSpStr over K
for f being Form of V,V holds diagker f =  {  v where v is Vector of V : f . (v,v) = 0. K  }  ;

registration
let K be non empty right_complementable add-associative right_zeroed right-distributive doubleLoopStr ;
let V be non empty right_zeroed 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
 not leftker f is empty
proof
now__::_thesis:_for_w_being_Vector_of_W_holds_f_._((0._V),w)_=_0._K
let w be Vector of W; ::_thesis: f . ((0. V),w) = 0. K
thus f . ((0. V),w) = (FunctionalSAF (f,w)) . (0. V) by Th9
.= 0. K by HAHNBAN1:def_9 ; ::_thesis: verum
end;
then  0. V in leftker f ;
hence  not leftker f is empty ; ::_thesis: verum
end;
end;

registration
let K be non empty right_complementable add-associative right_zeroed associative well-unital distributive doubleLoopStr ;
let V be non empty right_complementable add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital 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
 not leftker f is empty
proof
now__::_thesis:_for_w_being_Vector_of_W_holds_f_._((0._V),w)_=_0._K
let w be Vector of W; ::_thesis: f . ((0. V),w) = 0. K
thus f . ((0. V),w) = (FunctionalSAF (f,w)) . (0. V) by Th9
.= 0. K by HAHNBAN1:def_9 ; ::_thesis: verum
end;
then  0. V in leftker f ;
hence  not leftker f is empty ; ::_thesis: verum
end;
end;

registration
let K be non empty right_complementable add-associative right_zeroed right-distributive doubleLoopStr ;
let V be non empty VectSpStr over K;
let W be non empty right_zeroed VectSpStr over K;
let f be additiveFAF Form of V,W;
cluster rightker f ->  non empty ;
coherence
 not rightker f is empty
proof
now__::_thesis:_for_v_being_Vector_of_V_holds_f_._(v,(0._W))_=_0._K
let v be Vector of V; ::_thesis: f . (v,(0. W)) = 0. K
thus f . (v,(0. W)) = (FunctionalFAF (f,v)) . (0. W) by Th8
.= 0. K by HAHNBAN1:def_9 ; ::_thesis: verum
end;
then  0. W in rightker f ;
hence  not rightker f is empty ; ::_thesis: verum
end;
end;

registration
let K be non empty right_complementable add-associative right_zeroed associative well-unital distributive doubleLoopStr ;
let V be non empty VectSpStr over K;
let W be non empty right_complementable add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over K;
let f be homogeneousFAF Form of V,W;
cluster rightker f ->  non empty ;
coherence
 not rightker f is empty
proof
now__::_thesis:_for_v_being_Vector_of_V_holds_f_._(v,(0._W))_=_0._K
let v be Vector of V; ::_thesis: f . (v,(0. W)) = 0. K
thus f . (v,(0. W)) = (FunctionalFAF (f,v)) . (0. W) by Th8
.= 0. K by HAHNBAN1:def_9 ; ::_thesis: verum
end;
then  0. W in rightker f ;
hence  not rightker f is empty ; ::_thesis: verum
end;
end;

registration
let K be non empty right_complementable add-associative right_zeroed doubleLoopStr ;
let V be non empty right_zeroed VectSpStr over K;
let f be additiveFAF Form of V,V;
cluster diagker f ->  non empty ;
coherence
 not diagker f is empty
proof
 f . ((0. V),(0. V)) = 0. K by Th29;
then  0. V in diagker f ;
hence  not diagker f is empty ; ::_thesis: verum
end;
end;

registration
let K be non empty right_complementable add-associative right_zeroed doubleLoopStr ;
let V be non empty right_zeroed VectSpStr over K;
let f be additiveSAF Form of V,V;
cluster diagker f ->  non empty ;
coherence
 not diagker f is empty
proof
 f . ((0. V),(0. V)) = 0. K by Th30;
then  0. V in diagker f ;
hence  not diagker f is empty ; ::_thesis: verum
end;
end;

registration
let K be non empty right_complementable add-associative right_zeroed associative well-unital distributive doubleLoopStr ;
let V be non empty right_complementable add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over K;
let f be homogeneousFAF Form of V,V;
cluster diagker f ->  non empty ;
coherence
 not diagker f is empty
proof
 f . ((0. V),(0. V)) = 0. K by Th34;
then  0. V in diagker f ;
hence  not diagker f is empty ; ::_thesis: verum
end;
end;

registration
let K be non empty right_complementable add-associative right_zeroed associative well-unital distributive doubleLoopStr ;
let V be non empty right_complementable add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital VectSpStr over K;
let f be homogeneousSAF Form of V,V;
cluster diagker f ->  non empty ;
coherence
 not diagker f is empty
proof
 f . ((0. V),(0. V)) = 0. K by Th33;
then  0. V in diagker f ;
hence  not diagker f is empty ; ::_thesis: verum
end;
end;

theorem :: BILINEAR:41
for K being ZeroStr
for V being non empty VectSpStr over K
for f being Form of V,V holds
( leftker f c= diagker f & rightker f c= diagker f )
proof
let K be ZeroStr ; ::_thesis: for V being non empty VectSpStr over K
for f being Form of V,V holds
( leftker f c= diagker f & rightker f c= diagker f )
let V be non empty VectSpStr over K; ::_thesis: for f being Form of V,V holds
( leftker f c= diagker f & rightker f c= diagker f )
let f be Form of V,V; ::_thesis: ( leftker f c= diagker f & rightker f c= diagker f )
thus  leftker f c= diagker f ::_thesis: rightker f c= diagker f
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in leftker f or x in diagker f )
assume  x in leftker f ; ::_thesis: x in diagker f
then consider v being Vector of V such that
A1: v = x and
A2: for w being Vector of V holds f . (v,w) = 0. K ;
 f . (v,v) = 0. K by A2;
hence  x in diagker f by A1; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rightker f or x in diagker f )
assume  x in rightker f ; ::_thesis: x in diagker f
then consider v being Vector of V such that
A3: v = x and
A4: for w being Vector of V holds f . (w,v) = 0. K ;
 f . (v,v) = 0. K by A4;
hence  x in diagker f by A3; ::_thesis: verum
end;

theorem Th42: :: BILINEAR:42
for K being non empty right_complementable add-associative right_zeroed right-distributive doubleLoopStr
for V, W being non empty VectSpStr over K
for f being additiveSAF homogeneousSAF Form of V,W holds leftker f is linearly-closed
proof
let K be non empty right_complementable add-associative right_zeroed right-distributive doubleLoopStr ; ::_thesis: for V, W being non empty VectSpStr over K
for f being additiveSAF homogeneousSAF Form of V,W holds leftker f is linearly-closed
let V, W be non empty VectSpStr over K; ::_thesis: for f being additiveSAF homogeneousSAF Form of V,W holds leftker f is linearly-closed
let f be additiveSAF homogeneousSAF Form of V,W; ::_thesis: leftker f is linearly-closed
set V1 = leftker f;
thus  for v, u being Vector of V st v in leftker f & u in leftker f holds
v + u in leftker f :: according to VECTSP_4:def_1 ::_thesis: for b1 being Element of the carrier of K
for b2 being Element of the carrier of V holds
( not b2 in leftker f or b1 * b2 in leftker f )
proof
let v, u be Vector of V; ::_thesis: ( v in leftker f & u in leftker f implies v + u in leftker f )
assume that
A1: v in leftker f and
A2: u in leftker f ; ::_thesis: v + u in leftker f
consider u1 being Vector of V such that
A3: u1 = u and
A4: for w being Vector of W holds f . (u1,w) = 0. K by A2;
consider v1 being Vector of V such that
A5: v1 = v and
A6: for w being Vector of W holds f . (v1,w) = 0. K by A1;
now__::_thesis:_for_w_being_Vector_of_W_holds_f_._((v_+_u),w)_=_0._K
let w be Vector of W; ::_thesis: f . ((v + u),w) = 0. K
thus f . ((v + u),w) = (f . (v1,w)) + (f . (u1,w)) by A5, A3, Th26
.= (0. K) + (f . (u1,w)) by A6
.= (0. K) + (0. K) by A4
.= 0. K by RLVECT_1:def_4 ; ::_thesis: verum
end;
hence  v + u in leftker f ; ::_thesis: verum
end;
let a be Element of K; ::_thesis: for b1 being Element of the carrier of V holds
( not b1 in leftker f or a * b1 in leftker f )
let v be Vector of V; ::_thesis: ( not v in leftker f or a * v in leftker f )
assume  v in leftker f ; ::_thesis: a * v in leftker f
then consider v1 being Vector of V such that
A7: v1 = v and
A8: for w being Vector of W holds f . (v1,w) = 0. K ;
now__::_thesis:_for_w_being_Vector_of_W_holds_f_._((a_*_v),w)_=_0._K
let w be Vector of W; ::_thesis: f . ((a * v),w) = 0. K
thus f . ((a * v),w) = a * (f . (v1,w)) by A7, Th31
.= a * (0. K) by A8
.= 0. K by VECTSP_1:6 ; ::_thesis: verum
end;
hence  a * v in leftker f ; ::_thesis: verum
end;

theorem Th43: :: BILINEAR:43
for K being non empty right_complementable add-associative right_zeroed right-distributive doubleLoopStr
for V, W being non empty VectSpStr over K
for f being additiveFAF homogeneousFAF Form of V,W holds rightker f is linearly-closed
proof
let K be non empty right_complementable add-associative right_zeroed right-distributive doubleLoopStr ; ::_thesis: for V, W being non empty VectSpStr over K
for f being additiveFAF homogeneousFAF Form of V,W holds rightker f is linearly-closed
let V, W be non empty VectSpStr over K; ::_thesis: for f being additiveFAF homogeneousFAF Form of V,W holds rightker f is linearly-closed
let f be additiveFAF homogeneousFAF Form of V,W; ::_thesis: rightker f is linearly-closed
set V1 = rightker f;
thus  for v, u being Vector of W st v in rightker f & u in rightker f holds
v + u in rightker f :: according to VECTSP_4:def_1 ::_thesis: for b1 being Element of the carrier of K
for b2 being Element of the carrier of W holds
( not b2 in rightker f or b1 * b2 in rightker f )
proof
let v, u be Vector of W; ::_thesis: ( v in rightker f & u in rightker f implies v + u in rightker f )
assume that
A1: v in rightker f and
A2: u in rightker f ; ::_thesis: v + u in rightker f
consider u1 being Vector of W such that
A3: u1 = u and
A4: for w being Vector of V holds f . (w,u1) = 0. K by A2;
consider v1 being Vector of W such that
A5: v1 = v and
A6: for w being Vector of V holds f . (w,v1) = 0. K by A1;
now__::_thesis:_for_w_being_Vector_of_V_holds_f_._(w,(v_+_u))_=_0._K
let w be Vector of V; ::_thesis: f . (w,(v + u)) = 0. K
thus f . (w,(v + u)) = (f . (w,v1)) + (f . (w,u1)) by A5, A3, Th27
.= (0. K) + (f . (w,u1)) by A6
.= (0. K) + (0. K) by A4
.= 0. K by RLVECT_1:def_4 ; ::_thesis: verum
end;
hence  v + u in rightker f ; ::_thesis: verum
end;
let a be Element of K; ::_thesis: for b1 being Element of the carrier of W holds
( not b1 in rightker f or a * b1 in rightker f )
let v be Vector of W; ::_thesis: ( not v in rightker f or a * v in rightker f )
assume  v in rightker f ; ::_thesis: a * v in rightker f
then consider v1 being Vector of W such that
A7: v1 = v and
A8: for w being Vector of V holds f . (w,v1) = 0. K ;
now__::_thesis:_for_w_being_Vector_of_V_holds_f_._(w,(a_*_v))_=_0._K
let w be Vector of V; ::_thesis: f . (w,(a * v)) = 0. K
thus f . (w,(a * v)) = a * (f . (w,v1)) by A7, Th32
.= a * (0. K) by A8
.= 0. K by VECTSP_1:6 ; ::_thesis: verum
end;
hence  a * v in rightker f ; ::_thesis: verum
end;

definition
let K be non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr ;
let V be VectSp of K;
let W be non empty VectSpStr over K;
let f be additiveSAF homogeneousSAF Form of V,W;
func LKer f ->  non empty strict Subspace of V means :Def18: :: BILINEAR:def 18
 the carrier of it = leftker f;
existence
 ex b1 being non empty strict Subspace of V st the carrier of b1 = leftker f by Th42, VECTSP_4:34;
uniqueness
 for b1, b2 being non empty strict Subspace of V st the carrier of b1 = leftker f & the carrier of b2 = leftker f holds
b1 = b2 by VECTSP_4:29;
end;

:: deftheorem Def18 defines LKer BILINEAR:def_18_:_
 for K being non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr
for V being VectSp of K
for W being non empty VectSpStr over K
for f being additiveSAF homogeneousSAF Form of V,W
for b5 being non empty strict Subspace of V holds
( b5 = LKer f iff the carrier of b5 = leftker f );

definition
let K be non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr ;
let V be non empty VectSpStr over K;
let W be VectSp of K;
let f be additiveFAF homogeneousFAF Form of V,W;
func RKer f ->  non empty strict Subspace of W means :Def19: :: BILINEAR:def 19
 the carrier of it = rightker f;
existence
 ex b1 being non empty strict Subspace of W st the carrier of b1 = rightker f by Th43, VECTSP_4:34;
uniqueness
 for b1, b2 being non empty strict Subspace of W st the carrier of b1 = rightker f & the carrier of b2 = rightker f holds
b1 = b2 by VECTSP_4:29;
end;

:: deftheorem Def19 defines RKer BILINEAR:def_19_:_
 for K being non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr
for V being non empty VectSpStr over K
for W being VectSp of K
for f being additiveFAF homogeneousFAF Form of V,W
for b5 being non empty strict Subspace of W holds
( b5 = RKer f iff the carrier of b5 = rightker f );

definition
let K be non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr ;
let V be VectSp of K;
let 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 :Def20: :: BILINEAR:def 20
 for A being Vector of (VectQuot (V,(LKer f)))
for w being Vector of W
for v being Vector of V st A = v + (LKer f) holds
it . (A,w) = f . (v,w);
existence
 ex b1 being additiveSAF homogeneousSAF Form of (VectQuot (V,(LKer f))),W st
for A being Vector of (VectQuot (V,(LKer f)))
for w being Vector of W
for v being Vector of V st A = v + (LKer f) holds
b1 . (A,w) = f . (v,w)
proof
set L = LKer f;
set vq = VectQuot (V,(LKer f));
set C = CosetSet (V,(LKer f));
set aC = addCoset (V,(LKer f));
set mC = lmultCoset (V,(LKer f));
defpred S1[ set , set , set ] means  for a being Vector of V st $1 = a + (LKer f) holds
$3 = f . (a,$2);
A1: now__::_thesis:_for_A_being_Vector_of_(VectQuot_(V,(LKer_f)))
for_w0_being_Vector_of_W_ex_y_being_Element_of_the_carrier_of_K_st_S1[A,w0,y]
let A be Vector of (VectQuot (V,(LKer f))); ::_thesis: for w0 being Vector of W ex y being Element of the carrier of K st S1[A,w0,y]
let w0 be Vector of W; ::_thesis: ex y being Element of the carrier of K st S1[A,w0,y]
consider a being Vector of V such that
A2: A = a + (LKer f) by VECTSP10:22;
take y = f . (a,w0); ::_thesis: S1[A,w0,y]
now__::_thesis:_for_a1_being_Vector_of_V_st_A_=_a1_+_(LKer_f)_holds_
y_=_f_._(a1,w0)
let a1 be Vector of V; ::_thesis: ( A = a1 + (LKer f) implies y = f . (a1,w0) )
assume  A = a1 + (LKer f) ; ::_thesis: y = f . (a1,w0)
then  a in a1 + (LKer f) by A2, VECTSP_4:44;
then consider w being Vector of V such that
A3: w in LKer f and
A4: a = a1 + w by VECTSP_4:42;
 w in the carrier of (LKer f) by A3, STRUCT_0:def_5;
then  w in leftker f by Def18;
then A5: ex aa being Vector of V st
( aa = w & ( for ww being Vector of W holds f . (aa,ww) = 0. K ) ) ;
thus y = (f . (a1,w0)) + (f . (w,w0)) by A4, Th26
.= (f . (a1,w0)) + (0. K) by A5
.= f . (a1,w0) by RLVECT_1:def_4 ; ::_thesis: verum
end;
hence  S1[A,w0,y] ; ::_thesis: verum
end;
consider ff being Function of [: the carrier of (VectQuot (V,(LKer f))), the carrier of W:], the carrier of K such that
A6: for A being Vector of (VectQuot (V,(LKer f)))
for w being Vector of W holds S1[A,w,ff . (A,w)] from BINOP_1:sch_3(A1);
reconsider ff = ff as Form of (VectQuot (V,(LKer f))),W ;
A7: CosetSet (V,(LKer f)) = the carrier of (VectQuot (V,(LKer f))) by VECTSP10:def_6;
now__::_thesis:_for_w_being_Vector_of_W_holds_FunctionalSAF_(ff,w)_is_additive
let w be Vector of W; ::_thesis: FunctionalSAF (ff,w) is additive
set ffw = FunctionalSAF (ff,w);
now__::_thesis:_for_A,_B_being_Vector_of_(VectQuot_(V,(LKer_f)))_holds_(FunctionalSAF_(ff,w))_._(A_+_B)_=_((FunctionalSAF_(ff,w))_._A)_+_((FunctionalSAF_(ff,w))_._B)
let A, B be Vector of (VectQuot (V,(LKer f))); ::_thesis: (FunctionalSAF (ff,w)) . (A + B) = ((FunctionalSAF (ff,w)) . A) + ((FunctionalSAF (ff,w)) . B)
consider a being Vector of V such that
A8: A = a + (LKer f) by VECTSP10:22;
consider b being Vector of V such that
A9: B = b + (LKer f) by VECTSP10:22;
A10: ( the addF of (VectQuot (V,(LKer f))) = addCoset (V,(LKer f)) & (addCoset (V,(LKer f))) . (A,B) = (a + b) + (LKer f) ) by A7, A8, A9, VECTSP10:def_3, VECTSP10:def_6;
thus (FunctionalSAF (ff,w)) . (A + B) = ff . ((A + B),w) by Th9
.= f . ((a + b),w) by A6, A10, RLVECT_1:2
.= (f . (a,w)) + (f . (b,w)) by Th26
.= (ff . (A,w)) + (f . (b,w)) by A6, A8
.= (ff . (A,w)) + (ff . (B,w)) by A6, A9
.= ((FunctionalSAF (ff,w)) . A) + (ff . (B,w)) by Th9
.= ((FunctionalSAF (ff,w)) . A) + ((FunctionalSAF (ff,w)) . B) by Th9 ; ::_thesis: verum
end;
hence  FunctionalSAF (ff,w) is additive by VECTSP_1:def_20; ::_thesis: verum
end;
then reconsider ff = ff as additiveSAF Form of (VectQuot (V,(LKer f))),W by Def12;
now__::_thesis:_for_w_being_Vector_of_W_holds_FunctionalSAF_(ff,w)_is_homogeneous
let w be Vector of W; ::_thesis: FunctionalSAF (ff,w) is homogeneous
set ffw = FunctionalSAF (ff,w);
now__::_thesis:_for_A_being_Vector_of_(VectQuot_(V,(LKer_f)))
for_r_being_Element_of_K_holds_(FunctionalSAF_(ff,w))_._(r_*_A)_=_r_*_((FunctionalSAF_(ff,w))_._A)
let A be Vector of (VectQuot (V,(LKer f))); ::_thesis: for r being Element of K holds (FunctionalSAF (ff,w)) . (r * A) = r * ((FunctionalSAF (ff,w)) . A)
let r be Element of K; ::_thesis: (FunctionalSAF (ff,w)) . (r * A) = r * ((FunctionalSAF (ff,w)) . A)
consider a being Vector of V such that
A11: A = a + (LKer f) by VECTSP10:22;
A12: ( the lmult of (VectQuot (V,(LKer f))) = lmultCoset (V,(LKer f)) & (lmultCoset (V,(LKer f))) . (r,A) = (r * a) + (LKer f) ) by A7, A11, VECTSP10:def_5, VECTSP10:def_6;
thus (FunctionalSAF (ff,w)) . (r * A) = ff . ((r * A),w) by Th9
.= f . ((r * a),w) by A6, A12
.= r * (f . (a,w)) by Th31
.= r * (ff . (A,w)) by A6, A11
.= r * ((FunctionalSAF (ff,w)) . A) by Th9 ; ::_thesis: verum
end;
hence  FunctionalSAF (ff,w) is homogeneous by HAHNBAN1:def_8; ::_thesis: verum
end;
then reconsider ff = ff as additiveSAF homogeneousSAF Form of (VectQuot (V,(LKer f))),W by Def14;
take  ff ; ::_thesis: for A being Vector of (VectQuot (V,(LKer f)))
for w being Vector of W
for v being Vector of V st A = v + (LKer f) holds
ff . (A,w) = f . (v,w)
thus  for A being Vector of (VectQuot (V,(LKer f)))
for w being Vector of W
for v being Vector of V st A = v + (LKer f) holds
ff . (A,w) = f . (v,w) by A6; ::_thesis: verum
end;
uniqueness
 for b1, b2 being additiveSAF homogeneousSAF Form of (VectQuot (V,(LKer f))),W st ( for A being Vector of (VectQuot (V,(LKer f)))
for w being Vector of W
for v being Vector of V st A = v + (LKer f) holds
b1 . (A,w) = f . (v,w) ) & ( for A being Vector of (VectQuot (V,(LKer f)))
for w being Vector of W
for v being Vector of V st A = v + (LKer f) holds
b2 . (A,w) = f . (v,w) ) holds
b1 = b2
proof
set L = LKer f;
set vq = VectQuot (V,(LKer f));
let f1, f2 be additiveSAF homogeneousSAF Form of (VectQuot (V,(LKer f))),W; ::_thesis: ( ( for A being Vector of (VectQuot (V,(LKer f)))
for w being Vector of W
for v being Vector of V st A = v + (LKer f) holds
f1 . (A,w) = f . (v,w) ) & ( for A being Vector of (VectQuot (V,(LKer f)))
for w being Vector of W
for v being Vector of V st A = v + (LKer f) holds
f2 . (A,w) = f . (v,w) ) implies f1 = f2 )
assume that
A13: for A being Vector of (VectQuot (V,(LKer f)))
for w being Vector of W
for a being Vector of V st A = a + (LKer f) holds
f1 . (A,w) = f . (a,w) and
A14: for A being Vector of (VectQuot (V,(LKer f)))
for w being Vector of W
for a being Vector of V st A = a + (LKer f) holds
f2 . (A,w) = f . (a,w) ; ::_thesis: f1 = f2
now__::_thesis:_for_A_being_Vector_of_(VectQuot_(V,(LKer_f)))
for_w_being_Vector_of_W_holds_f1_._(A,w)_=_f2_._(A,w)
let A be Vector of (VectQuot (V,(LKer f))); ::_thesis: for w being Vector of W holds f1 . (A,w) = f2 . (A,w)
let w be Vector of W; ::_thesis: f1 . (A,w) = f2 . (A,w)
consider a being Vector of V such that
A15: A = a + (LKer f) by VECTSP10:22;
thus f1 . (A,w) = f . (a,w) by A13, A15
.= f2 . (A,w) by A14, A15 ; ::_thesis: verum
end;
hence  f1 = f2 by BINOP_1:2; ::_thesis: verum
end;
end;

:: deftheorem Def20 defines LQForm BILINEAR:def_20_:_
 for K being non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr
for V being VectSp of K
for W being non empty VectSpStr over K
for f being additiveSAF homogeneousSAF Form of V,W
for b5 being additiveSAF homogeneousSAF Form of (VectQuot (V,(LKer f))),W holds
( b5 = LQForm f iff for A being Vector of (VectQuot (V,(LKer f)))
for w being Vector of W
for v being Vector of V st A = v + (LKer f) holds
b5 . (A,w) = f . (v,w) );

definition
let K be non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr ;
let V be non empty VectSpStr over K;
let 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 :Def21: :: BILINEAR:def 21
 for A being Vector of (VectQuot (W,(RKer f)))
for v being Vector of V
for w being Vector of W st A = w + (RKer f) holds
it . (v,A) = f . (v,w);
existence
 ex b1 being additiveFAF homogeneousFAF Form of V,(VectQuot (W,(RKer f))) st
for A being Vector of (VectQuot (W,(RKer f)))
for v being Vector of V
for w being Vector of W st A = w + (RKer f) holds
b1 . (v,A) = f . (v,w)
proof
set L = RKer f;
set vq = VectQuot (W,(RKer f));
set C = CosetSet (W,(RKer f));
set aC = addCoset (W,(RKer f));
set mC = lmultCoset (W,(RKer f));
defpred S1[ set , set , set ] means  for w being Vector of W st $2 = w + (RKer f) holds
$3 = f . ($1,w);
A1: now__::_thesis:_for_v0_being_Vector_of_V
for_A_being_Vector_of_(VectQuot_(W,(RKer_f)))_ex_y_being_Element_of_the_carrier_of_K_st_S1[v0,A,y]
let v0 be Vector of V; ::_thesis: for A being Vector of (VectQuot (W,(RKer f))) ex y being Element of the carrier of K st S1[v0,A,y]
let A be Vector of (VectQuot (W,(RKer f))); ::_thesis: ex y being Element of the carrier of K st S1[v0,A,y]
consider a being Vector of W such that
A2: A = a + (RKer f) by VECTSP10:22;
take y = f . (v0,a); ::_thesis: S1[v0,A,y]
now__::_thesis:_for_a1_being_Vector_of_W_st_A_=_a1_+_(RKer_f)_holds_
y_=_f_._(v0,a1)
let a1 be Vector of W; ::_thesis: ( A = a1 + (RKer f) implies y = f . (v0,a1) )
assume  A = a1 + (RKer f) ; ::_thesis: y = f . (v0,a1)
then  a in a1 + (RKer f) by A2, VECTSP_4:44;
then consider w being Vector of W such that
A3: w in RKer f and
A4: a = a1 + w by VECTSP_4:42;
 w in the carrier of (RKer f) by A3, STRUCT_0:def_5;
then  w in rightker f by Def19;
then A5: ex aa being Vector of W st
( aa = w & ( for vv being Vector of V holds f . (vv,aa) = 0. K ) ) ;
thus y = (f . (v0,a1)) + (f . (v0,w)) by A4, Th27
.= (f . (v0,a1)) + (0. K) by A5
.= f . (v0,a1) by RLVECT_1:def_4 ; ::_thesis: verum
end;
hence  S1[v0,A,y] ; ::_thesis: verum
end;
consider ff being Function of [: the carrier of V, the carrier of (VectQuot (W,(RKer f))):], the carrier of K such that
A6: for v being Vector of V
for A being Vector of (VectQuot (W,(RKer f))) holds S1[v,A,ff . (v,A)] from BINOP_1:sch_3(A1);
reconsider ff = ff as Form of V,(VectQuot (W,(RKer f))) ;
A7: CosetSet (W,(RKer f)) = the carrier of (VectQuot (W,(RKer f))) by VECTSP10:def_6;
now__::_thesis:_for_v_being_Vector_of_V_holds_FunctionalFAF_(ff,v)_is_additive
let v be Vector of V; ::_thesis: FunctionalFAF (ff,v) is additive
set ffw = FunctionalFAF (ff,v);
now__::_thesis:_for_A,_B_being_Vector_of_(VectQuot_(W,(RKer_f)))_holds_(FunctionalFAF_(ff,v))_._(A_+_B)_=_((FunctionalFAF_(ff,v))_._A)_+_((FunctionalFAF_(ff,v))_._B)
let A, B be Vector of (VectQuot (W,(RKer f))); ::_thesis: (FunctionalFAF (ff,v)) . (A + B) = ((FunctionalFAF (ff,v)) . A) + ((FunctionalFAF (ff,v)) . B)
consider a being Vector of W such that
A8: A = a + (RKer f) by VECTSP10:22;
consider b being Vector of W such that
A9: B = b + (RKer f) by VECTSP10:22;
A10: ( the addF of (VectQuot (W,(RKer f))) = addCoset (W,(RKer f)) & (addCoset (W,(RKer f))) . (A,B) = (a + b) + (RKer f) ) by A7, A8, A9, VECTSP10:def_3, VECTSP10:def_6;
thus (FunctionalFAF (ff,v)) . (A + B) = ff . (v,(A + B)) by Th8
.= f . (v,(a + b)) by A6, A10, RLVECT_1:2
.= (f . (v,a)) + (f . (v,b)) by Th27
.= (ff . (v,A)) + (f . (v,b)) by A6, A8
.= (ff . (v,A)) + (ff . (v,B)) by A6, A9
.= ((FunctionalFAF (ff,v)) . A) + (ff . (v,B)) by Th8
.= ((FunctionalFAF (ff,v)) . A) + ((FunctionalFAF (ff,v)) . B) by Th8 ; ::_thesis: verum
end;
hence  FunctionalFAF (ff,v) is additive by VECTSP_1:def_20; ::_thesis: verum
end;
then reconsider ff = ff as additiveFAF Form of V,(VectQuot (W,(RKer f))) by Def11;
now__::_thesis:_for_v_being_Vector_of_V_holds_FunctionalFAF_(ff,v)_is_homogeneous
let v be Vector of V; ::_thesis: FunctionalFAF (ff,v) is homogeneous
set ffw = FunctionalFAF (ff,v);
now__::_thesis:_for_A_being_Vector_of_(VectQuot_(W,(RKer_f)))
for_r_being_Element_of_K_holds_(FunctionalFAF_(ff,v))_._(r_*_A)_=_r_*_((FunctionalFAF_(ff,v))_._A)
let A be Vector of (VectQuot (W,(RKer f))); ::_thesis: for r being Element of K holds (FunctionalFAF (ff,v)) . (r * A) = r * ((FunctionalFAF (ff,v)) . A)
let r be Element of K; ::_thesis: (FunctionalFAF (ff,v)) . (r * A) = r * ((FunctionalFAF (ff,v)) . A)
consider a being Vector of W such that
A11: A = a + (RKer f) by VECTSP10:22;
A12: ( the lmult of (VectQuot (W,(RKer f))) = lmultCoset (W,(RKer f)) & (lmultCoset (W,(RKer f))) . (r,A) = (r * a) + (RKer f) ) by A7, A11, VECTSP10:def_5, VECTSP10:def_6;
thus (FunctionalFAF (ff,v)) . (r * A) = ff . (v,(r * A)) by Th8
.= f . (v,(r * a)) by A6, A12
.= r * (f . (v,a)) by Th32
.= r * (ff . (v,A)) by A6, A11
.= r * ((FunctionalFAF (ff,v)) . A) by Th8 ; ::_thesis: verum
end;
hence  FunctionalFAF (ff,v) is homogeneous by HAHNBAN1:def_8; ::_thesis: verum
end;
then reconsider ff = ff as additiveFAF homogeneousFAF Form of V,(VectQuot (W,(RKer f))) by Def13;
take  ff ; ::_thesis: for A being Vector of (VectQuot (W,(RKer f)))
for v being Vector of V
for w being Vector of W st A = w + (RKer f) holds
ff . (v,A) = f . (v,w)
thus  for A being Vector of (VectQuot (W,(RKer f)))
for v being Vector of V
for w being Vector of W st A = w + (RKer f) holds
ff . (v,A) = f . (v,w) by A6; ::_thesis: verum
end;
uniqueness
 for b1, b2 being additiveFAF homogeneousFAF Form of V,(VectQuot (W,(RKer f))) st ( for A being Vector of (VectQuot (W,(RKer f)))
for v being Vector of V
for w being Vector of W st A = w + (RKer f) holds
b1 . (v,A) = f . (v,w) ) & ( for A being Vector of (VectQuot (W,(RKer f)))
for v being Vector of V
for w being Vector of W st A = w + (RKer f) holds
b2 . (v,A) = f . (v,w) ) holds
b1 = b2
proof
set L = RKer f;
set vq = VectQuot (W,(RKer f));
let f1, f2 be additiveFAF homogeneousFAF Form of V,(VectQuot (W,(RKer f))); ::_thesis: ( ( for A being Vector of (VectQuot (W,(RKer f)))
for v being Vector of V
for w being Vector of W st A = w + (RKer f) holds
f1 . (v,A) = f . (v,w) ) & ( for A being Vector of (VectQuot (W,(RKer f)))
for v being Vector of V
for w being Vector of W st A = w + (RKer f) holds
f2 . (v,A) = f . (v,w) ) implies f1 = f2 )
assume that
A13: for A being Vector of (VectQuot (W,(RKer f)))
for v being Vector of V
for a being Vector of W st A = a + (RKer f) holds
f1 . (v,A) = f . (v,a) and
A14: for A being Vector of (VectQuot (W,(RKer f)))
for v being Vector of V
for a being Vector of W st A = a + (RKer f) holds
f2 . (v,A) = f . (v,a) ; ::_thesis: f1 = f2
now__::_thesis:_for_v_being_Vector_of_V
for_A_being_Vector_of_(VectQuot_(W,(RKer_f)))_holds_f1_._(v,A)_=_f2_._(v,A)
let v be Vector of V; ::_thesis: for A being Vector of (VectQuot (W,(RKer f))) holds f1 . (v,A) = f2 . (v,A)
let A be Vector of (VectQuot (W,(RKer f))); ::_thesis: f1 . (v,A) = f2 . (v,A)
consider a being Vector of W such that
A15: A = a + (RKer f) by VECTSP10:22;
thus f1 . (v,A) = f . (v,a) by A13, A15
.= f2 . (v,A) by A14, A15 ; ::_thesis: verum
end;
hence  f1 = f2 by BINOP_1:2; ::_thesis: verum
end;
end;

:: deftheorem Def21 defines RQForm BILINEAR:def_21_:_
 for K being non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr
for V being non empty VectSpStr over K
for W being VectSp of K
for f being additiveFAF homogeneousFAF Form of V,W
for b5 being additiveFAF homogeneousFAF Form of V,(VectQuot (W,(RKer f))) holds
( b5 = RQForm f iff for A being Vector of (VectQuot (W,(RKer f)))
for v being Vector of V
for w being Vector of W st A = w + (RKer f) holds
b5 . (v,A) = f . (v,w) );

registration
let K be non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr ;
let V, W be VectSp of K;
let f be bilinear-Form of V,W;
cluster LQForm f ->  additiveFAF additiveSAF homogeneousFAF homogeneousSAF ;
coherence
 ( LQForm f is additiveFAF & LQForm f is homogeneousFAF )
proof
set lf = LQForm f;
thus  LQForm f is additiveFAF ::_thesis: LQForm f is homogeneousFAF
proof
let A be Vector of (VectQuot (V,(LKer f))); :: according to BILINEAR:def_11 ::_thesis: FunctionalFAF ((LQForm f),A) is additive
set flf = FunctionalFAF ((LQForm f),A);
consider v being Vector of V such that
A1: A = v + (LKer f) by VECTSP10:22;
let w, t be Vector of W; :: according to VECTSP_1:def_20 ::_thesis: (FunctionalFAF ((LQForm f),A)) . (w + t) = ((FunctionalFAF ((LQForm f),A)) . w) + ((FunctionalFAF ((LQForm f),A)) . t)
thus (FunctionalFAF ((LQForm f),A)) . (w + t) = (LQForm f) . (A,(w + t)) by Th8
.= f . (v,(w + t)) by A1, Def20
.= (f . (v,w)) + (f . (v,t)) by Th27
.= ((LQForm f) . (A,w)) + (f . (v,t)) by A1, Def20
.= ((LQForm f) . (A,w)) + ((LQForm f) . (A,t)) by A1, Def20
.= ((FunctionalFAF ((LQForm f),A)) . w) + ((LQForm f) . (A,t)) by Th8
.= ((FunctionalFAF ((LQForm f),A)) . w) + ((FunctionalFAF ((LQForm f),A)) . t) by Th8 ; ::_thesis: verum
end;
let A be Vector of (VectQuot (V,(LKer f))); :: according to BILINEAR:def_13 ::_thesis: FunctionalFAF ((LQForm f),A) is homogeneous
set flf = FunctionalFAF ((LQForm f),A);
consider v being Vector of V such that
A2: A = v + (LKer f) by VECTSP10:22;
let w be Vector of W; :: according to HAHNBAN1:def_8 ::_thesis: for b1 being Element of the carrier of K holds (FunctionalFAF ((LQForm f),A)) . (b1 * w) = b1 * ((FunctionalFAF ((LQForm f),A)) . w)
let r be Scalar of ; ::_thesis: (FunctionalFAF ((LQForm f),A)) . (r * w) = r * ((FunctionalFAF ((LQForm f),A)) . w)
thus (FunctionalFAF ((LQForm f),A)) . (r * w) = (LQForm f) . (A,(r * w)) by Th8
.= f . (v,(r * w)) by A2, Def20
.= r * (f . (v,w)) by Th32
.= r * ((LQForm f) . (A,w)) by A2, Def20
.= r * ((FunctionalFAF ((LQForm f),A)) . w) by Th8 ; ::_thesis: verum
end;
cluster RQForm f ->  additiveFAF additiveSAF homogeneousFAF homogeneousSAF ;
coherence
 ( RQForm f is additiveSAF & RQForm f is homogeneousSAF )
proof
set lf = RQForm f;
thus  RQForm f is additiveSAF ::_thesis: RQForm f is homogeneousSAF
proof
let A be Vector of (VectQuot (W,(RKer f))); :: according to BILINEAR:def_12 ::_thesis: FunctionalSAF ((RQForm f),A) is additive
set flf = FunctionalSAF ((RQForm f),A);
consider w being Vector of W such that
A3: A = w + (RKer f) by VECTSP10:22;
let v, t be Vector of V; :: according to VECTSP_1:def_20 ::_thesis: (FunctionalSAF ((RQForm f),A)) . (v + t) = ((FunctionalSAF ((RQForm f),A)) . v) + ((FunctionalSAF ((RQForm f),A)) . t)
thus (FunctionalSAF ((RQForm f),A)) . (v + t) = (RQForm f) . ((v + t),A) by Th9
.= f . ((v + t),w) by A3, Def21
.= (f . (v,w)) + (f . (t,w)) by Th26
.= ((RQForm f) . (v,A)) + (f . (t,w)) by A3, Def21
.= ((RQForm f) . (v,A)) + ((RQForm f) . (t,A)) by A3, Def21
.= ((FunctionalSAF ((RQForm f),A)) . v) + ((RQForm f) . (t,A)) by Th9
.= ((FunctionalSAF ((RQForm f),A)) . v) + ((FunctionalSAF ((RQForm f),A)) . t) by Th9 ; ::_thesis: verum
end;
let A be Vector of (VectQuot (W,(RKer f))); :: according to BILINEAR:def_14 ::_thesis: FunctionalSAF ((RQForm f),A) is homogeneous
set flf = FunctionalSAF ((RQForm f),A);
consider w being Vector of W such that
A4: A = w + (RKer f) by VECTSP10:22;
let v be Vector of V; :: according to HAHNBAN1:def_8 ::_thesis: for b1 being Element of the carrier of K holds (FunctionalSAF ((RQForm f),A)) . (b1 * v) = b1 * ((FunctionalSAF ((RQForm f),A)) . v)
let r be Scalar of ; ::_thesis: (FunctionalSAF ((RQForm f),A)) . (r * v) = r * ((FunctionalSAF ((RQForm f),A)) . v)
thus (FunctionalSAF ((RQForm f),A)) . (r * v) = (RQForm f) . ((r * v),A) by Th9
.= f . ((r * v),w) by A4, Def21
.= r * (f . (v,w)) by Th31
.= r * ((RQForm f) . (v,A)) by A4, Def21
.= r * ((FunctionalSAF ((RQForm f),A)) . v) by Th9 ; ::_thesis: verum
end;
end;

definition
let K be non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive 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 :Def22: :: BILINEAR:def 22
 for A being Vector of (VectQuot (V,(LKer f)))
for B being Vector of (VectQuot (W,(RKer f)))
for v being Vector of V
for w being Vector of W st A = v + (LKer f) & B = w + (RKer f) holds
it . (A,B) = f . (v,w);
existence
 ex b1 being bilinear-Form of (VectQuot (V,(LKer f))),(VectQuot (W,(RKer f))) st
for A being Vector of (VectQuot (V,(LKer f)))
for B being Vector of (VectQuot (W,(RKer f)))
for v being Vector of V
for w being Vector of W st A = v + (LKer f) & B = w + (RKer f) holds
b1 . (A,B) = f . (v,w)
proof
set L = LKer f;
set vq = VectQuot (V,(LKer f));
set Cv = CosetSet (V,(LKer f));
set aCv = addCoset (V,(LKer f));
set mCv = lmultCoset (V,(LKer f));
set R = RKer f;
set wq = VectQuot (W,(RKer f));
set Cw = CosetSet (W,(RKer f));
set aCw = addCoset (W,(RKer f));
set mCw = lmultCoset (W,(RKer f));
defpred S1[ set , set , set ] means  for v being Vector of V
for w being Vector of W st $1 = v + (LKer f) & $2 = w + (RKer f) holds
$3 = f . (v,w);
A1: now__::_thesis:_for_A_being_Vector_of_(VectQuot_(V,(LKer_f)))
for_B_being_Vector_of_(VectQuot_(W,(RKer_f)))_ex_y_being_Element_of_the_carrier_of_K_st_S1[A,B,y]
let A be Vector of (VectQuot (V,(LKer f))); ::_thesis: for B being Vector of (VectQuot (W,(RKer f))) ex y being Element of the carrier of K st S1[A,B,y]
let B be Vector of (VectQuot (W,(RKer f))); ::_thesis: ex y being Element of the carrier of K st S1[A,B,y]
consider a being Vector of V such that
A2: A = a + (LKer f) by VECTSP10:22;
consider b being Vector of W such that
A3: B = b + (RKer f) by VECTSP10:22;
take y = f . (a,b); ::_thesis: S1[A,B,y]
now__::_thesis:_for_a1_being_Vector_of_V
for_b1_being_Vector_of_W_st_A_=_a1_+_(LKer_f)_&_B_=_b1_+_(RKer_f)_holds_
y_=_f_._(a1,b1)
let a1 be Vector of V; ::_thesis: for b1 being Vector of W st A = a1 + (LKer f) & B = b1 + (RKer f) holds
y = f . (a1,b1)
let b1 be Vector of W; ::_thesis: ( A = a1 + (LKer f) & B = b1 + (RKer f) implies y = f . (a1,b1) )
assume  A = a1 + (LKer f) ; ::_thesis: ( B = b1 + (RKer f) implies y = f . (a1,b1) )
then  a in a1 + (LKer f) by A2, VECTSP_4:44;
then consider vv being Vector of V such that
A4: vv in LKer f and
A5: a = a1 + vv by VECTSP_4:42;
 vv in the carrier of (LKer f) by A4, STRUCT_0:def_5;
then  vv in leftker f by Def18;
then A6: ex aa being Vector of V st
( aa = vv & ( for w0 being Vector of W holds f . (aa,w0) = 0. K ) ) ;
assume  B = b1 + (RKer f) ; ::_thesis: y = f . (a1,b1)
then  b in b1 + (RKer f) by A3, VECTSP_4:44;
then consider ww being Vector of W such that
A7: ww in RKer f and
A8: b = b1 + ww by VECTSP_4:42;
 ww in the carrier of (RKer f) by A7, STRUCT_0:def_5;
then  ww in rightker f by Def19;
then A9: ex bb being Vector of W st
( bb = ww & ( for v0 being Vector of V holds f . (v0,bb) = 0. K ) ) ;
thus y = ((f . (a1,b1)) + (f . (a1,ww))) + ((f . (vv,b1)) + (f . (vv,ww))) by A5, A8, Th28
.= ((f . (a1,b1)) + (0. K)) + ((f . (vv,b1)) + (f . (vv,ww))) by A9
.= ((f . (a1,b1)) + (0. K)) + ((0. K) + (f . (vv,ww))) by A6
.= (f . (a1,b1)) + ((0. K) + (f . (vv,ww))) by RLVECT_1:def_4
.= (f . (a1,b1)) + (f . (vv,ww)) by RLVECT_1:4
.= (f . (a1,b1)) + (0. K) by A6
.= f . (a1,b1) by RLVECT_1:def_4 ; ::_thesis: verum
end;
hence  S1[A,B,y] ; ::_thesis: verum
end;
consider ff being Function of [: the carrier of (VectQuot (V,(LKer f))), the carrier of (VectQuot (W,(RKer f))):], the carrier of K such that
A10: for A being Vector of (VectQuot (V,(LKer f)))
for B being Vector of (VectQuot (W,(RKer f))) holds S1[A,B,ff . (A,B)] from BINOP_1:sch_3(A1);
reconsider ff = ff as Form of (VectQuot (V,(LKer f))),(VectQuot (W,(RKer f))) ;
A11: CosetSet (V,(LKer f)) = the carrier of (VectQuot (V,(LKer f))) by VECTSP10:def_6;
A12: now__::_thesis:_for_ww_being_Vector_of_(VectQuot_(W,(RKer_f)))_holds_FunctionalSAF_(ff,ww)_is_homogeneous
let ww be Vector of (VectQuot (W,(RKer f))); ::_thesis: FunctionalSAF (ff,ww) is homogeneous
consider w being Vector of W such that
A13: ww = w + (RKer f) by VECTSP10:22;
set ffw = FunctionalSAF (ff,ww);
now__::_thesis:_for_A_being_Vector_of_(VectQuot_(V,(LKer_f)))
for_r_being_Element_of_K_holds_(FunctionalSAF_(ff,ww))_._(r_*_A)_=_r_*_((FunctionalSAF_(ff,ww))_._A)
let A be Vector of (VectQuot (V,(LKer f))); ::_thesis: for r being Element of K holds (FunctionalSAF (ff,ww)) . (r * A) = r * ((FunctionalSAF (ff,ww)) . A)
let r be Element of K; ::_thesis: (FunctionalSAF (ff,ww)) . (r * A) = r * ((FunctionalSAF (ff,ww)) . A)
consider a being Vector of V such that
A14: A = a + (LKer f) by VECTSP10:22;
A15: ( the lmult of (VectQuot (V,(LKer f))) = lmultCoset (V,(LKer f)) & (lmultCoset (V,(LKer f))) . (r,A) = (r * a) + (LKer f) ) by A11, A14, VECTSP10:def_5, VECTSP10:def_6;
thus (FunctionalSAF (ff,ww)) . (r * A) = ff . ((r * A),ww) by Th9
.= f . ((r * a),w) by A10, A13, A15
.= r * (f . (a,w)) by Th31
.= r * (ff . (A,ww)) by A10, A13, A14
.= r * ((FunctionalSAF (ff,ww)) . A) by Th9 ; ::_thesis: verum
end;
hence  FunctionalSAF (ff,ww) is homogeneous by HAHNBAN1:def_8; ::_thesis: verum
end;
A16: CosetSet (W,(RKer f)) = the carrier of (VectQuot (W,(RKer f))) by VECTSP10:def_6;
A17: now__::_thesis:_for_vv_being_Vector_of_(VectQuot_(V,(LKer_f)))_holds_FunctionalFAF_(ff,vv)_is_homogeneous
let vv be Vector of (VectQuot (V,(LKer f))); ::_thesis: FunctionalFAF (ff,vv) is homogeneous
consider v being Vector of V such that
A18: vv = v + (LKer f) by VECTSP10:22;
set ffv = FunctionalFAF (ff,vv);
now__::_thesis:_for_A_being_Vector_of_(VectQuot_(W,(RKer_f)))
for_r_being_Element_of_K_holds_(FunctionalFAF_(ff,vv))_._(r_*_A)_=_r_*_((FunctionalFAF_(ff,vv))_._A)
let A be Vector of (VectQuot (W,(RKer f))); ::_thesis: for r being Element of K holds (FunctionalFAF (ff,vv)) . (r * A) = r * ((FunctionalFAF (ff,vv)) . A)
let r be Element of K; ::_thesis: (FunctionalFAF (ff,vv)) . (r * A) = r * ((FunctionalFAF (ff,vv)) . A)
consider a being Vector of W such that
A19: A = a + (RKer f) by VECTSP10:22;
A20: ( the lmult of (VectQuot (W,(RKer f))) = lmultCoset (W,(RKer f)) & (lmultCoset (W,(RKer f))) . (r,A) = (r * a) + (RKer f) ) by A16, A19, VECTSP10:def_5, VECTSP10:def_6;
thus (FunctionalFAF (ff,vv)) . (r * A) = ff . (vv,(r * A)) by Th8
.= f . (v,(r * a)) by A10, A18, A20
.= r * (f . (v,a)) by Th32
.= r * (ff . (vv,A)) by A10, A18, A19
.= r * ((FunctionalFAF (ff,vv)) . A) by Th8 ; ::_thesis: verum
end;
hence  FunctionalFAF (ff,vv) is homogeneous by HAHNBAN1:def_8; ::_thesis: verum
end;
A21: now__::_thesis:_for_ww_being_Vector_of_(VectQuot_(W,(RKer_f)))_holds_FunctionalSAF_(ff,ww)_is_additive
let ww be Vector of (VectQuot (W,(RKer f))); ::_thesis: FunctionalSAF (ff,ww) is additive
consider w being Vector of W such that
A22: ww = w + (RKer f) by VECTSP10:22;
set ffw = FunctionalSAF (ff,ww);
now__::_thesis:_for_A,_B_being_Vector_of_(VectQuot_(V,(LKer_f)))_holds_(FunctionalSAF_(ff,ww))_._(A_+_B)_=_((FunctionalSAF_(ff,ww))_._A)_+_((FunctionalSAF_(ff,ww))_._B)
let A, B be Vector of (VectQuot (V,(LKer f))); ::_thesis: (FunctionalSAF (ff,ww)) . (A + B) = ((FunctionalSAF (ff,ww)) . A) + ((FunctionalSAF (ff,ww)) . B)
consider a being Vector of V such that
A23: A = a + (LKer f) by VECTSP10:22;
consider b being Vector of V such that
A24: B = b + (LKer f) by VECTSP10:22;
A25: ( the addF of (VectQuot (V,(LKer f))) = addCoset (V,(LKer f)) & (addCoset (V,(LKer f))) . (A,B) = (a + b) + (LKer f) ) by A11, A23, A24, VECTSP10:def_3, VECTSP10:def_6;
thus (FunctionalSAF (ff,ww)) . (A + B) = ff . ((A + B),ww) by Th9
.= f . ((a + b),w) by A10, A22, A25, RLVECT_1:2
.= (f . (a,w)) + (f . (b,w)) by Th26
.= (ff . (A,ww)) + (f . (b,w)) by A10, A22, A23
.= (ff . (A,ww)) + (ff . (B,ww)) by A10, A22, A24
.= ((FunctionalSAF (ff,ww)) . A) + (ff . (B,ww)) by Th9
.= ((FunctionalSAF (ff,ww)) . A) + ((FunctionalSAF (ff,ww)) . B) by Th9 ; ::_thesis: verum
end;
hence  FunctionalSAF (ff,ww) is additive by VECTSP_1:def_20; ::_thesis: verum
end;
now__::_thesis:_for_vv_being_Vector_of_(VectQuot_(V,(LKer_f)))_holds_FunctionalFAF_(ff,vv)_is_additive
let vv be Vector of (VectQuot (V,(LKer f))); ::_thesis: FunctionalFAF (ff,vv) is additive
consider v being Vector of V such that
A26: vv = v + (LKer f) by VECTSP10:22;
set ffv = FunctionalFAF (ff,vv);
now__::_thesis:_for_A,_B_being_Vector_of_(VectQuot_(W,(RKer_f)))_holds_(FunctionalFAF_(ff,vv))_._(A_+_B)_=_((FunctionalFAF_(ff,vv))_._A)_+_((FunctionalFAF_(ff,vv))_._B)
let A, B be Vector of (VectQuot (W,(RKer f))); ::_thesis: (FunctionalFAF (ff,vv)) . (A + B) = ((FunctionalFAF (ff,vv)) . A) + ((FunctionalFAF (ff,vv)) . B)
consider a being Vector of W such that
A27: A = a + (RKer f) by VECTSP10:22;
consider b being Vector of W such that
A28: B = b + (RKer f) by VECTSP10:22;
A29: ( the addF of (VectQuot (W,(RKer f))) = addCoset (W,(RKer f)) & (addCoset (W,(RKer f))) . (A,B) = (a + b) + (RKer f) ) by A16, A27, A28, VECTSP10:def_3, VECTSP10:def_6;
thus (FunctionalFAF (ff,vv)) . (A + B) = ff . (vv,(A + B)) by Th8
.= f . (v,(a + b)) by A10, A26, A29, RLVECT_1:2
.= (f . (v,a)) + (f . (v,b)) by Th27
.= (ff . (vv,A)) + (f . (v,b)) by A10, A26, A27
.= (ff . (vv,A)) + (ff . (vv,B)) by A10, A26, A28
.= ((FunctionalFAF (ff,vv)) . A) + (ff . (vv,B)) by Th8
.= ((FunctionalFAF (ff,vv)) . A) + ((FunctionalFAF (ff,vv)) . B) by Th8 ; ::_thesis: verum
end;
hence  FunctionalFAF (ff,vv) is additive by VECTSP_1:def_20; ::_thesis: verum
end;
then reconsider ff = ff as bilinear-Form of (VectQuot (V,(LKer f))),(VectQuot (W,(RKer f))) by A21, A12, A17, Def11, Def12, Def13, Def14;
take  ff ; ::_thesis: for A being Vector of (VectQuot (V,(LKer f)))
for B being Vector of (VectQuot (W,(RKer f)))
for v being Vector of V
for w being Vector of W st A = v + (LKer f) & B = w + (RKer f) holds
ff . (A,B) = f . (v,w)
thus  for A being Vector of (VectQuot (V,(LKer f)))
for B being Vector of (VectQuot (W,(RKer f)))
for v being Vector of V
for w being Vector of W st A = v + (LKer f) & B = w + (RKer f) holds
ff . (A,B) = f . (v,w) by A10; ::_thesis: verum
end;
uniqueness
 for b1, b2 being bilinear-Form of (VectQuot (V,(LKer f))),(VectQuot (W,(RKer f))) st ( for A being Vector of (VectQuot (V,(LKer f)))
for B being Vector of (VectQuot (W,(RKer f)))
for v being Vector of V
for w being Vector of W st A = v + (LKer f) & B = w + (RKer f) holds
b1 . (A,B) = f . (v,w) ) & ( for A being Vector of (VectQuot (V,(LKer f)))
for B being Vector of (VectQuot (W,(RKer f)))
for v being Vector of V
for w being Vector of W st A = v + (LKer f) & B = w + (RKer f) holds
b2 . (A,B) = f . (v,w) ) holds
b1 = b2
proof
set L = LKer f;
set vq = VectQuot (V,(LKer f));
set R = RKer f;
set wq = VectQuot (W,(RKer f));
let f1, f2 be bilinear-Form of (VectQuot (V,(LKer f))),(VectQuot (W,(RKer f))); ::_thesis: ( ( for A being Vector of (VectQuot (V,(LKer f)))
for B being Vector of (VectQuot (W,(RKer f)))
for v being Vector of V
for w being Vector of W st A = v + (LKer f) & B = w + (RKer f) holds
f1 . (A,B) = f . (v,w) ) & ( for A being Vector of (VectQuot (V,(LKer f)))
for B being Vector of (VectQuot (W,(RKer f)))
for v being Vector of V
for w being Vector of W st A = v + (LKer f) & B = w + (RKer f) holds
f2 . (A,B) = f . (v,w) ) implies f1 = f2 )
assume that
A30: for A being Vector of (VectQuot (V,(LKer f)))
for B being Vector of (VectQuot (W,(RKer f)))
for v being Vector of V
for w being Vector of W st A = v + (LKer f) & B = w + (RKer f) holds
f1 . (A,B) = f . (v,w) and
A31: for A being Vector of (VectQuot (V,(LKer f)))
for B being Vector of (VectQuot (W,(RKer f)))
for v being Vector of V
for w being Vector of W st A = v + (LKer f) & B = w + (RKer f) holds
f2 . (A,B) = f . (v,w) ; ::_thesis: f1 = f2
now__::_thesis:_for_A_being_Vector_of_(VectQuot_(V,(LKer_f)))
for_B_being_Vector_of_(VectQuot_(W,(RKer_f)))_holds_f1_._(A,B)_=_f2_._(A,B)
let A be Vector of (VectQuot (V,(LKer f))); ::_thesis: for B being Vector of (VectQuot (W,(RKer f))) holds f1 . (A,B) = f2 . (A,B)
let B be Vector of (VectQuot (W,(RKer f))); ::_thesis: f1 . (A,B) = f2 . (A,B)
consider a being Vector of V such that
A32: A = a + (LKer f) by VECTSP10:22;
consider b being Vector of W such that
A33: B = b + (RKer f) by VECTSP10:22;
thus f1 . (A,B) = f . (a,b) by A30, A32, A33
.= f2 . (A,B) by A31, A32, A33 ; ::_thesis: verum
end;
hence  f1 = f2 by BINOP_1:2; ::_thesis: verum
end;
end;

:: deftheorem Def22 defines QForm BILINEAR:def_22_:_
 for K being non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr
for V, W being VectSp of K
for f being bilinear-Form of V,W
for b5 being bilinear-Form of (VectQuot (V,(LKer f))),(VectQuot (W,(RKer f))) holds
( b5 = QForm f iff for A being Vector of (VectQuot (V,(LKer f)))
for B being Vector of (VectQuot (W,(RKer f)))
for v being Vector of V
for w being Vector of W st A = v + (LKer f) & B = w + (RKer f) holds
b5 . (A,B) = f . (v,w) );

theorem Th44: :: BILINEAR:44
for K being non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr
for V being VectSp of K
for W being non empty VectSpStr over K
for f being additiveSAF homogeneousSAF Form of V,W holds rightker f = rightker (LQForm f)
proof
let K be non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr ; ::_thesis: for V being VectSp of K
for W being non empty VectSpStr over K
for f being additiveSAF homogeneousSAF Form of V,W holds rightker f = rightker (LQForm f)
let V be VectSp of K; ::_thesis: for W being non empty VectSpStr over K
for f being additiveSAF homogeneousSAF Form of V,W holds rightker f = rightker (LQForm f)
let W be non empty VectSpStr over K; ::_thesis: for f being additiveSAF homogeneousSAF Form of V,W holds rightker f = rightker (LQForm f)
let f be additiveSAF homogeneousSAF Form of V,W; ::_thesis: rightker f = rightker (LQForm f)
set lf = LQForm f;
set qv = VectQuot (V,(LKer f));
thus  rightker f c= rightker (LQForm f) :: according to XBOOLE_0:def_10 ::_thesis: rightker (LQForm f) c= rightker f
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rightker f or x in rightker (LQForm f) )
assume  x in rightker f ; ::_thesis: x in rightker (LQForm f)
then consider w being Vector of W such that
A1: x = w and
A2: for v being Vector of V holds f . (v,w) = 0. K ;
now__::_thesis:_for_A_being_Vector_of_(VectQuot_(V,(LKer_f)))_holds_(LQForm_f)_._(A,w)_=_0._K
let A be Vector of (VectQuot (V,(LKer f))); ::_thesis: (LQForm f) . (A,w) = 0. K
consider v being Vector of V such that
A3: A = v + (LKer f) by VECTSP10:22;
thus (LQForm f) . (A,w) = f . (v,w) by A3, Def20
.= 0. K by A2 ; ::_thesis: verum
end;
hence  x in rightker (LQForm f) by A1; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rightker (LQForm f) or x in rightker f )
assume  x in rightker (LQForm f) ; ::_thesis: x in rightker f
then consider w being Vector of W such that
A4: x = w and
A5: for A being Vector of (VectQuot (V,(LKer f))) holds (LQForm f) . (A,w) = 0. K ;
now__::_thesis:_for_v_being_Vector_of_V_holds_f_._(v,w)_=_0._K
let v be Vector of V; ::_thesis: f . (v,w) = 0. K
reconsider A = v + (LKer f) as Vector of (VectQuot (V,(LKer f))) by VECTSP10:23;
thus f . (v,w) = (LQForm f) . (A,w) by Def20
.= 0. K by A5 ; ::_thesis: verum
end;
hence  x in rightker f by A4; ::_thesis: verum
end;

theorem Th45: :: BILINEAR:45
for K being non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr
for V being non empty VectSpStr over K
for W being VectSp of K
for f being additiveFAF homogeneousFAF Form of V,W holds leftker f = leftker (RQForm f)
proof
let K be non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr ; ::_thesis: for V being non empty VectSpStr over K
for W being VectSp of K
for f being additiveFAF homogeneousFAF Form of V,W holds leftker f = leftker (RQForm f)
let V be non empty VectSpStr over K; ::_thesis: for W being VectSp of K
for f being additiveFAF homogeneousFAF Form of V,W holds leftker f = leftker (RQForm f)
let W be VectSp of K; ::_thesis: for f being additiveFAF homogeneousFAF Form of V,W holds leftker f = leftker (RQForm f)
let f be additiveFAF homogeneousFAF Form of V,W; ::_thesis: leftker f = leftker (RQForm f)
set rf = RQForm f;
set qw = VectQuot (W,(RKer f));
thus  leftker f c= leftker (RQForm f) :: according to XBOOLE_0:def_10 ::_thesis: leftker (RQForm f) c= leftker f
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in leftker f or x in leftker (RQForm f) )
assume  x in leftker f ; ::_thesis: x in leftker (RQForm f)
then consider v being Vector of V such that
A1: x = v and
A2: for w being Vector of W holds f . (v,w) = 0. K ;
now__::_thesis:_for_A_being_Vector_of_(VectQuot_(W,(RKer_f)))_holds_(RQForm_f)_._(v,A)_=_0._K
let A be Vector of (VectQuot (W,(RKer f))); ::_thesis: (RQForm f) . (v,A) = 0. K
consider w being Vector of W such that
A3: A = w + (RKer f) by VECTSP10:22;
thus (RQForm f) . (v,A) = f . (v,w) by A3, Def21
.= 0. K by A2 ; ::_thesis: verum
end;
hence  x in leftker (RQForm f) by A1; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in leftker (RQForm f) or x in leftker f )
assume  x in leftker (RQForm f) ; ::_thesis: x in leftker f
then consider v being Vector of V such that
A4: x = v and
A5: for A being Vector of (VectQuot (W,(RKer f))) holds (RQForm f) . (v,A) = 0. K ;
now__::_thesis:_for_w_being_Vector_of_W_holds_f_._(v,w)_=_0._K
let w be Vector of W; ::_thesis: f . (v,w) = 0. K
reconsider A = w + (RKer f) as Vector of (VectQuot (W,(RKer f))) by VECTSP10:23;
thus f . (v,w) = (RQForm f) . (v,A) by Def21
.= 0. K by A5 ; ::_thesis: verum
end;
hence  x in leftker f by A4; ::_thesis: verum
end;

theorem Th46: :: BILINEAR:46
for K being non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr
for V, W being VectSp of K
for f being bilinear-Form of V,W holds RKer f = RKer (LQForm f)
proof
let K be non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr ; ::_thesis: for V, W being VectSp of K
for f being bilinear-Form of V,W holds RKer f = RKer (LQForm f)
let V, W be VectSp of K; ::_thesis: for f being bilinear-Form of V,W holds RKer f = RKer (LQForm f)
let f be bilinear-Form of V,W; ::_thesis: RKer f = RKer (LQForm f)
the carrier of (RKer f) = rightker f by Def19
.= rightker (LQForm f) by Th44
.= the carrier of (RKer (LQForm f)) by Def19 ;
hence  RKer f = RKer (LQForm f) by VECTSP_4:29; ::_thesis: verum
end;

theorem Th47: :: BILINEAR:47
for K being non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr
for V, W being VectSp of K
for f being bilinear-Form of V,W holds LKer f = LKer (RQForm f)
proof
let K be non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr ; ::_thesis: for V, W being VectSp of K
for f being bilinear-Form of V,W holds LKer f = LKer (RQForm f)
let V, W be VectSp of K; ::_thesis: for f being bilinear-Form of V,W holds LKer f = LKer (RQForm f)
let f be bilinear-Form of V,W; ::_thesis: LKer f = LKer (RQForm f)
the carrier of (LKer f) = leftker f by Def18
.= leftker (RQForm f) by Th45
.= the carrier of (LKer (RQForm f)) by Def18 ;
hence  LKer f = LKer (RQForm f) by VECTSP_4:29; ::_thesis: verum
end;

theorem Th48: :: BILINEAR:48
for K being non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr
for V, W being VectSp of K
for f being bilinear-Form of V,W holds
( QForm f = RQForm (LQForm f) & QForm f = LQForm (RQForm f) )
proof
let K be non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr ; ::_thesis: for V, W being VectSp of K
for f being bilinear-Form of V,W holds
( QForm f = RQForm (LQForm f) & QForm f = LQForm (RQForm f) )
let V, W be VectSp of K; ::_thesis: for f being bilinear-Form of V,W holds
( QForm f = RQForm (LQForm f) & QForm f = LQForm (RQForm f) )
let f be bilinear-Form of V,W; ::_thesis: ( QForm f = RQForm (LQForm f) & QForm f = LQForm (RQForm f) )
set L = LKer f;
set vq = VectQuot (V,(LKer f));
set R = RKer f;
set wq = VectQuot (W,(RKer f));
set RL = RKer (LQForm f);
set wqr = VectQuot (W,(RKer (LQForm f)));
set LR = LKer (RQForm f);
set vql = VectQuot (V,(LKer (RQForm f)));
A1: dom (QForm f) = [: the carrier of (VectQuot (V,(LKer f))), the carrier of (VectQuot (W,(RKer f))):] by FUNCT_2:def_1;
A2: now__::_thesis:_for_x_being_set_st_x_in_dom_(QForm_f)_holds_
(QForm_f)_._x_=_(RQForm_(LQForm_f))_._x
let x be set ; ::_thesis: ( x in dom (QForm f) implies (QForm f) . x = (RQForm (LQForm f)) . x )
assume  x in dom (QForm f) ; ::_thesis: (QForm f) . x = (RQForm (LQForm f)) . x
then consider A being Vector of (VectQuot (V,(LKer f))), B being Vector of (VectQuot (W,(RKer f))) such that
A3: x = [A,B] by DOMAIN_1:1;
consider w being Vector of W such that
A4: B = w + (RKer f) by VECTSP10:22;
A5: RKer f = RKer (LQForm f) by Th46;
consider v being Vector of V such that
A6: A = v + (LKer f) by VECTSP10:22;
thus (QForm f) . x = (QForm f) . (A,B) by A3
.= f . (v,w) by A6, A4, Def22
.= (LQForm f) . (A,w) by A6, Def20
.= (RQForm (LQForm f)) . (A,B) by A4, A5, Def21
.= (RQForm (LQForm f)) . x by A3 ; ::_thesis: verum
end;
 ( dom (RQForm (LQForm f)) = [: the carrier of (VectQuot (V,(LKer f))), the carrier of (VectQuot (W,(RKer (LQForm f)))):] & the carrier of (VectQuot (W,(RKer (LQForm f)))) = the carrier of (VectQuot (W,(RKer f))) ) by Th46, FUNCT_2:def_1;
hence  QForm f = RQForm (LQForm f) by A1, A2, FUNCT_1:2; ::_thesis: QForm f = LQForm (RQForm f)
A7: now__::_thesis:_for_x_being_set_st_x_in_dom_(QForm_f)_holds_
(QForm_f)_._x_=_(LQForm_(RQForm_f))_._x
let x be set ; ::_thesis: ( x in dom (QForm f) implies (QForm f) . x = (LQForm (RQForm f)) . x )
assume  x in dom (QForm f) ; ::_thesis: (QForm f) . x = (LQForm (RQForm f)) . x
then consider A being Vector of (VectQuot (V,(LKer f))), B being Vector of (VectQuot (W,(RKer f))) such that
A8: x = [A,B] by DOMAIN_1:1;
consider w being Vector of W such that
A9: B = w + (RKer f) by VECTSP10:22;
A10: LKer f = LKer (RQForm f) by Th47;
consider v being Vector of V such that
A11: A = v + (LKer f) by VECTSP10:22;
thus (QForm f) . x = (QForm f) . (A,B) by A8
.= f . (v,w) by A11, A9, Def22
.= (RQForm f) . (v,B) by A9, Def21
.= (LQForm (RQForm f)) . (A,B) by A11, A10, Def20
.= (LQForm (RQForm f)) . x by A8 ; ::_thesis: verum
end;
 ( dom (LQForm (RQForm f)) = [: the carrier of (VectQuot (V,(LKer (RQForm f)))), the carrier of (VectQuot (W,(RKer f))):] & the carrier of (VectQuot (V,(LKer (RQForm f)))) = the carrier of (VectQuot (V,(LKer f))) ) by Th47, FUNCT_2:def_1;
hence  QForm f = LQForm (RQForm f) by A1, A7, FUNCT_1:2; ::_thesis: verum
end;

theorem Th49: :: BILINEAR:49
for K being non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr
for V, W being VectSp of K
for f being 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 non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr ; ::_thesis: for V, W being VectSp of K
for f being 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)) )
let V, W be VectSp of K; ::_thesis: for f being 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)) )
let f be bilinear-Form of V,W; ::_thesis: ( 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)) )
set vq = VectQuot (V,(LKer f));
set wq = VectQuot (W,(RKer f));
set wqr = VectQuot (W,(RKer (LQForm f)));
set vql = VectQuot (V,(LKer (RQForm f)));
set rlf = RQForm (LQForm f);
set qf = QForm f;
set lrf = LQForm (RQForm f);
thus  leftker (QForm f) c= leftker (RQForm (LQForm f)) :: according to XBOOLE_0:def_10 ::_thesis: ( leftker (RQForm (LQForm f)) c= leftker (QForm f) & rightker (QForm f) = rightker (RQForm (LQForm f)) & leftker (QForm f) = leftker (LQForm (RQForm f)) & rightker (QForm f) = rightker (LQForm (RQForm f)) )
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in leftker (QForm f) or x in leftker (RQForm (LQForm f)) )
assume  x in leftker (QForm f) ; ::_thesis: x in leftker (RQForm (LQForm f))
then consider vv being Vector of (VectQuot (V,(LKer f))) such that
A1: x = vv and
A2: for ww being Vector of (VectQuot (W,(RKer f))) holds (QForm f) . (vv,ww) = 0. K ;
now__::_thesis:_for_ww_being_Vector_of_(VectQuot_(W,(RKer_(LQForm_f))))_holds_(RQForm_(LQForm_f))_._(vv,ww)_=_0._K
let ww be Vector of (VectQuot (W,(RKer (LQForm f)))); ::_thesis: (RQForm (LQForm f)) . (vv,ww) = 0. K
reconsider w = ww as Vector of (VectQuot (W,(RKer f))) by Th46;
thus (RQForm (LQForm f)) . (vv,ww) = (QForm f) . (vv,w) by Th48
.= 0. K by A2 ; ::_thesis: verum
end;
hence  x in leftker (RQForm (LQForm f)) by A1; ::_thesis: verum
end;
thus  leftker (RQForm (LQForm f)) c= leftker (QForm f) ::_thesis: ( rightker (QForm f) = rightker (RQForm (LQForm f)) & leftker (QForm f) = leftker (LQForm (RQForm f)) & rightker (QForm f) = rightker (LQForm (RQForm f)) )
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in leftker (RQForm (LQForm f)) or x in leftker (QForm f) )
assume  x in leftker (RQForm (LQForm f)) ; ::_thesis: x in leftker (QForm f)
then consider vv being Vector of (VectQuot (V,(LKer f))) such that
A3: x = vv and
A4: for ww being Vector of (VectQuot (W,(RKer (LQForm f)))) holds (RQForm (LQForm f)) . (vv,ww) = 0. K ;
now__::_thesis:_for_ww_being_Vector_of_(VectQuot_(W,(RKer_f)))_holds_(QForm_f)_._(vv,ww)_=_0._K
let ww be Vector of (VectQuot (W,(RKer f))); ::_thesis: (QForm f) . (vv,ww) = 0. K
reconsider w = ww as Vector of (VectQuot (W,(RKer (LQForm f)))) by Th46;
thus (QForm f) . (vv,ww) = (RQForm (LQForm f)) . (vv,w) by Th48
.= 0. K by A4 ; ::_thesis: verum
end;
hence  x in leftker (QForm f) by A3; ::_thesis: verum
end;
thus  rightker (QForm f) c= rightker (RQForm (LQForm f)) :: according to XBOOLE_0:def_10 ::_thesis: ( rightker (RQForm (LQForm f)) c= rightker (QForm f) & leftker (QForm f) = leftker (LQForm (RQForm f)) & rightker (QForm f) = rightker (LQForm (RQForm f)) )
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rightker (QForm f) or x in rightker (RQForm (LQForm f)) )
assume  x in rightker (QForm f) ; ::_thesis: x in rightker (RQForm (LQForm f))
then consider ww being Vector of (VectQuot (W,(RKer f))) such that
A5: x = ww and
A6: for vv being Vector of (VectQuot (V,(LKer f))) holds (QForm f) . (vv,ww) = 0. K ;
reconsider w = ww as Vector of (VectQuot (W,(RKer (LQForm f)))) by Th46;
now__::_thesis:_for_vv_being_Vector_of_(VectQuot_(V,(LKer_f)))_holds_(RQForm_(LQForm_f))_._(vv,w)_=_0._K
let vv be Vector of (VectQuot (V,(LKer f))); ::_thesis: (RQForm (LQForm f)) . (vv,w) = 0. K
thus (RQForm (LQForm f)) . (vv,w) = (QForm f) . (vv,ww) by Th48
.= 0. K by A6 ; ::_thesis: verum
end;
hence  x in rightker (RQForm (LQForm f)) by A5; ::_thesis: verum
end;
thus  rightker (RQForm (LQForm f)) c= rightker (QForm f) ::_thesis: ( leftker (QForm f) = leftker (LQForm (RQForm f)) & rightker (QForm f) = rightker (LQForm (RQForm f)) )
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rightker (RQForm (LQForm f)) or x in rightker (QForm f) )
assume  x in rightker (RQForm (LQForm f)) ; ::_thesis: x in rightker (QForm f)
then consider ww being Vector of (VectQuot (W,(RKer (LQForm f)))) such that
A7: x = ww and
A8: for vv being Vector of (VectQuot (V,(LKer f))) holds (RQForm (LQForm f)) . (vv,ww) = 0. K ;
reconsider w = ww as Vector of (VectQuot (W,(RKer f))) by Th46;
now__::_thesis:_for_vv_being_Vector_of_(VectQuot_(V,(LKer_f)))_holds_(QForm_f)_._(vv,w)_=_0._K
let vv be Vector of (VectQuot (V,(LKer f))); ::_thesis: (QForm f) . (vv,w) = 0. K
thus (QForm f) . (vv,w) = (RQForm (LQForm f)) . (vv,ww) by Th48
.= 0. K by A8 ; ::_thesis: verum
end;
hence  x in rightker (QForm f) by A7; ::_thesis: verum
end;
thus  leftker (QForm f) c= leftker (LQForm (RQForm f)) :: according to XBOOLE_0:def_10 ::_thesis: ( leftker (LQForm (RQForm f)) c= leftker (QForm f) & rightker (QForm f) = rightker (LQForm (RQForm f)) )
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in leftker (QForm f) or x in leftker (LQForm (RQForm f)) )
assume  x in leftker (QForm f) ; ::_thesis: x in leftker (LQForm (RQForm f))
then consider vv being Vector of (VectQuot (V,(LKer f))) such that
A9: x = vv and
A10: for ww being Vector of (VectQuot (W,(RKer f))) holds (QForm f) . (vv,ww) = 0. K ;
reconsider v = vv as Vector of (VectQuot (V,(LKer (RQForm f)))) by Th47;
now__::_thesis:_for_ww_being_Vector_of_(VectQuot_(W,(RKer_f)))_holds_(LQForm_(RQForm_f))_._(v,ww)_=_0._K
let ww be Vector of (VectQuot (W,(RKer f))); ::_thesis: (LQForm (RQForm f)) . (v,ww) = 0. K
thus (LQForm (RQForm f)) . (v,ww) = (QForm f) . (vv,ww) by Th48
.= 0. K by A10 ; ::_thesis: verum
end;
hence  x in leftker (LQForm (RQForm f)) by A9; ::_thesis: verum
end;
thus  leftker (LQForm (RQForm f)) c= leftker (QForm f) ::_thesis: rightker (QForm f) = rightker (LQForm (RQForm f))
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in leftker (LQForm (RQForm f)) or x in leftker (QForm f) )
assume  x in leftker (LQForm (RQForm f)) ; ::_thesis: x in leftker (QForm f)
then consider vv being Vector of (VectQuot (V,(LKer (RQForm f)))) such that
A11: x = vv and
A12: for ww being Vector of (VectQuot (W,(RKer f))) holds (LQForm (RQForm f)) . (vv,ww) = 0. K ;
reconsider v = vv as Vector of (VectQuot (V,(LKer f))) by Th47;
now__::_thesis:_for_ww_being_Vector_of_(VectQuot_(W,(RKer_f)))_holds_(QForm_f)_._(v,ww)_=_0._K
let ww be Vector of (VectQuot (W,(RKer f))); ::_thesis: (QForm f) . (v,ww) = 0. K
thus (QForm f) . (v,ww) = (LQForm (RQForm f)) . (vv,ww) by Th48
.= 0. K by A12 ; ::_thesis: verum
end;
hence  x in leftker (QForm f) by A11; ::_thesis: verum
end;
thus  rightker (QForm f) c= rightker (LQForm (RQForm f)) :: according to XBOOLE_0:def_10 ::_thesis: rightker (LQForm (RQForm f)) c= rightker (QForm f)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rightker (QForm f) or x in rightker (LQForm (RQForm f)) )
assume  x in rightker (QForm f) ; ::_thesis: x in rightker (LQForm (RQForm f))
then consider ww being Vector of (VectQuot (W,(RKer f))) such that
A13: x = ww and
A14: for vv being Vector of (VectQuot (V,(LKer f))) holds (QForm f) . (vv,ww) = 0. K ;
now__::_thesis:_for_vv_being_Vector_of_(VectQuot_(V,(LKer_(RQForm_f))))_holds_(LQForm_(RQForm_f))_._(vv,ww)_=_0._K
let vv be Vector of (VectQuot (V,(LKer (RQForm f)))); ::_thesis: (LQForm (RQForm f)) . (vv,ww) = 0. K
reconsider v = vv as Vector of (VectQuot (V,(LKer f))) by Th47;
thus (LQForm (RQForm f)) . (vv,ww) = (QForm f) . (v,ww) by Th48
.= 0. K by A14 ; ::_thesis: verum
end;
hence  x in rightker (LQForm (RQForm f)) by A13; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rightker (LQForm (RQForm f)) or x in rightker (QForm f) )
assume  x in rightker (LQForm (RQForm f)) ; ::_thesis: x in rightker (QForm f)
then consider ww being Vector of (VectQuot (W,(RKer f))) such that
A15: x = ww and
A16: for vv being Vector of (VectQuot (V,(LKer (RQForm f)))) holds (LQForm (RQForm f)) . (vv,ww) = 0. K ;
now__::_thesis:_for_vv_being_Vector_of_(VectQuot_(V,(LKer_f)))_holds_(QForm_f)_._(vv,ww)_=_0._K
let vv be Vector of (VectQuot (V,(LKer f))); ::_thesis: (QForm f) . (vv,ww) = 0. K
reconsider v = vv as Vector of (VectQuot (V,(LKer (RQForm f)))) by Th47;
thus (QForm f) . (vv,ww) = (LQForm (RQForm f)) . (v,ww) by Th48
.= 0. K by A16 ; ::_thesis: verum
end;
hence  x in rightker (QForm f) by A15; ::_thesis: verum
end;

theorem Th50: :: BILINEAR:50
for K being non empty right_complementable add-associative right_zeroed distributive doubleLoopStr
for V, W being non empty VectSpStr over K
for f being Functional of V
for g being Functional of W holds ker f c= leftker (FormFunctional (f,g))
proof
let K be non empty right_complementable add-associative right_zeroed distributive doubleLoopStr ; ::_thesis: for V, W being non empty VectSpStr over K
for f being Functional of V
for g being Functional of W holds ker f c= leftker (FormFunctional (f,g))
let V, W be non empty VectSpStr over K; ::_thesis: for f being Functional of V
for g being Functional of W holds ker f c= leftker (FormFunctional (f,g))
let f be Functional of V; ::_thesis: for g being Functional of W holds ker f c= leftker (FormFunctional (f,g))
let g be Functional of W; ::_thesis: ker f c= leftker (FormFunctional (f,g))
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 ; :: according to TARSKI:def_3 ::_thesis: ( not x in ker f or x in leftker (FormFunctional (f,g)) )
assume  x in ker f ; ::_thesis: x in leftker (FormFunctional (f,g))
then consider v being Vector of V such that
A2: x = v and
A3: f . v = 0. K by A1;
now__::_thesis:_for_w_being_Vector_of_W_holds_(FormFunctional_(f,g))_._(v,w)_=_0._K
let w be Vector of W; ::_thesis: (FormFunctional (f,g)) . (v,w) = 0. K
thus (FormFunctional (f,g)) . (v,w) = (f . v) * (g . w) by Def10
.= 0. K by A3, VECTSP_1:7 ; ::_thesis: verum
end;
hence  x in leftker (FormFunctional (f,g)) by A2; ::_thesis: verum
end;

theorem Th51: :: BILINEAR:51
for K being non empty right_complementable almost_left_invertible add-associative right_zeroed associative commutative well-unital distributive doubleLoopStr
for V, W being non empty VectSpStr over K
for f being Functional of V
for g being Functional of W st g <> 0Functional W holds
leftker (FormFunctional (f,g)) = ker f
proof
let K be non empty right_complementable almost_left_invertible add-associative right_zeroed associative commutative well-unital distributive doubleLoopStr ; ::_thesis: for V, W being non empty VectSpStr over K
for f being Functional of V
for g being Functional of W st g <> 0Functional W holds
leftker (FormFunctional (f,g)) = ker f
let V, W be non empty VectSpStr over K; ::_thesis: for f being Functional of V
for g being Functional of W st g <> 0Functional W holds
leftker (FormFunctional (f,g)) = ker f
let f be Functional of V; ::_thesis: for g being Functional of W st g <> 0Functional W holds
leftker (FormFunctional (f,g)) = ker f
let g be Functional of W; ::_thesis: ( g <> 0Functional W implies leftker (FormFunctional (f,g)) = ker f )
set fg = FormFunctional (f,g);
assume A1: g <> 0Functional W ; ::_thesis: leftker (FormFunctional (f,g)) = ker f
A2: ker f =  {  v where v is Vector of V : f . v = 0. K  }  by VECTSP10:def_9;
thus  leftker (FormFunctional (f,g)) c= ker f :: according to XBOOLE_0:def_10 ::_thesis: ker f c= leftker (FormFunctional (f,g))
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in leftker (FormFunctional (f,g)) or x in ker f )
assume  x in leftker (FormFunctional (f,g)) ; ::_thesis: x in ker f
then consider v being Vector of V such that
A3: x = v and
A4: for w being Vector of W holds (FormFunctional (f,g)) . (v,w) = 0. K ;
assume  not x in ker f ; ::_thesis: contradiction
then A5: f . v <> 0. K by A2, A3;
now__::_thesis:_for_w_being_Vector_of_W_holds_g_._w_=_(0Functional_W)_._w
let w be Vector of W; ::_thesis: g . w = (0Functional W) . w
(f . v) * (g . w) = (FormFunctional (f,g)) . (v,w) by Def10
.= 0. K by A4 ;
hence g . w = 0. K by A5, VECTSP_1:12
.= (0Functional W) . w by HAHNBAN1:14 ;
::_thesis: verum
end;
hence  contradiction by A1, FUNCT_2:63; ::_thesis: verum
end;
thus  ker f c= leftker (FormFunctional (f,g)) by Th50; ::_thesis: verum
end;

theorem Th52: :: BILINEAR:52
for K being non empty right_complementable add-associative right_zeroed distributive doubleLoopStr
for V, W being non empty VectSpStr over K
for f being Functional of V
for g being Functional of W holds ker g c= rightker (FormFunctional (f,g))
proof
let K be non empty right_complementable add-associative right_zeroed distributive doubleLoopStr ; ::_thesis: for V, W being non empty VectSpStr over K
for f being Functional of V
for g being Functional of W holds ker g c= rightker (FormFunctional (f,g))
let V, W be non empty VectSpStr over K; ::_thesis: for f being Functional of V
for g being Functional of W holds ker g c= rightker (FormFunctional (f,g))
let f be Functional of V; ::_thesis: for g being Functional of W holds ker g c= rightker (FormFunctional (f,g))
let g be Functional of W; ::_thesis: ker g c= rightker (FormFunctional (f,g))
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 ; :: according to TARSKI:def_3 ::_thesis: ( not x in ker g or x in rightker (FormFunctional (f,g)) )
assume  x in ker g ; ::_thesis: x in rightker (FormFunctional (f,g))
then consider w being Vector of W such that
A2: x = w and
A3: g . w = 0. K by A1;
now__::_thesis:_for_v_being_Vector_of_V_holds_(FormFunctional_(f,g))_._(v,w)_=_0._K
let v be Vector of V; ::_thesis: (FormFunctional (f,g)) . (v,w) = 0. K
thus (FormFunctional (f,g)) . (v,w) = (f . v) * (g . w) by Def10
.= 0. K by A3, VECTSP_1:6 ; ::_thesis: verum
end;
hence  x in rightker (FormFunctional (f,g)) by A2; ::_thesis: verum
end;

theorem Th53: :: BILINEAR:53
for K being non empty right_complementable almost_left_invertible add-associative right_zeroed associative commutative well-unital distributive doubleLoopStr
for V, W being non empty VectSpStr over K
for f being Functional of V
for g being Functional of W st f <> 0Functional V holds
rightker (FormFunctional (f,g)) = ker g
proof
let K be non empty right_complementable almost_left_invertible add-associative right_zeroed associative commutative well-unital distributive doubleLoopStr ; ::_thesis: for V, W being non empty VectSpStr over K
for f being Functional of V
for g being Functional of W st f <> 0Functional V holds
rightker (FormFunctional (f,g)) = ker g
let V, W be non empty VectSpStr over K; ::_thesis: for f being Functional of V
for g being Functional of W st f <> 0Functional V holds
rightker (FormFunctional (f,g)) = ker g
let f be Functional of V; ::_thesis: for g being Functional of W st f <> 0Functional V holds
rightker (FormFunctional (f,g)) = ker g
let g be Functional of W; ::_thesis: ( f <> 0Functional V implies rightker (FormFunctional (f,g)) = ker g )
set fg = FormFunctional (f,g);
assume A1: f <> 0Functional V ; ::_thesis: rightker (FormFunctional (f,g)) = ker g
A2: ker g =  {  w where w is Vector of W : g . w = 0. K  }  by VECTSP10:def_9;
thus  rightker (FormFunctional (f,g)) c= ker g :: according to XBOOLE_0:def_10 ::_thesis: ker g c= rightker (FormFunctional (f,g))
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rightker (FormFunctional (f,g)) or x in ker g )
assume  x in rightker (FormFunctional (f,g)) ; ::_thesis: x in ker g
then consider w being Vector of W such that
A3: x = w and
A4: for v being Vector of V holds (FormFunctional (f,g)) . (v,w) = 0. K ;
assume  not x in ker g ; ::_thesis: contradiction
then A5: g . w <> 0. K by A2, A3;
now__::_thesis:_for_v_being_Vector_of_V_holds_f_._v_=_(0Functional_V)_._v
let v be Vector of V; ::_thesis: f . v = (0Functional V) . v
(f . v) * (g . w) = (FormFunctional (f,g)) . (v,w) by Def10
.= 0. K by A4 ;
hence f . v = 0. K by A5, VECTSP_1:12
.= (0Functional V) . v by HAHNBAN1:14 ;
::_thesis: verum
end;
hence  contradiction by A1, FUNCT_2:63; ::_thesis: verum
end;
thus  ker g c= rightker (FormFunctional (f,g)) by Th52; ::_thesis: verum
end;

theorem Th54: :: BILINEAR:54
for K being non empty right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive doubleLoopStr
for V being VectSp of K
for W being non empty VectSpStr over K
for f being linear-Functional of V
for g being 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 non empty right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive doubleLoopStr ; ::_thesis: for V being VectSp of K
for W being non empty VectSpStr over K
for f being linear-Functional of V
for g being Functional of W st g <> 0Functional W holds
( LKer (FormFunctional (f,g)) = Ker f & LQForm (FormFunctional (f,g)) = FormFunctional ((CQFunctional f),g) )
let V be VectSp of K; ::_thesis: for W being non empty VectSpStr over K
for f being linear-Functional of V
for g being Functional of W st g <> 0Functional W holds
( LKer (FormFunctional (f,g)) = Ker f & LQForm (FormFunctional (f,g)) = FormFunctional ((CQFunctional f),g) )
let W be non empty VectSpStr over K; ::_thesis: for f being linear-Functional of V
for g being Functional of W st g <> 0Functional W holds
( LKer (FormFunctional (f,g)) = Ker f & LQForm (FormFunctional (f,g)) = FormFunctional ((CQFunctional f),g) )
let f be linear-Functional of V; ::_thesis: for g being Functional of W st g <> 0Functional W holds
( LKer (FormFunctional (f,g)) = Ker f & LQForm (FormFunctional (f,g)) = FormFunctional ((CQFunctional f),g) )
let g be Functional of W; ::_thesis: ( g <> 0Functional W implies ( LKer (FormFunctional (f,g)) = Ker f & LQForm (FormFunctional (f,g)) = FormFunctional ((CQFunctional f),g) ) )
set fg = FormFunctional (f,g);
set cf = CQFunctional f;
set fcfg = FormFunctional ((CQFunctional f),g);
set vql = VectQuot (V,(LKer (FormFunctional (f,g))));
set vq = VectQuot (V,(Ker f));
assume  g <> 0Functional W ; ::_thesis: ( LKer (FormFunctional (f,g)) = Ker f & LQForm (FormFunctional (f,g)) = FormFunctional ((CQFunctional f),g) )
then A1: leftker (FormFunctional (f,g)) = ker f by Th51;
 the carrier of (LKer (FormFunctional (f,g))) = leftker (FormFunctional (f,g)) by Def18;
hence A2: LKer (FormFunctional (f,g)) = Ker f by A1, VECTSP10:def_11; ::_thesis: LQForm (FormFunctional (f,g)) = FormFunctional ((CQFunctional f),g)
A3: now__::_thesis:_for_x_being_set_st_x_in_dom_(FormFunctional_((CQFunctional_f),g))_holds_
(FormFunctional_((CQFunctional_f),g))_._x_=_(LQForm_(FormFunctional_(f,g)))_._x
let x be set ; ::_thesis: ( x in dom (FormFunctional ((CQFunctional f),g)) implies (FormFunctional ((CQFunctional f),g)) . x = (LQForm (FormFunctional (f,g))) . x )
assume  x in dom (FormFunctional ((CQFunctional f),g)) ; ::_thesis: (FormFunctional ((CQFunctional f),g)) . x = (LQForm (FormFunctional (f,g))) . x
then consider A being Vector of (VectQuot (V,(Ker f))), B being Vector of W such that
A4: x = [A,B] by DOMAIN_1:1;
consider v being Vector of V such that
A5: A = v + (Ker f) by VECTSP10:22;
thus (FormFunctional ((CQFunctional f),g)) . x = (FormFunctional ((CQFunctional f),g)) . (A,B) by A4
.= ((CQFunctional f) . A) * (g . B) by Def10
.= (f . v) * (g . B) by A5, VECTSP10:35
.= (FormFunctional (f,g)) . (v,B) by Def10
.= (LQForm (FormFunctional (f,g))) . (A,B) by A2, A5, Def20
.= (LQForm (FormFunctional (f,g))) . x by A4 ; ::_thesis: verum
end;
 ( dom (LQForm (FormFunctional (f,g))) = [: the carrier of (VectQuot (V,(LKer (FormFunctional (f,g))))), the carrier of W:] & dom (FormFunctional ((CQFunctional f),g)) = [: the carrier of (VectQuot (V,(Ker f))), the carrier of W:] ) by FUNCT_2:def_1;
hence  LQForm (FormFunctional (f,g)) = FormFunctional ((CQFunctional f),g) by A2, A3, FUNCT_1:2; ::_thesis: verum
end;

theorem Th55: :: BILINEAR:55
for K being non empty right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive doubleLoopStr
for V being non empty VectSpStr over K
for W being VectSp of K
for f being Functional of V
for g being 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 non empty right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive doubleLoopStr ; ::_thesis: for V being non empty VectSpStr over K
for W being VectSp of K
for f being Functional of V
for g being linear-Functional of W st f <> 0Functional V holds
( RKer (FormFunctional (f,g)) = Ker g & RQForm (FormFunctional (f,g)) = FormFunctional (f,(CQFunctional g)) )
let V be non empty VectSpStr over K; ::_thesis: for W being VectSp of K
for f being Functional of V
for g being linear-Functional of W st f <> 0Functional V holds
( RKer (FormFunctional (f,g)) = Ker g & RQForm (FormFunctional (f,g)) = FormFunctional (f,(CQFunctional g)) )
let W be VectSp of K; ::_thesis: for f being Functional of V
for g being linear-Functional of W st f <> 0Functional V holds
( RKer (FormFunctional (f,g)) = Ker g & RQForm (FormFunctional (f,g)) = FormFunctional (f,(CQFunctional g)) )
let f be Functional of V; ::_thesis: for g being linear-Functional of W st f <> 0Functional V holds
( RKer (FormFunctional (f,g)) = Ker g & RQForm (FormFunctional (f,g)) = FormFunctional (f,(CQFunctional g)) )
let g be linear-Functional of W; ::_thesis: ( f <> 0Functional V implies ( RKer (FormFunctional (f,g)) = Ker g & RQForm (FormFunctional (f,g)) = FormFunctional (f,(CQFunctional g)) ) )
set fg = FormFunctional (f,g);
set cg = CQFunctional g;
set fcfg = FormFunctional (f,(CQFunctional g));
set wqr = VectQuot (W,(RKer (FormFunctional (f,g))));
set wq = VectQuot (W,(Ker g));
assume  f <> 0Functional V ; ::_thesis: ( RKer (FormFunctional (f,g)) = Ker g & RQForm (FormFunctional (f,g)) = FormFunctional (f,(CQFunctional g)) )
then A1: rightker (FormFunctional (f,g)) = ker g by Th53;
 the carrier of (RKer (FormFunctional (f,g))) = rightker (FormFunctional (f,g)) by Def19;
hence A2: RKer (FormFunctional (f,g)) = Ker g by A1, VECTSP10:def_11; ::_thesis: RQForm (FormFunctional (f,g)) = FormFunctional (f,(CQFunctional g))
A3: now__::_thesis:_for_x_being_set_st_x_in_dom_(FormFunctional_(f,(CQFunctional_g)))_holds_
(FormFunctional_(f,(CQFunctional_g)))_._x_=_(RQForm_(FormFunctional_(f,g)))_._x
let x be set ; ::_thesis: ( x in dom (FormFunctional (f,(CQFunctional g))) implies (FormFunctional (f,(CQFunctional g))) . x = (RQForm (FormFunctional (f,g))) . x )
assume  x in dom (FormFunctional (f,(CQFunctional g))) ; ::_thesis: (FormFunctional (f,(CQFunctional g))) . x = (RQForm (FormFunctional (f,g))) . x
then consider A being Vector of V, B being Vector of (VectQuot (W,(Ker g))) such that
A4: x = [A,B] by DOMAIN_1:1;
consider w being Vector of W such that
A5: B = w + (Ker g) by VECTSP10:22;
thus (FormFunctional (f,(CQFunctional g))) . x = (FormFunctional (f,(CQFunctional g))) . (A,B) by A4
.= (f . A) * ((CQFunctional g) . B) by Def10
.= (f . A) * (g . w) by A5, VECTSP10:35
.= (FormFunctional (f,g)) . (A,w) by Def10
.= (RQForm (FormFunctional (f,g))) . (A,B) by A2, A5, Def21
.= (RQForm (FormFunctional (f,g))) . x by A4 ; ::_thesis: verum
end;
 ( dom (RQForm (FormFunctional (f,g))) = [: the carrier of V, the carrier of (VectQuot (W,(RKer (FormFunctional (f,g))))):] & dom (FormFunctional (f,(CQFunctional g))) = [: the carrier of V, the carrier of (VectQuot (W,(Ker g))):] ) by FUNCT_2:def_1;
hence  RQForm (FormFunctional (f,g)) = FormFunctional (f,(CQFunctional g)) by A2, A3, FUNCT_1:2; ::_thesis: verum
end;

theorem :: BILINEAR:56
for K being Field
for V, W being non trivial VectSp of K
for f being V17() linear-Functional of V
for g being V17() linear-Functional of W holds QForm (FormFunctional (f,g)) = FormFunctional ((CQFunctional f),(CQFunctional g))
proof
let K be Field; ::_thesis: for V, W being non trivial VectSp of K
for f being V17() linear-Functional of V
for g being V17() linear-Functional of W holds QForm (FormFunctional (f,g)) = FormFunctional ((CQFunctional f),(CQFunctional g))
let V, W be non trivial VectSp of K; ::_thesis: for f being V17() linear-Functional of V
for g being V17() linear-Functional of W holds QForm (FormFunctional (f,g)) = FormFunctional ((CQFunctional f),(CQFunctional g))
let f be V17() linear-Functional of V; ::_thesis: for g being V17() linear-Functional of W holds QForm (FormFunctional (f,g)) = FormFunctional ((CQFunctional f),(CQFunctional g))
let g be V17() linear-Functional of W; ::_thesis: QForm (FormFunctional (f,g)) = FormFunctional ((CQFunctional f),(CQFunctional g))
A1: CQFunctional f <> 0Functional (VectQuot (V,(Ker f))) ;
A2: g <> 0Functional W ;
then A3: LQForm (FormFunctional (f,g)) = FormFunctional ((CQFunctional f),g) by Th54;
thus  QForm (FormFunctional (f,g)) = RQForm (LQForm (FormFunctional (f,g))) by Th48
.= RQForm (FormFunctional ((CQFunctional f),g)) by A2, A3, Th54
.= FormFunctional ((CQFunctional f),(CQFunctional g)) by A1, Th55 ; ::_thesis: verum
end;

definition
let K be ZeroStr ;
let V, W be non empty VectSpStr over K;
let f be Form of V,W;
attrf is degenerated-on-left  means :Def23: :: BILINEAR:def 23
 leftker f <> {(0. V)};
attrf is degenerated-on-right  means :Def24: :: BILINEAR:def 24
 rightker f <> {(0. W)};
end;

:: deftheorem Def23 defines degenerated-on-left BILINEAR:def_23_:_
 for K being ZeroStr
for V, W being non empty VectSpStr over K
for f being Form of V,W holds
( f is degenerated-on-left iff leftker f <> {(0. V)} );

:: deftheorem Def24 defines degenerated-on-right BILINEAR:def_24_:_
 for K being ZeroStr
for V, W being non empty VectSpStr over K
for f being Form of V,W holds
( f is degenerated-on-right iff rightker f <> {(0. W)} );

registration
let K be non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr ;
let V be VectSp of K;
let W be non empty right_zeroed VectSpStr over K;
let f be additiveSAF homogeneousSAF Form of V,W;
cluster LQForm f ->  additiveSAF homogeneousSAF non degenerated-on-left ;
coherence
 not LQForm f is degenerated-on-left
proof
set qf = LQForm f;
set L = LKer f;
set qV = VectQuot (V,(LKer f));
thus  leftker (LQForm f) c= {(0. (VectQuot (V,(LKer f))))} :: according to XBOOLE_0:def_10,BILINEAR:def_23 ::_thesis: {(0. (VectQuot (V,(LKer f))))} c= leftker (LQForm f)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in leftker (LQForm f) or x in {(0. (VectQuot (V,(LKer f))))} )
assume  x in leftker (LQForm f) ; ::_thesis: x in {(0. (VectQuot (V,(LKer f))))}
then consider vv being Vector of (VectQuot (V,(LKer f))) such that
A1: x = vv and
A2: for w being Vector of W holds (LQForm f) . (vv,w) = 0. K ;
consider v being Vector of V such that
A3: vv = v + (LKer f) by VECTSP10:22;
now__::_thesis:_for_w_being_Vector_of_W_holds_f_._(v,w)_=_0._K
let w be Vector of W; ::_thesis: f . (v,w) = 0. K
thus f . (v,w) = (LQForm f) . (vv,w) by A3, Def20
.= 0. K by A2 ; ::_thesis: verum
end;
then  v in leftker f ;
then  v in the carrier of (LKer f) by Def18;
then  v in LKer f by STRUCT_0:def_5;
then v + (LKer f) = the carrier of (LKer f) by VECTSP_4:49
.= zeroCoset (V,(LKer f)) by VECTSP10:def_4
.= 0. (VectQuot (V,(LKer f))) by VECTSP10:21 ;
hence  x in {(0. (VectQuot (V,(LKer f))))} by A1, A3, TARSKI:def_1; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {(0. (VectQuot (V,(LKer f))))} or x in leftker (LQForm f) )
assume  x in {(0. (VectQuot (V,(LKer f))))} ; ::_thesis: x in leftker (LQForm f)
then A4: x = 0. (VectQuot (V,(LKer f))) by TARSKI:def_1;
 for w being Vector of W holds (LQForm f) . ((0. (VectQuot (V,(LKer f)))),w) = 0. K by Th30;
hence  x in leftker (LQForm f) by A4; ::_thesis: verum
end;
end;

registration
let K be non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr ;
let V be non empty right_zeroed VectSpStr over K;
let W be VectSp of K;
let f be additiveFAF homogeneousFAF Form of V,W;
cluster RQForm f ->  additiveFAF homogeneousFAF non degenerated-on-right ;
coherence
 not RQForm f is degenerated-on-right
proof
set qf = RQForm f;
set R = RKer f;
set qW = VectQuot (W,(RKer f));
thus  rightker (RQForm f) c= {(0. (VectQuot (W,(RKer f))))} :: according to XBOOLE_0:def_10,BILINEAR:def_24 ::_thesis: {(0. (VectQuot (W,(RKer f))))} c= rightker (RQForm f)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rightker (RQForm f) or x in {(0. (VectQuot (W,(RKer f))))} )
assume  x in rightker (RQForm f) ; ::_thesis: x in {(0. (VectQuot (W,(RKer f))))}
then consider ww being Vector of (VectQuot (W,(RKer f))) such that
A1: x = ww and
A2: for v being Vector of V holds (RQForm f) . (v,ww) = 0. K ;
consider w being Vector of W such that
A3: ww = w + (RKer f) by VECTSP10:22;
now__::_thesis:_for_v_being_Vector_of_V_holds_f_._(v,w)_=_0._K
let v be Vector of V; ::_thesis: f . (v,w) = 0. K
thus f . (v,w) = (RQForm f) . (v,ww) by A3, Def21
.= 0. K by A2 ; ::_thesis: verum
end;
then  w in rightker f ;
then  w in the carrier of (RKer f) by Def19;
then  w in RKer f by STRUCT_0:def_5;
then w + (RKer f) = the carrier of (RKer f) by VECTSP_4:49
.= zeroCoset (W,(RKer f)) by VECTSP10:def_4
.= 0. (VectQuot (W,(RKer f))) by VECTSP10:21 ;
hence  x in {(0. (VectQuot (W,(RKer f))))} by A1, A3, TARSKI:def_1; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {(0. (VectQuot (W,(RKer f))))} or x in rightker (RQForm f) )
assume  x in {(0. (VectQuot (W,(RKer f))))} ; ::_thesis: x in rightker (RQForm f)
then A4: x = 0. (VectQuot (W,(RKer f))) by TARSKI:def_1;
 for v being Vector of V holds (RQForm f) . (v,(0. (VectQuot (W,(RKer f))))) = 0. K by Th29;
hence  x in rightker (RQForm f) by A4; ::_thesis: verum
end;
end;

registration
let K be non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive 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
 ( not QForm f is degenerated-on-left & not QForm f is degenerated-on-right )
proof
 rightker (RQForm f) = {(0. (VectQuot (W,(RKer f))))} by Def24;
then A1: rightker (LQForm (RQForm f)) = {(0. (VectQuot (W,(RKer f))))} by Th44;
 leftker (LQForm f) = {(0. (VectQuot (V,(LKer f))))} by Def23;
then A2: leftker (RQForm (LQForm f)) = {(0. (VectQuot (V,(LKer f))))} by Th45;
 ( leftker (RQForm (LQForm f)) = leftker (QForm f) & rightker (LQForm (RQForm f)) = rightker (QForm f) ) by Th49;
hence  ( not QForm f is degenerated-on-left & not QForm f is degenerated-on-right ) by A2, A1, Def23, Def24; ::_thesis: verum
end;
end;

registration
let K be non empty right_complementable Abelian add-associative right_zeroed associative well-unital distributive doubleLoopStr ;
let V, W be VectSp of K;
let f be bilinear-Form of V,W;
cluster RQForm (LQForm f) ->  additiveFAF homogeneousFAF non degenerated-on-left non degenerated-on-right ;
coherence
 ( not RQForm (LQForm f) is degenerated-on-left & not RQForm (LQForm f) is degenerated-on-right )
proof
 leftker (LQForm f) = {(0. (VectQuot (V,(LKer f))))} by Def23;
then  leftker (RQForm (LQForm f)) = {(0. (VectQuot (V,(LKer f))))} by Th45;
hence  ( not RQForm (LQForm f) is degenerated-on-left & not RQForm (LQForm f) is degenerated-on-right ) by Def23; ::_thesis: verum
end;
cluster LQForm (RQForm f) ->  additiveSAF homogeneousSAF non degenerated-on-left non degenerated-on-right ;
coherence
 ( not LQForm (RQForm f) is degenerated-on-left & not LQForm (RQForm f) is degenerated-on-right )
proof
 rightker (RQForm f) = {(0. (VectQuot (W,(RKer f))))} by Def24;
then  rightker (LQForm (RQForm f)) = {(0. (VectQuot (W,(RKer f))))} by Th44;
hence  ( not LQForm (RQForm f) is degenerated-on-left & not LQForm (RQForm f) is degenerated-on-right ) by Def24; ::_thesis: verum
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
 not QForm f is constant
proof
consider v being Vector of V, w being Vector of W such that
A1: f . (v,w) <> 0. K by Th40;
reconsider B = w + (RKer f) as Vector of (VectQuot (W,(RKer f))) by VECTSP10:23;
reconsider A = v + (LKer f) as Vector of (VectQuot (V,(LKer f))) by VECTSP10:23;
 (QForm f) . (A,B) = f . (v,w) by Def22;
hence  not QForm f is constant by A1, Th40; ::_thesis: verum
end;
end;

begin

definition
let K be 1-sorted ;
let V be VectSpStr over K;
let f be Form of V,V;
attrf is symmetric  means :Def25: :: BILINEAR:def 25
 for v, w being Vector of V holds f . (v,w) = f . (w,v);
end;

:: deftheorem Def25 defines symmetric BILINEAR:def_25_:_
 for K being 1-sorted
for V being VectSpStr over K
for f being Form of V,V holds
( f is symmetric iff for v, w being Vector of V holds f . (v,w) = f . (w,v) );

definition
let K be ZeroStr ;
let V be VectSpStr over K;
let f be Form of V,V;
attrf is alternating  means :Def26: :: BILINEAR:def 26
 for v being Vector of V holds f . (v,v) = 0. K;
end;

:: deftheorem Def26 defines alternating BILINEAR:def_26_:_
 for K being ZeroStr
for V being VectSpStr over K
for f being Form of V,V holds
( f is alternating iff for v being Vector of V holds f . (v,v) = 0. K );

registration
let K be non empty ZeroStr ;
let V be non empty VectSpStr over K;
cluster NulForm (V,V) ->  symmetric ;
coherence
 NulForm (V,V) is symmetric
proof
let v, w be Vector of V; :: according to BILINEAR:def_25 ::_thesis: (NulForm (V,V)) . (v,w) = (NulForm (V,V)) . (w,v)
thus (NulForm (V,V)) . (v,w) = 0. K by FUNCOP_1:70
.= (NulForm (V,V)) . (w,v) by FUNCOP_1:70 ; ::_thesis: verum
end;
cluster NulForm (V,V) ->  alternating ;
coherence
 NulForm (V,V) is alternating
proof
let v be Vector of V; :: according to BILINEAR:def_26 ::_thesis: (NulForm (V,V)) . (v,v) = 0. K
thus  (NulForm (V,V)) . (v,v) = 0. K by FUNCOP_1:70; ::_thesis: verum
end;
end;

registration
let K be non empty ZeroStr ;
let V be non empty VectSpStr over K;
cluster non empty Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of K -valued Function-like V20([: the carrier of V, the carrier of V:]) V21([: the carrier of V, the carrier of V:], the carrier of K) symmetric for Element of bool [:[: the carrier of V, the carrier of V:], the carrier of K:];
existence
 ex b1 being Form of V,V st b1 is symmetric
proof
take  NulForm (V,V) ; ::_thesis: NulForm (V,V) is symmetric
thus  NulForm (V,V) is symmetric ; ::_thesis: verum
end;
cluster non empty Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of K -valued Function-like V20([: the carrier of V, the carrier of V:]) V21([: the carrier of V, the carrier of V:], the carrier of K) alternating for Element of bool [:[: the carrier of V, the carrier of V:], the carrier of K:];
existence
 ex b1 being Form of V,V st b1 is alternating
proof
take  NulForm (V,V) ; ::_thesis: NulForm (V,V) is alternating
thus  NulForm (V,V) is alternating ; ::_thesis: verum
end;
end;

registration
let K be non empty right_complementable add-associative right_zeroed right-distributive doubleLoopStr ;
let V be non empty VectSpStr over K;
cluster non empty Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of K -valued Function-like V20([: the carrier of V, the carrier of V:]) V21([: the carrier of V, the carrier of V:], the carrier of K) additiveFAF additiveSAF homogeneousFAF homogeneousSAF symmetric for Element of bool [:[: the carrier of V, the carrier of V:], the carrier of K:];
existence
 ex b1 being Form of V,V st
( b1 is symmetric & b1 is additiveFAF & b1 is homogeneousFAF & b1 is additiveSAF & b1 is homogeneousSAF )
proof
take  NulForm (V,V) ; ::_thesis: ( NulForm (V,V) is symmetric & NulForm (V,V) is additiveFAF & NulForm (V,V) is homogeneousFAF & NulForm (V,V) is additiveSAF & NulForm (V,V) is homogeneousSAF )
thus  ( NulForm (V,V) is symmetric & NulForm (V,V) is additiveFAF & NulForm (V,V) is homogeneousFAF & NulForm (V,V) is additiveSAF & NulForm (V,V) is homogeneousSAF ) ; ::_thesis: verum
end;
cluster non empty Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of K -valued Function-like V20([: the carrier of V, the carrier of V:]) V21([: the carrier of V, the carrier of V:], the carrier of K) additiveFAF additiveSAF homogeneousFAF homogeneousSAF alternating for Element of bool [:[: the carrier of V, the carrier of V:], the carrier of K:];
existence
 ex b1 being Form of V,V st
( b1 is alternating & b1 is additiveFAF & b1 is homogeneousFAF & b1 is additiveSAF & b1 is homogeneousSAF )
proof
take  NulForm (V,V) ; ::_thesis: ( NulForm (V,V) is alternating & NulForm (V,V) is additiveFAF & NulForm (V,V) is homogeneousFAF & NulForm (V,V) is additiveSAF & NulForm (V,V) is homogeneousSAF )
thus  ( NulForm (V,V) is alternating & NulForm (V,V) is additiveFAF & NulForm (V,V) is homogeneousFAF & NulForm (V,V) is additiveSAF & NulForm (V,V) is homogeneousSAF ) ; ::_thesis: verum
end;
end;

registration
let K be Field;
let V be non trivial VectSp of K;
cluster non empty non trivial Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of K -valued Function-like non constant V20([: the carrier of V, the carrier of V:]) V21([: the carrier of V, the carrier of V:], the carrier of K) additiveFAF additiveSAF homogeneousFAF homogeneousSAF symmetric for Element of bool [:[: the carrier of V, the carrier of V:], the carrier of K:];
existence
 ex b1 being Form of V,V st
( b1 is symmetric & not b1 is trivial & not b1 is constant & b1 is additiveFAF & b1 is homogeneousFAF & b1 is additiveSAF & b1 is homogeneousSAF )
proof
set f = the non trivial V17() linear-Functional of V;
take ff = FormFunctional ( the non trivial V17() linear-Functional of V, the non trivial V17() linear-Functional of V); ::_thesis: ( ff is symmetric & not ff is trivial & not ff is constant & ff is additiveFAF & ff is homogeneousFAF & ff is additiveSAF & ff is homogeneousSAF )
now__::_thesis:_for_v,_w_being_Vector_of_V_holds_ff_._(v,w)_=_ff_._(w,v)
let v, w be Vector of V; ::_thesis: ff . (v,w) = ff . (w,v)
thus ff . (v,w) = ( the non trivial V17() linear-Functional of V . v) * ( the non trivial V17() linear-Functional of V . w) by Def10
.= ff . (w,v) by Def10 ; ::_thesis: verum
end;
hence  ( ff is symmetric & not ff is trivial & not ff is constant & ff is additiveFAF & ff is homogeneousFAF & ff is additiveSAF & ff is homogeneousSAF ) by Def25; ::_thesis: verum
end;
end;

registration
let K be non empty right_complementable add-associative right_zeroed addLoopStr ;
let V be non empty VectSpStr over K;
cluster non empty Relation-like [: the carrier of V, the carrier of V:] -defined the carrier of K -valued Function-like V20([: the carrier of V, the carrier of V:]) V21([: the carrier of V, the carrier of V:], the carrier of K) additiveFAF additiveSAF alternating for Element of bool [:[: the carrier of V, the carrier of V:], the carrier of K:];
existence
 ex b1 being Form of V,V st
( b1 is alternating & b1 is additiveFAF & b1 is additiveSAF )
proof
take  NulForm (V,V) ; ::_thesis: ( NulForm (V,V) is alternating & NulForm (V,V) is additiveFAF & NulForm (V,V) is additiveSAF )
thus  ( NulForm (V,V) is alternating & NulForm (V,V) is additiveFAF & NulForm (V,V) is additiveSAF ) ; ::_thesis: verum
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;
clusterf + g ->  symmetric ;
coherence
 f + g is symmetric
proof
let v, w be Vector of V; :: according to BILINEAR:def_25 ::_thesis: (f + g) . (v,w) = (f + g) . (w,v)
thus (f + g) . (v,w) = (f . (v,w)) + (g . (v,w)) by Def2
.= (f . (w,v)) + (g . (v,w)) by Def25
.= (f . (w,v)) + (g . (w,v)) by Def25
.= (f + g) . (w,v) by Def2 ; ::_thesis: verum
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;
clustera * f ->  symmetric ;
coherence
 a * f is symmetric
proof
let v, w be Vector of V; :: according to BILINEAR:def_25 ::_thesis: (a * f) . (v,w) = (a * f) . (w,v)
thus (a * f) . (v,w) = a * (f . (v,w)) by Def3
.= a * (f . (w,v)) by Def25
.= (a * f) . (w,v) by Def3 ; ::_thesis: verum
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
 - f is symmetric
proof
let v, w be Vector of V; :: according to BILINEAR:def_25 ::_thesis: (- f) . (v,w) = (- f) . (w,v)
thus (- f) . (v,w) = - (f . (v,w)) by Def4
.= - (f . (w,v)) by Def25
.= (- f) . (w,v) by Def4 ; ::_thesis: verum
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;
clusterf - g ->  symmetric ;
coherence
 f - g is symmetric ;
end;

registration
let K be non empty right_zeroed addLoopStr ;
let V be non empty VectSpStr over K;
let f, g be alternating Form of V,V;
clusterf + g ->  alternating ;
coherence
 f + g is alternating
proof
let v be Vector of V; :: according to BILINEAR:def_26 ::_thesis: (f + g) . (v,v) = 0. K
thus (f + g) . (v,v) = (f . (v,v)) + (g . (v,v)) by Def2
.= (0. K) + (g . (v,v)) by Def26
.= (0. K) + (0. K) by Def26
.= 0. K by RLVECT_1:def_4 ; ::_thesis: verum
end;
end;

registration
let K be non empty right_complementable add-associative right_zeroed right-distributive doubleLoopStr ;
let V be non empty VectSpStr over K;
let f be alternating Form of V,V;
let a be Scalar of K;
clustera * f ->  alternating ;
coherence
 a * f is alternating
proof
let v be Vector of V; :: according to BILINEAR:def_26 ::_thesis: (a * f) . (v,v) = 0. K
thus (a * f) . (v,v) = a * (f . (v,v)) by Def3
.= a * (0. K) by Def26
.= 0. K by VECTSP_1:6 ; ::_thesis: verum
end;
end;

registration
let K be non empty right_complementable add-associative right_zeroed addLoopStr ;
let V be non empty VectSpStr over K;
let f be alternating Form of V,V;
cluster - f ->  alternating ;
coherence
 - f is alternating
proof
let v be Vector of V; :: according to BILINEAR:def_26 ::_thesis: (- f) . (v,v) = 0. K
thus (- f) . (v,v) = - (f . (v,v)) by Def4
.= - (0. K) by Def26
.= 0. K by RLVECT_1:12 ; ::_thesis: verum
end;
end;

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

theorem :: BILINEAR:57
for K being non empty right_complementable add-associative right_zeroed right-distributive doubleLoopStr
for V being non empty VectSpStr over K
for f being symmetric bilinear-Form of V,V holds leftker f = rightker f
proof
let K be non empty right_complementable add-associative right_zeroed right-distributive doubleLoopStr ; ::_thesis: for V being non empty VectSpStr over K
for f being symmetric bilinear-Form of V,V holds leftker f = rightker f
let V be non empty VectSpStr over K; ::_thesis: for f being symmetric bilinear-Form of V,V holds leftker f = rightker f
let f be symmetric bilinear-Form of V,V; ::_thesis: leftker f = rightker f
thus  leftker f c= rightker f :: according to XBOOLE_0:def_10 ::_thesis: rightker f c= leftker f
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in leftker f or x in rightker f )
assume  x in leftker f ; ::_thesis: x in rightker f
then consider v being Vector of V such that
A1: v = x and
A2: for w being Vector of V holds f . (v,w) = 0. K ;
now__::_thesis:_for_w_being_Vector_of_V_holds_f_._(w,v)_=_0._K
let w be Vector of V; ::_thesis: f . (w,v) = 0. K
thus f . (w,v) = f . (v,w) by Def25
.= 0. K by A2 ; ::_thesis: verum
end;
hence  x in rightker f by A1; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rightker f or x in leftker f )
assume  x in rightker f ; ::_thesis: x in leftker f
then consider w being Vector of V such that
A3: w = x and
A4: for v being Vector of V holds f . (v,w) = 0. K ;
now__::_thesis:_for_v_being_Vector_of_V_holds_f_._(w,v)_=_0._K
let v be Vector of V; ::_thesis: f . (w,v) = 0. K
thus f . (w,v) = f . (v,w) by Def25
.= 0. K by A4 ; ::_thesis: verum
end;
hence  x in leftker f by A3; ::_thesis: verum
end;

theorem Th58: :: BILINEAR:58
for K being non empty right_complementable add-associative right_zeroed addLoopStr
for V being non empty VectSpStr over K
for f being additiveFAF additiveSAF alternating Form of V,V
for v, w being Vector of V holds f . (v,w) = - (f . (w,v))
proof
let K be non empty right_complementable add-associative right_zeroed addLoopStr ; ::_thesis: for V being non empty VectSpStr over K
for f being additiveFAF additiveSAF alternating Form of V,V
for v, w being Vector of V holds f . (v,w) = - (f . (w,v))
let V be non empty VectSpStr over K; ::_thesis: for f being additiveFAF additiveSAF alternating Form of V,V
for v, w being Vector of V holds f . (v,w) = - (f . (w,v))
let f be additiveFAF additiveSAF alternating Form of V,V; ::_thesis: for v, w being Vector of V holds f . (v,w) = - (f . (w,v))
let v, w be Vector of V; ::_thesis: f . (v,w) = - (f . (w,v))
0. K = f . ((v + w),(v + w)) by Def26
.= ((f . (v,v)) + (f . (v,w))) + ((f . (w,v)) + (f . (w,w))) by Th28
.= ((0. K) + (f . (v,w))) + ((f . (w,v)) + (f . (w,w))) by Def26
.= ((0. K) + (f . (v,w))) + ((f . (w,v)) + (0. K)) by Def26
.= ((0. K) + (f . (v,w))) + (f . (w,v)) by RLVECT_1:def_4
.= (f . (v,w)) + (f . (w,v)) by RLVECT_1:4 ;
hence  f . (v,w) = - (f . (w,v)) by RLVECT_1:6; ::_thesis: verum
end;

definition
let K be Fanoian Field;
let V be non empty VectSpStr over K;
let f be additiveFAF additiveSAF Form of V,V;
redefine attr f is alternating  means :: BILINEAR:def 27
 for v, w being Vector of V holds f . (v,w) = - (f . (w,v));
compatibility
 ( f is alternating iff for v, w being Vector of V holds f . (v,w) = - (f . (w,v)) )
proof
thus  ( f is alternating implies for v, w being Vector of V holds f . (v,w) = - (f . (w,v)) ) by Th58; ::_thesis: ( ( for v, w being Vector of V holds f . (v,w) = - (f . (w,v)) ) implies f is alternating )
assume A1: for v, w being Vector of V holds f . (v,w) = - (f . (w,v)) ; ::_thesis: f is alternating
let v be Vector of V; :: according to BILINEAR:def_26 ::_thesis: f . (v,v) = 0. K
 f . (v,v) = - (f . (v,v)) by A1;
then  (f . (v,v)) + (f . (v,v)) = 0. K by VECTSP_1:16;
hence  f . (v,v) = 0. K by VECTSP_1:def_18; ::_thesis: verum
end;
end;

:: deftheorem  defines alternating BILINEAR:def_27_:_
 for K being Fanoian Field
for V being non empty VectSpStr over K
for f being additiveFAF additiveSAF Form of V,V holds
( f is alternating iff for v, w being Vector of V holds f . (v,w) = - (f . (w,v)) );

theorem :: BILINEAR:59
for K being non empty right_complementable add-associative right_zeroed right-distributive doubleLoopStr
for V being non empty VectSpStr over K
for f being alternating bilinear-Form of V,V holds leftker f = rightker f
proof
let K be non empty right_complementable add-associative right_zeroed right-distributive doubleLoopStr ; ::_thesis: for V being non empty VectSpStr over K
for f being alternating bilinear-Form of V,V holds leftker f = rightker f
let V be non empty VectSpStr over K; ::_thesis: for f being alternating bilinear-Form of V,V holds leftker f = rightker f
let f be alternating bilinear-Form of V,V; ::_thesis: leftker f = rightker f
thus  leftker f c= rightker f :: according to XBOOLE_0:def_10 ::_thesis: rightker f c= leftker f
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in leftker f or x in rightker f )
assume  x in leftker f ; ::_thesis: x in rightker f
then consider v being Vector of V such that
A1: v = x and
A2: for w being Vector of V holds f . (v,w) = 0. K ;
now__::_thesis:_for_w_being_Vector_of_V_holds_f_._(w,v)_=_0._K
let w be Vector of V; ::_thesis: f . (w,v) = 0. K
thus f . (w,v) = - (f . (v,w)) by Th58
.= - (0. K) by A2
.= 0. K by RLVECT_1:12 ; ::_thesis: verum
end;
hence  x in rightker f by A1; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rightker f or x in leftker f )
assume  x in rightker f ; ::_thesis: x in leftker f
then consider w being Vector of V such that
A3: w = x and
A4: for v being Vector of V holds f . (v,w) = 0. K ;
now__::_thesis:_for_v_being_Vector_of_V_holds_f_._(w,v)_=_0._K
let v be Vector of V; ::_thesis: f . (w,v) = 0. K
thus f . (w,v) = - (f . (v,w)) by Th58
.= - (0. K) by A4
.= 0. K by RLVECT_1:12 ; ::_thesis: verum
end;
hence  x in leftker f by A3; ::_thesis: verum
end;