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

set vr = VectQuot (V,(RKer (f *')));

VectQuot (V,(RKer (f *'))) = VectQuot (V,(LKer f)) by Th56;

then reconsider sc = Q*Form f as Form of (VectQuot (V,(LKer f))),(VectQuot (V,(LKer f))) ;

A1: sc is homogeneousSAF

set vr = VectQuot (V,(RKer (f *')));

VectQuot (V,(RKer (f *'))) = VectQuot (V,(LKer f)) by Th56;

then reconsider sc = Q*Form f as Form of (VectQuot (V,(LKer f))),(VectQuot (V,(LKer f))) ;

A1: sc is homogeneousSAF

proof

A5:
sc is additiveSAF
let w be Vector of (VectQuot (V,(LKer f))); :: according to BILINEAR:def 14 :: thesis: FunctionalSAF (sc,w) is homogeneous

set fg = FunctionalSAF (sc,w);

let v be Vector of (VectQuot (V,(LKer f))); :: according to HAHNBAN1:def 8 :: thesis: for b_{1} being Element of the carrier of F_Complex holds (FunctionalSAF (sc,w)) . (b_{1} * v) = b_{1} * ((FunctionalSAF (sc,w)) . v)

let r be Scalar of ; :: thesis: (FunctionalSAF (sc,w)) . (r * v) = r * ((FunctionalSAF (sc,w)) . v)

consider va being Vector of V such that

A2: v = va + (LKer f) by VECTSP10:22;

A3: r * v = (r * va) + (LKer f) by A2, VECTSP10:25;

reconsider A = w as Vector of (VectQuot (V,(RKer (f *')))) by Th56;

consider wa being Vector of V such that

A4: A = wa + (RKer (f *')) by VECTSP10:22;

thus (FunctionalSAF (sc,w)) . (r * v) = (Q*Form f) . ((r * v),w) by BILINEAR:9

.= f . ((r * va),wa) by A4, A3, Def12

.= r * (f . (va,wa)) by BILINEAR:31

.= r * (sc . (v,w)) by A4, A2, Def12

.= r * ((FunctionalSAF (sc,w)) . v) by BILINEAR:9 ; :: thesis: verum

end;set fg = FunctionalSAF (sc,w);

let v be Vector of (VectQuot (V,(LKer f))); :: according to HAHNBAN1:def 8 :: thesis: for b

let r be Scalar of ; :: thesis: (FunctionalSAF (sc,w)) . (r * v) = r * ((FunctionalSAF (sc,w)) . v)

consider va being Vector of V such that

A2: v = va + (LKer f) by VECTSP10:22;

A3: r * v = (r * va) + (LKer f) by A2, VECTSP10:25;

reconsider A = w as Vector of (VectQuot (V,(RKer (f *')))) by Th56;

consider wa being Vector of V such that

A4: A = wa + (RKer (f *')) by VECTSP10:22;

thus (FunctionalSAF (sc,w)) . (r * v) = (Q*Form f) . ((r * v),w) by BILINEAR:9

.= f . ((r * va),wa) by A4, A3, Def12

.= r * (f . (va,wa)) by BILINEAR:31

.= r * (sc . (v,w)) by A4, A2, Def12

.= r * ((FunctionalSAF (sc,w)) . v) by BILINEAR:9 ; :: thesis: verum

proof

A10:
sc is hermitan
let w be Vector of (VectQuot (V,(LKer f))); :: according to BILINEAR:def 12 :: thesis: FunctionalSAF (sc,w) is additive

set fg = FunctionalSAF (sc,w);

let v1, v2 be Vector of (VectQuot (V,(LKer f))); :: according to VECTSP_1:def 19 :: thesis: (FunctionalSAF (sc,w)) . (v1 + v2) = ((FunctionalSAF (sc,w)) . v1) + ((FunctionalSAF (sc,w)) . v2)

consider va being Vector of V such that

A6: v1 = va + (LKer f) by VECTSP10:22;

consider vb being Vector of V such that

A7: v2 = vb + (LKer f) by VECTSP10:22;

reconsider A = w as Vector of (VectQuot (V,(RKer (f *')))) by Th56;

consider wa being Vector of V such that

A8: A = wa + (RKer (f *')) by VECTSP10:22;

A9: v1 + v2 = (va + vb) + (LKer f) by A6, A7, VECTSP10:26;

thus (FunctionalSAF (sc,w)) . (v1 + v2) = (Q*Form f) . ((v1 + v2),w) by BILINEAR:9

.= f . ((va + vb),wa) by A8, A9, Def12

.= (f . (va,wa)) + (f . (vb,wa)) by BILINEAR:26

.= (sc . (v1,w)) + (f . (vb,wa)) by A8, A6, Def12

.= (sc . (v1,w)) + (sc . (v2,w)) by A8, A7, Def12

.= ((FunctionalSAF (sc,w)) . v1) + (sc . (v2,w)) by BILINEAR:9

.= ((FunctionalSAF (sc,w)) . v1) + ((FunctionalSAF (sc,w)) . v2) by BILINEAR:9 ; :: thesis: verum

end;set fg = FunctionalSAF (sc,w);

let v1, v2 be Vector of (VectQuot (V,(LKer f))); :: according to VECTSP_1:def 19 :: thesis: (FunctionalSAF (sc,w)) . (v1 + v2) = ((FunctionalSAF (sc,w)) . v1) + ((FunctionalSAF (sc,w)) . v2)

consider va being Vector of V such that

A6: v1 = va + (LKer f) by VECTSP10:22;

consider vb being Vector of V such that

A7: v2 = vb + (LKer f) by VECTSP10:22;

reconsider A = w as Vector of (VectQuot (V,(RKer (f *')))) by Th56;

consider wa being Vector of V such that

A8: A = wa + (RKer (f *')) by VECTSP10:22;

A9: v1 + v2 = (va + vb) + (LKer f) by A6, A7, VECTSP10:26;

thus (FunctionalSAF (sc,w)) . (v1 + v2) = (Q*Form f) . ((v1 + v2),w) by BILINEAR:9

.= f . ((va + vb),wa) by A8, A9, Def12

.= (f . (va,wa)) + (f . (vb,wa)) by BILINEAR:26

.= (sc . (v1,w)) + (f . (vb,wa)) by A8, A6, Def12

.= (sc . (v1,w)) + (sc . (v2,w)) by A8, A7, Def12

.= ((FunctionalSAF (sc,w)) . v1) + (sc . (v2,w)) by BILINEAR:9

.= ((FunctionalSAF (sc,w)) . v1) + ((FunctionalSAF (sc,w)) . v2) by BILINEAR:9 ; :: thesis: verum

proof

sc is diagReR+0valued
let v, w be Vector of (VectQuot (V,(LKer f))); :: according to HERMITAN:def 5 :: thesis: sc . (v,w) = (sc . (w,v)) *'

reconsider A = w as Vector of (VectQuot (V,(RKer (f *')))) by Th56;

consider wa being Vector of V such that

A11: A = wa + (RKer (f *')) by VECTSP10:22;

A12: w = wa + (LKer f) by A11, Th56;

reconsider B = v as Vector of (VectQuot (V,(RKer (f *')))) by Th56;

consider va being Vector of V such that

A13: v = va + (LKer f) by VECTSP10:22;

A14: B = va + (RKer (f *')) by A13, Th56;

thus sc . (v,w) = f . (va,wa) by A11, A13, Def12

.= (f . (wa,va)) *' by Def5

.= (sc . (w,v)) *' by A14, A12, Def12 ; :: thesis: verum

end;reconsider A = w as Vector of (VectQuot (V,(RKer (f *')))) by Th56;

consider wa being Vector of V such that

A11: A = wa + (RKer (f *')) by VECTSP10:22;

A12: w = wa + (LKer f) by A11, Th56;

reconsider B = v as Vector of (VectQuot (V,(RKer (f *')))) by Th56;

consider va being Vector of V such that

A13: v = va + (LKer f) by VECTSP10:22;

A14: B = va + (RKer (f *')) by A13, Th56;

thus sc . (v,w) = f . (va,wa) by A11, A13, Def12

.= (f . (wa,va)) *' by Def5

.= (sc . (w,v)) *' by A14, A12, Def12 ; :: thesis: verum

proof

hence
Q*Form f is diagReR+0valued hermitan-Form of (VectQuot (V,(LKer f)))
by A1, A5, A10; :: thesis: verum
let v be Vector of (VectQuot (V,(LKer f))); :: according to HERMITAN:def 7 :: thesis: 0 <= Re (sc . (v,v))

reconsider A = v as Vector of (VectQuot (V,(RKer (f *')))) by Th56;

consider va being Vector of V such that

A15: v = va + (LKer f) by VECTSP10:22;

A = va + (RKer (f *')) by A15, Th56;

then sc . (v,v) = f . (va,va) by A15, Def12;

hence 0 <= Re (sc . (v,v)) by Def7; :: thesis: verum

end;reconsider A = v as Vector of (VectQuot (V,(RKer (f *')))) by Th56;

consider va being Vector of V such that

A15: v = va + (LKer f) by VECTSP10:22;

A = va + (RKer (f *')) by A15, Th56;

then sc . (v,v) = f . (va,va) by A15, Def12;

hence 0 <= Re (sc . (v,v)) by Def7; :: thesis: verum