set K = F_Complex ;

set L = LKer f;

set vq = VectQuot (V,(LKer f));

set Cv = CosetSet (V,(LKer f));

set aCv = addCoset (V,(LKer f));

set mCv = lmultCoset (V,(LKer f));

set R = RKer (f *');

set wq = VectQuot (W,(RKer (f *')));

set Cw = CosetSet (W,(RKer (f *')));

set aCw = addCoset (W,(RKer (f *')));

set mCw = lmultCoset (W,(RKer (f *')));

defpred S_{1}[ set , set , set ] means for v being Vector of V

for w being Vector of W st $1 = v + (LKer f) & $2 = w + (RKer (f *')) holds

$3 = f . (v,w);

A1: rightker f = rightker (f *') by Th55;

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

for B being Vector of (VectQuot (W,(RKer (f *')))) holds S_{1}[A,B,ff . (A,B)]
from BINOP_1:sch 3(A2);

reconsider ff = ff as Form of (VectQuot (V,(LKer f))),(VectQuot (W,(RKer (f *')))) ;

A12: 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 B being Vector of (VectQuot (W,(RKer (f *'))))

for v being Vector of V

for w being Vector of W st A = v + (LKer f) & B = w + (RKer (f *')) holds

ff . (A,B) = f . (v,w)

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

for B being Vector of (VectQuot (W,(RKer (f *'))))

for v being Vector of V

for w being Vector of W st A = v + (LKer f) & B = w + (RKer (f *')) holds

ff . (A,B) = f . (v,w) by A11; :: thesis: verum

set L = LKer f;

set vq = VectQuot (V,(LKer f));

set Cv = CosetSet (V,(LKer f));

set aCv = addCoset (V,(LKer f));

set mCv = lmultCoset (V,(LKer f));

set R = RKer (f *');

set wq = VectQuot (W,(RKer (f *')));

set Cw = CosetSet (W,(RKer (f *')));

set aCw = addCoset (W,(RKer (f *')));

set mCw = lmultCoset (W,(RKer (f *')));

defpred S

for w being Vector of W st $1 = v + (LKer f) & $2 = w + (RKer (f *')) holds

$3 = f . (v,w);

A1: rightker f = rightker (f *') by Th55;

A2: now :: thesis: for A being Vector of (VectQuot (V,(LKer f)))

for B being Vector of (VectQuot (W,(RKer (f *')))) ex y being Element of the carrier of F_Complex st S_{1}[A,B,y]

consider ff being Function of [: the carrier of (VectQuot (V,(LKer f))), the carrier of (VectQuot (W,(RKer (f *')))):], the carrier of F_Complex such that for B being Vector of (VectQuot (W,(RKer (f *')))) ex y being Element of the carrier of F_Complex st S

let A be Vector of (VectQuot (V,(LKer f))); :: thesis: for B being Vector of (VectQuot (W,(RKer (f *')))) ex y being Element of the carrier of F_Complex st S_{1}[A,B,y]

let B be Vector of (VectQuot (W,(RKer (f *')))); :: thesis: ex y being Element of the carrier of F_Complex st S_{1}[A,B,y]

consider a being Vector of V such that

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

consider b being Vector of W such that

A4: B = b + (RKer (f *')) by VECTSP10:22;

take y = f . (a,b); :: thesis: S_{1}[A,B,y]

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

end;let B be Vector of (VectQuot (W,(RKer (f *')))); :: thesis: ex y being Element of the carrier of F_Complex st S

consider a being Vector of V such that

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

consider b being Vector of W such that

A4: B = b + (RKer (f *')) by VECTSP10:22;

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

now :: thesis: for a1 being Vector of V

for b1 being Vector of W st A = a1 + (LKer f) & B = b1 + (RKer (f *')) holds

y = f . (a1,b1)

hence
Sfor b1 being Vector of W st A = a1 + (LKer f) & B = b1 + (RKer (f *')) holds

y = f . (a1,b1)

let a1 be Vector of V; :: thesis: for b1 being Vector of W st A = a1 + (LKer f) & B = b1 + (RKer (f *')) holds

y = f . (a1,b1)

let b1 be Vector of W; :: thesis: ( A = a1 + (LKer f) & B = b1 + (RKer (f *')) implies y = f . (a1,b1) )

assume A = a1 + (LKer f) ; :: thesis: ( B = b1 + (RKer (f *')) implies y = f . (a1,b1) )

then a in a1 + (LKer f) by A3, VECTSP_4:44;

then consider vv being Vector of V such that

A5: vv in LKer f and

A6: a = a1 + vv by VECTSP_4:42;

vv in the carrier of (LKer f) by A5, STRUCT_0:def 5;

then vv in leftker f by BILINEAR:def 18;

then A7: ex aa being Vector of V st

( aa = vv & ( for w0 being Vector of W holds f . (aa,w0) = 0. F_Complex ) ) ;

assume B = b1 + (RKer (f *')) ; :: thesis: y = f . (a1,b1)

then b in b1 + (RKer (f *')) by A4, VECTSP_4:44;

then consider ww being Vector of W such that

A8: ww in RKer (f *') and

A9: b = b1 + ww by VECTSP_4:42;

ww in the carrier of (RKer (f *')) by A8, STRUCT_0:def 5;

then ww in rightker (f *') by BILINEAR:def 19;

then A10: ex bb being Vector of W st

( bb = ww & ( for v0 being Vector of V holds f . (v0,bb) = 0. F_Complex ) ) by A1;

thus y = ((f . (a1,b1)) + (f . (a1,ww))) + ((f . (vv,b1)) + (f . (vv,ww))) by A6, A9, BILINEAR:28

.= ((f . (a1,b1)) + (0. F_Complex)) + ((f . (vv,b1)) + (f . (vv,ww))) by A10

.= ((f . (a1,b1)) + (0. F_Complex)) + ((0. F_Complex) + (f . (vv,ww))) by A7

.= (f . (a1,b1)) + ((0. F_Complex) + (f . (vv,ww))) by RLVECT_1:def 4

.= (f . (a1,b1)) + (f . (vv,ww)) by RLVECT_1:4

.= (f . (a1,b1)) + (0. F_Complex) by A7

.= f . (a1,b1) by RLVECT_1:def 4 ; :: thesis: verum

end;y = f . (a1,b1)

let b1 be Vector of W; :: thesis: ( A = a1 + (LKer f) & B = b1 + (RKer (f *')) implies y = f . (a1,b1) )

assume A = a1 + (LKer f) ; :: thesis: ( B = b1 + (RKer (f *')) implies y = f . (a1,b1) )

then a in a1 + (LKer f) by A3, VECTSP_4:44;

then consider vv being Vector of V such that

A5: vv in LKer f and

A6: a = a1 + vv by VECTSP_4:42;

vv in the carrier of (LKer f) by A5, STRUCT_0:def 5;

then vv in leftker f by BILINEAR:def 18;

then A7: ex aa being Vector of V st

( aa = vv & ( for w0 being Vector of W holds f . (aa,w0) = 0. F_Complex ) ) ;

assume B = b1 + (RKer (f *')) ; :: thesis: y = f . (a1,b1)

then b in b1 + (RKer (f *')) by A4, VECTSP_4:44;

then consider ww being Vector of W such that

A8: ww in RKer (f *') and

A9: b = b1 + ww by VECTSP_4:42;

ww in the carrier of (RKer (f *')) by A8, STRUCT_0:def 5;

then ww in rightker (f *') by BILINEAR:def 19;

then A10: ex bb being Vector of W st

( bb = ww & ( for v0 being Vector of V holds f . (v0,bb) = 0. F_Complex ) ) by A1;

thus y = ((f . (a1,b1)) + (f . (a1,ww))) + ((f . (vv,b1)) + (f . (vv,ww))) by A6, A9, BILINEAR:28

.= ((f . (a1,b1)) + (0. F_Complex)) + ((f . (vv,b1)) + (f . (vv,ww))) by A10

.= ((f . (a1,b1)) + (0. F_Complex)) + ((0. F_Complex) + (f . (vv,ww))) by A7

.= (f . (a1,b1)) + ((0. F_Complex) + (f . (vv,ww))) by RLVECT_1:def 4

.= (f . (a1,b1)) + (f . (vv,ww)) by RLVECT_1:4

.= (f . (a1,b1)) + (0. F_Complex) by A7

.= f . (a1,b1) by RLVECT_1:def 4 ; :: thesis: verum

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

for B being Vector of (VectQuot (W,(RKer (f *')))) holds S

reconsider ff = ff as Form of (VectQuot (V,(LKer f))),(VectQuot (W,(RKer (f *')))) ;

A12: CosetSet (V,(LKer f)) = the carrier of (VectQuot (V,(LKer f))) by VECTSP10:def 6;

A13: now :: thesis: for ww being Vector of (VectQuot (W,(RKer (f *')))) holds FunctionalSAF (ff,ww) is homogeneous

A17:
CosetSet (W,(RKer (f *'))) = the carrier of (VectQuot (W,(RKer (f *'))))
by VECTSP10:def 6;let ww be Vector of (VectQuot (W,(RKer (f *')))); :: thesis: FunctionalSAF (ff,ww) is homogeneous

consider w being Vector of W such that

A14: ww = w + (RKer (f *')) by VECTSP10:22;

set ffw = FunctionalSAF (ff,ww);

end;consider w being Vector of W such that

A14: ww = w + (RKer (f *')) by VECTSP10:22;

set ffw = FunctionalSAF (ff,ww);

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

for r being Element of F_Complex holds (FunctionalSAF (ff,ww)) . (r * A) = r * ((FunctionalSAF (ff,ww)) . A)

hence
FunctionalSAF (ff,ww) is homogeneous
; :: thesis: verumfor r being Element of F_Complex holds (FunctionalSAF (ff,ww)) . (r * A) = r * ((FunctionalSAF (ff,ww)) . A)

let A be Vector of (VectQuot (V,(LKer f))); :: thesis: for r being Element of F_Complex holds (FunctionalSAF (ff,ww)) . (r * A) = r * ((FunctionalSAF (ff,ww)) . A)

let r be Element of F_Complex; :: thesis: (FunctionalSAF (ff,ww)) . (r * A) = r * ((FunctionalSAF (ff,ww)) . A)

consider a being Vector of V such that

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

A16: ( the lmult of (VectQuot (V,(LKer f))) = lmultCoset (V,(LKer f)) & (lmultCoset (V,(LKer f))) . (r,A) = (r * a) + (LKer f) ) by A12, A15, VECTSP10:def 5, VECTSP10:def 6;

thus (FunctionalSAF (ff,ww)) . (r * A) = ff . (( the lmult of (VectQuot (V,(LKer f))) . (r,A)),ww) by BILINEAR:9

.= f . ((r * a),w) by A11, A14, A16

.= r * (f . (a,w)) by BILINEAR:31

.= r * (ff . (A,ww)) by A11, A14, A15

.= r * ((FunctionalSAF (ff,ww)) . A) by BILINEAR:9 ; :: thesis: verum

end;let r be Element of F_Complex; :: thesis: (FunctionalSAF (ff,ww)) . (r * A) = r * ((FunctionalSAF (ff,ww)) . A)

consider a being Vector of V such that

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

A16: ( the lmult of (VectQuot (V,(LKer f))) = lmultCoset (V,(LKer f)) & (lmultCoset (V,(LKer f))) . (r,A) = (r * a) + (LKer f) ) by A12, A15, VECTSP10:def 5, VECTSP10:def 6;

thus (FunctionalSAF (ff,ww)) . (r * A) = ff . (( the lmult of (VectQuot (V,(LKer f))) . (r,A)),ww) by BILINEAR:9

.= f . ((r * a),w) by A11, A14, A16

.= r * (f . (a,w)) by BILINEAR:31

.= r * (ff . (A,ww)) by A11, A14, A15

.= r * ((FunctionalSAF (ff,ww)) . A) by BILINEAR:9 ; :: thesis: verum

A18: now :: thesis: for vv being Vector of (VectQuot (V,(LKer f))) holds FunctionalFAF (ff,vv) is cmplxhomogeneous

let vv be Vector of (VectQuot (V,(LKer f))); :: thesis: FunctionalFAF (ff,vv) is cmplxhomogeneous

consider v being Vector of V such that

A19: vv = v + (LKer f) by VECTSP10:22;

set ffv = FunctionalFAF (ff,vv);

end;consider v being Vector of V such that

A19: vv = v + (LKer f) by VECTSP10:22;

set ffv = FunctionalFAF (ff,vv);

now :: thesis: for A being Vector of (VectQuot (W,(RKer (f *'))))

for r being Element of F_Complex holds (FunctionalFAF (ff,vv)) . (r * A) = (r *') * ((FunctionalFAF (ff,vv)) . A)

hence
FunctionalFAF (ff,vv) is cmplxhomogeneous
; :: thesis: verumfor r being Element of F_Complex holds (FunctionalFAF (ff,vv)) . (r * A) = (r *') * ((FunctionalFAF (ff,vv)) . A)

let A be Vector of (VectQuot (W,(RKer (f *')))); :: thesis: for r being Element of F_Complex holds (FunctionalFAF (ff,vv)) . (r * A) = (r *') * ((FunctionalFAF (ff,vv)) . A)

let r be Element of F_Complex; :: thesis: (FunctionalFAF (ff,vv)) . (r * A) = (r *') * ((FunctionalFAF (ff,vv)) . A)

consider a being Vector of W such that

A20: A = a + (RKer (f *')) by VECTSP10:22;

A21: ( the lmult of (VectQuot (W,(RKer (f *')))) = lmultCoset (W,(RKer (f *'))) & (lmultCoset (W,(RKer (f *')))) . (r,A) = (r * a) + (RKer (f *')) ) by A17, A20, VECTSP10:def 5, VECTSP10:def 6;

thus (FunctionalFAF (ff,vv)) . (r * A) = ff . (vv,( the lmult of (VectQuot (W,(RKer (f *')))) . (r,A))) by BILINEAR:8

.= f . (v,(r * a)) by A11, A19, A21

.= (r *') * (f . (v,a)) by Th27

.= (r *') * (ff . (vv,A)) by A11, A19, A20

.= (r *') * ((FunctionalFAF (ff,vv)) . A) by BILINEAR:8 ; :: thesis: verum

end;let r be Element of F_Complex; :: thesis: (FunctionalFAF (ff,vv)) . (r * A) = (r *') * ((FunctionalFAF (ff,vv)) . A)

consider a being Vector of W such that

A20: A = a + (RKer (f *')) by VECTSP10:22;

A21: ( the lmult of (VectQuot (W,(RKer (f *')))) = lmultCoset (W,(RKer (f *'))) & (lmultCoset (W,(RKer (f *')))) . (r,A) = (r * a) + (RKer (f *')) ) by A17, A20, VECTSP10:def 5, VECTSP10:def 6;

thus (FunctionalFAF (ff,vv)) . (r * A) = ff . (vv,( the lmult of (VectQuot (W,(RKer (f *')))) . (r,A))) by BILINEAR:8

.= f . (v,(r * a)) by A11, A19, A21

.= (r *') * (f . (v,a)) by Th27

.= (r *') * (ff . (vv,A)) by A11, A19, A20

.= (r *') * ((FunctionalFAF (ff,vv)) . A) by BILINEAR:8 ; :: thesis: verum

A22: now :: thesis: for ww being Vector of (VectQuot (W,(RKer (f *')))) holds FunctionalSAF (ff,ww) is additive

let ww be Vector of (VectQuot (W,(RKer (f *')))); :: thesis: FunctionalSAF (ff,ww) is additive

consider w being Vector of W such that

A23: ww = w + (RKer (f *')) by VECTSP10:22;

set ffw = FunctionalSAF (ff,ww);

end;consider w being Vector of W such that

A23: ww = w + (RKer (f *')) by VECTSP10:22;

set ffw = FunctionalSAF (ff,ww);

now :: thesis: for A, B being Vector of (VectQuot (V,(LKer f))) holds (FunctionalSAF (ff,ww)) . (A + B) = ((FunctionalSAF (ff,ww)) . A) + ((FunctionalSAF (ff,ww)) . B)

hence
FunctionalSAF (ff,ww) is additive
; :: thesis: verumlet A, B be Vector of (VectQuot (V,(LKer f))); :: thesis: (FunctionalSAF (ff,ww)) . (A + B) = ((FunctionalSAF (ff,ww)) . A) + ((FunctionalSAF (ff,ww)) . B)

consider a being Vector of V such that

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

consider b being Vector of V such that

A25: B = b + (LKer f) by VECTSP10:22;

A26: ( the addF of (VectQuot (V,(LKer f))) = addCoset (V,(LKer f)) & (addCoset (V,(LKer f))) . (A,B) = (a + b) + (LKer f) ) by A12, A24, A25, VECTSP10:def 3, VECTSP10:def 6;

thus (FunctionalSAF (ff,ww)) . (A + B) = ff . (( the addF of (VectQuot (V,(LKer f))) . (A,B)),ww) by BILINEAR:9

.= f . ((a + b),w) by A11, A23, A26

.= (f . (a,w)) + (f . (b,w)) by BILINEAR:26

.= (ff . (A,ww)) + (f . (b,w)) by A11, A23, A24

.= (ff . (A,ww)) + (ff . (B,ww)) by A11, A23, A25

.= ((FunctionalSAF (ff,ww)) . A) + (ff . (B,ww)) by BILINEAR:9

.= ((FunctionalSAF (ff,ww)) . A) + ((FunctionalSAF (ff,ww)) . B) by BILINEAR:9 ; :: thesis: verum

end;consider a being Vector of V such that

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

consider b being Vector of V such that

A25: B = b + (LKer f) by VECTSP10:22;

A26: ( the addF of (VectQuot (V,(LKer f))) = addCoset (V,(LKer f)) & (addCoset (V,(LKer f))) . (A,B) = (a + b) + (LKer f) ) by A12, A24, A25, VECTSP10:def 3, VECTSP10:def 6;

thus (FunctionalSAF (ff,ww)) . (A + B) = ff . (( the addF of (VectQuot (V,(LKer f))) . (A,B)),ww) by BILINEAR:9

.= f . ((a + b),w) by A11, A23, A26

.= (f . (a,w)) + (f . (b,w)) by BILINEAR:26

.= (ff . (A,ww)) + (f . (b,w)) by A11, A23, A24

.= (ff . (A,ww)) + (ff . (B,ww)) by A11, A23, A25

.= ((FunctionalSAF (ff,ww)) . A) + (ff . (B,ww)) by BILINEAR:9

.= ((FunctionalSAF (ff,ww)) . A) + ((FunctionalSAF (ff,ww)) . B) by BILINEAR:9 ; :: thesis: verum

now :: thesis: for vv being Vector of (VectQuot (V,(LKer f))) holds FunctionalFAF (ff,vv) is additive

then reconsider ff = ff as sesquilinear-Form of (VectQuot (V,(LKer f))),(VectQuot (W,(RKer (f *')))) by A22, A13, A18, Def4, BILINEAR:def 11, BILINEAR:def 12, BILINEAR:def 14;let vv be Vector of (VectQuot (V,(LKer f))); :: thesis: FunctionalFAF (ff,vv) is additive

consider v being Vector of V such that

A27: vv = v + (LKer f) by VECTSP10:22;

set ffv = FunctionalFAF (ff,vv);

end;consider v being Vector of V such that

A27: vv = v + (LKer f) by VECTSP10:22;

set ffv = FunctionalFAF (ff,vv);

now :: thesis: for A, B being Vector of (VectQuot (W,(RKer (f *')))) holds (FunctionalFAF (ff,vv)) . (A + B) = ((FunctionalFAF (ff,vv)) . A) + ((FunctionalFAF (ff,vv)) . B)

hence
FunctionalFAF (ff,vv) is additive
; :: thesis: verumlet A, B be Vector of (VectQuot (W,(RKer (f *')))); :: thesis: (FunctionalFAF (ff,vv)) . (A + B) = ((FunctionalFAF (ff,vv)) . A) + ((FunctionalFAF (ff,vv)) . B)

consider a being Vector of W such that

A28: A = a + (RKer (f *')) by VECTSP10:22;

consider b being Vector of W such that

A29: B = b + (RKer (f *')) by VECTSP10:22;

A30: ( the addF of (VectQuot (W,(RKer (f *')))) = addCoset (W,(RKer (f *'))) & (addCoset (W,(RKer (f *')))) . (A,B) = (a + b) + (RKer (f *')) ) by A17, A28, A29, VECTSP10:def 3, VECTSP10:def 6;

thus (FunctionalFAF (ff,vv)) . (A + B) = ff . (vv,( the addF of (VectQuot (W,(RKer (f *')))) . (A,B))) by BILINEAR:8

.= f . (v,(a + b)) by A11, A27, A30

.= (f . (v,a)) + (f . (v,b)) by BILINEAR:27

.= (ff . (vv,A)) + (f . (v,b)) by A11, A27, A28

.= (ff . (vv,A)) + (ff . (vv,B)) by A11, A27, A29

.= ((FunctionalFAF (ff,vv)) . A) + (ff . (vv,B)) by BILINEAR:8

.= ((FunctionalFAF (ff,vv)) . A) + ((FunctionalFAF (ff,vv)) . B) by BILINEAR:8 ; :: thesis: verum

end;consider a being Vector of W such that

A28: A = a + (RKer (f *')) by VECTSP10:22;

consider b being Vector of W such that

A29: B = b + (RKer (f *')) by VECTSP10:22;

A30: ( the addF of (VectQuot (W,(RKer (f *')))) = addCoset (W,(RKer (f *'))) & (addCoset (W,(RKer (f *')))) . (A,B) = (a + b) + (RKer (f *')) ) by A17, A28, A29, VECTSP10:def 3, VECTSP10:def 6;

thus (FunctionalFAF (ff,vv)) . (A + B) = ff . (vv,( the addF of (VectQuot (W,(RKer (f *')))) . (A,B))) by BILINEAR:8

.= f . (v,(a + b)) by A11, A27, A30

.= (f . (v,a)) + (f . (v,b)) by BILINEAR:27

.= (ff . (vv,A)) + (f . (v,b)) by A11, A27, A28

.= (ff . (vv,A)) + (ff . (vv,B)) by A11, A27, A29

.= ((FunctionalFAF (ff,vv)) . A) + (ff . (vv,B)) by BILINEAR:8

.= ((FunctionalFAF (ff,vv)) . A) + ((FunctionalFAF (ff,vv)) . B) by BILINEAR:8 ; :: thesis: verum

take ff ; :: thesis: for A being Vector of (VectQuot (V,(LKer f)))

for B being Vector of (VectQuot (W,(RKer (f *'))))

for v being Vector of V

for w being Vector of W st A = v + (LKer f) & B = w + (RKer (f *')) holds

ff . (A,B) = f . (v,w)

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

for B being Vector of (VectQuot (W,(RKer (f *'))))

for v being Vector of V

for w being Vector of W st A = v + (LKer f) & B = w + (RKer (f *')) holds

ff . (A,B) = f . (v,w) by A11; :: thesis: verum