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

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

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

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

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

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

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