set vq = VectQuot V,(LKer f);
set vr = VectQuot V,(RKer (f *' ));
VectQuot V,(RKer (f *' )) = VectQuot V,(LKer f) by Th59;
then reconsider sc = Q*Form f as Form of (VectQuot V,(LKer f)),(VectQuot V,(LKer f)) ;
A1: sc is homogeneousSAF

proof

let w be Vector of (VectQuot V,(LKer f)); :: according to BILINEAR:def 15 :: thesis: FunctionalSAF sc,w is homogeneous
reconsider A = w as Vector of (VectQuot V,(RKer (f *' ))) by Th59;
consider wa being Vector of V such that
A2: A = wa + (RKer (f *' )) by VECTSP10:23;
set fg = FunctionalSAF sc,w;
let v be Vector of (VectQuot V,(LKer f)); :: according to HAHNBAN1:def 12 :: thesis: for b₁ being Element of the carrier of F_Complex holds (FunctionalSAF sc,w) . (b₁ * v) = b₁ * ((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
A3: v = va + (LKer f) by VECTSP10:23;
A4: r * v = (r * va) + (LKer f) by A3, VECTSP10:26;
thus (FunctionalSAF sc,w) . (r * v) = (Q*Form f) . (r * v),w by BILINEAR:10
.= f . (r * va),wa by A2, A4, Def12
.= r * (f . va,wa) by BILINEAR:32
.= r * (sc . v,w) by A2, A3, Def12
.= r * ((FunctionalSAF sc,w) . v) by BILINEAR:10 ; :: thesis: verum

end;

A5: sc is additiveSAF

proof

let w be Vector of (VectQuot V,(LKer f)); :: according to BILINEAR:def 13 :: thesis: FunctionalSAF sc,w is additive
reconsider A = w as Vector of (VectQuot V,(RKer (f *' ))) by Th59;
consider wa being Vector of V such that
A6: A = wa + (RKer (f *' )) by VECTSP10:23;
set fg = FunctionalSAF sc,w;
let v1, v2 be Vector of (VectQuot V,(LKer f)); :: according to HAHNBAN1:def 11 :: thesis: (FunctionalSAF sc,w) . (v1 + v2) = ((FunctionalSAF sc,w) . v1) + ((FunctionalSAF sc,w) . v2)
consider va being Vector of V such that
A7: v1 = va + (LKer f) by VECTSP10:23;
consider vb being Vector of V such that
A8: v2 = vb + (LKer f) by VECTSP10:23;
A9: v1 + v2 = (va + vb) + (LKer f) by A7, A8, VECTSP10:27;
thus (FunctionalSAF sc,w) . (v1 + v2) = (Q*Form f) . (v1 + v2),w by BILINEAR:10
.= f . (va + vb),wa by A6, A9, Def12
.= (f . va,wa) + (f . vb,wa) by BILINEAR:27
.= (sc . v1,w) + (f . vb,wa) by A6, A7, Def12
.= (sc . v1,w) + (sc . v2,w) by A6, A8, Def12
.= ((FunctionalSAF sc,w) . v1) + (sc . v2,w) by BILINEAR:10
.= ((FunctionalSAF sc,w) . v1) + ((FunctionalSAF sc,w) . v2) by BILINEAR:10 ; :: thesis: verum

end;

A10: sc is hermitan

proof

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 Th59;
consider wa being Vector of V such that
A11: A = wa + (RKer (f *' )) by VECTSP10:23;
reconsider B = v as Vector of (VectQuot V,(RKer (f *' ))) by Th59;
consider va being Vector of V such that
A12: v = va + (LKer f) by VECTSP10:23;
A13: B = va + (RKer (f *' )) by A12, Th59;
A14: w = wa + (LKer f) by A11, Th59;
thus sc . v,w = f . va,wa by A11, A12, Def12
.= (f . wa,va) *' by Def5
.= (sc . w,v) *' by A13, A14, Def12 ; :: thesis: verum

end;

sc is diagReR+0valued

proof

let v be Vector of (VectQuot V,(LKer f)); :: according to HERMITAN:def 7 :: thesis: 0 <= Re (sc . v,v)
consider va being Vector of V such that
A15: v = va + (LKer f) by VECTSP10:23;
reconsider A = v as Vector of (VectQuot V,(RKer (f *' ))) by Th59;
A = va + (RKer (f *' )) by A15, Th59;
then sc . v,v = f . va,va by A15, Def12;
hence 0 <= Re (sc . v,v) by Def7; :: thesis: verum

end;

hence Q*Form f is diagReR+0valued hermitan-Form of (VectQuot V,(LKer f)) by A1, A5, A10; :: thesis: verum