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
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
A2: v = va + (LKer f) by VECTSP10:23;
A3: r * v = (r * va) + (LKer f) by A2, VECTSP10:26;
reconsider A = w as Vector of (VectQuot V,(RKer (f *' ))) by Th59;
consider wa being Vector of V such that
A4: A = wa + (RKer (f *' )) by VECTSP10:23;
thus (FunctionalSAF sc,w) . (r * v) = (Q*Form f) . (r * v),w by BILINEAR:10
.= f . (r * va),wa by A4, A3, Def12
.= r * (f . va,wa) by BILINEAR:32
.= r * (sc . v,w) by A4, A2, 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
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
A6: v1 = va + (LKer f) by VECTSP10:23;
consider vb being Vector of V such that
A7: v2 = vb + (LKer f) by VECTSP10:23;
reconsider A = w as Vector of (VectQuot V,(RKer (f *' ))) by Th59;
consider wa being Vector of V such that
A8: A = wa + (RKer (f *' )) by VECTSP10:23;
A9: v1 + v2 = (va + vb) + (LKer f) by A6, A7, VECTSP10:27;
thus (FunctionalSAF sc,w) . (v1 + v2) = (Q*Form f) . (v1 + v2),w by BILINEAR:10
.= f . (va + vb),wa by A8, A9, Def12
.= (f . va,wa) + (f . vb,wa) by BILINEAR:27
.= (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: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;
A12: w = wa + (LKer f) by A11, Th59;
reconsider B = v as Vector of (VectQuot V,(RKer (f *' ))) by Th59;
consider va being Vector of V such that
A13: v = va + (LKer f) by VECTSP10:23;
A14: B = va + (RKer (f *' )) by A13, Th59;
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;

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)
reconsider A = v as Vector of (VectQuot V,(RKer (f *' ))) by Th59;
consider va being Vector of V such that
A15: v = va + (LKer f) by VECTSP10:23;
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