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

$3 = f . (a,$2);

A6: for A being Vector of (VectQuot (V,(LKer f)))

for w being Vector of W holds S_{1}[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;

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

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 S

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

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

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

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

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

end;let w0 be Vector of W; :: thesis: ex y being Element of the carrier of K st S

consider a being Vector of V such that

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

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

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

y = f . (a1,w0)

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

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

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

A6: for A being Vector of (VectQuot (V,(LKer f)))

for w being Vector of W holds S

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

then reconsider ff = ff as additiveSAF Form of (VectQuot (V,(LKer f))),W by Def12;let w be Vector of W; :: thesis: FunctionalSAF (ff,w) is additive

set ffw = FunctionalSAF (ff,w);

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

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

now :: thesis: for w being Vector of W holds FunctionalSAF (ff,w) is homogeneous

then reconsider ff = ff as additiveSAF homogeneousSAF Form of (VectQuot (V,(LKer f))),W by Def14;let w be Vector of W; :: thesis: FunctionalSAF (ff,w) is homogeneous

set ffw = FunctionalSAF (ff,w);

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

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

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