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 let A be
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 w0 be
Vector of
W;
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:23;
take y =
f . a,
w0;
S1[A,w0,y]now let a1 be
Vector of
V;
( A = a1 + (LKer f) implies y = f . a1,w0 )assume
A = a1 + (LKer f)
;
y = f . a1,w0then
a in a1 + (LKer f)
by A2, VECTSP_4:59;
then consider w being
Vector of
V such that A3:
w in LKer f
and A4:
a = a1 + w
by VECTSP_4:57;
w in the
carrier of
(LKer f)
by A3, STRUCT_0:def 5;
then
w in leftker f
by Def19;
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, Th27
.=
(f . a1,w0) + (0. K)
by A5
.=
f . a1,
w0
by RLVECT_1:def 7
;
verum end; hence
S1[
A,
w0,
y]
;
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 let w be
Vector of
W;
FunctionalSAF ff,w is additive set ffw =
FunctionalSAF ff,
w;
now let A,
B be
Vector of
(VectQuot V,(LKer f));
(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:23;
consider b being
Vector of
V such that A9:
B = b + (LKer f)
by VECTSP10:23;
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 Th10
.=
f . (a + b),
w
by A6, A10, RLVECT_1:5
.=
(f . a,w) + (f . b,w)
by Th27
.=
(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 Th10
.=
((FunctionalSAF ff,w) . A) + ((FunctionalSAF ff,w) . B)
by Th10
;
verum end; hence
FunctionalSAF ff,
w is
additive
by GRCAT_1:def 13;
verum end;
then reconsider ff = ff as additiveSAF Form of (VectQuot V,(LKer f)),W by Def13;
now let w be
Vector of
W;
FunctionalSAF ff,w is homogeneous set ffw =
FunctionalSAF ff,
w;
now let A be
Vector of
(VectQuot V,(LKer f));
for r being Element of K holds (FunctionalSAF ff,w) . (r * A) = r * ((FunctionalSAF ff,w) . A)let r be
Element of
K;
(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:23;
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 Th10
.=
f . (r * a),
w
by A6, A12, VECTSP_1:def 24
.=
r * (f . a,w)
by Th32
.=
r * (ff . A,w)
by A6, A11
.=
r * ((FunctionalSAF ff,w) . A)
by Th10
;
verum end; hence
FunctionalSAF ff,
w is
homogeneous
by HAHNBAN1:def 12;
verum end;
then reconsider ff = ff as additiveSAF homogeneousSAF Form of (VectQuot V,(LKer f)),W by Def15;
take
ff
; 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; verum