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 S_{1}[ set , set , set ] means for w being Vector of W st $2 = w + (RKer f) holds

$3 = f . ($1,w);

A6: for v being Vector of V

for A being Vector of (VectQuot (W,(RKer f))) holds S_{1}[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;

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

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 S

$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 S_{1}[v0,A,y]

consider ff being Function of [: the carrier of V, the carrier of (VectQuot (W,(RKer f))):], the carrier of K such that for A being Vector of (VectQuot (W,(RKer f))) ex y being Element of the carrier of K st S

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 S_{1}[v0,A,y]

let A be Vector of (VectQuot (W,(RKer f))); :: thesis: ex y being Element of the carrier of K st S_{1}[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: S_{1}[v0,A,y]

_{1}[v0,A,y]
; :: thesis: verum

end;let A be Vector of (VectQuot (W,(RKer f))); :: thesis: ex y being Element of the carrier of K st S

consider a being Vector of W such that

A2: A = a + (RKer f) by VECTSP10:22;

take y = f . (v0,a); :: thesis: S

now :: thesis: for a1 being Vector of W st A = a1 + (RKer f) holds

y = f . (v0,a1)

hence
Sy = 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;

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

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

A6: for v being Vector of V

for A being Vector of (VectQuot (W,(RKer f))) holds S

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

then reconsider ff = ff as additiveFAF Form of V,(VectQuot (W,(RKer f))) by Def11;let v be Vector of V; :: thesis: FunctionalFAF (ff,v) is additive

set ffw = FunctionalFAF (ff,v);

end;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)

hence
FunctionalFAF (ff,v) is additive
; :: thesis: verumlet 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;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

now :: thesis: for v being Vector of V holds FunctionalFAF (ff,v) is homogeneous

then reconsider ff = ff as additiveFAF homogeneousFAF Form of V,(VectQuot (W,(RKer f))) by Def13;let v be Vector of V; :: thesis: FunctionalFAF (ff,v) is homogeneous

set ffw = FunctionalFAF (ff,v);

end;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)

hence
FunctionalFAF (ff,v) is homogeneous
; :: thesis: verumfor 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;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

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