let K be non empty right_complementable almost_left_invertible Abelian add-associative right_zeroed well-unital distributive associative commutative doubleLoopStr ; :: thesis: for V being VectSp of K

for W being non empty ModuleStr 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 ModuleStr 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 ModuleStr 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)

hence LQForm (FormFunctional (f,g)) = FormFunctional ((CQFunctional f),g) by A2, A3, FUNCT_1:2; :: thesis: verum

for W being non empty ModuleStr 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 ModuleStr 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 ModuleStr 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 object st x in dom (FormFunctional ((CQFunctional f),g)) holds

(FormFunctional ((CQFunctional f),g)) . x = (LQForm (FormFunctional (f,g))) . x

( 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;(FormFunctional ((CQFunctional f),g)) . x = (LQForm (FormFunctional (f,g))) . x

let x be object ; :: 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;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

hence LQForm (FormFunctional (f,g)) = FormFunctional ((CQFunctional f),g) by A2, A3, FUNCT_1:2; :: thesis: verum