let K be Field; :: thesis: for V, W being non trivial VectSp of K
for f being V11() linear-Functional of V
for g being V11() linear-Functional of W holds QForm (FormFunctional f,g) = FormFunctional (CQFunctional f),(CQFunctional g)
let V, W be non trivial VectSp of K; :: thesis: for f being V11() linear-Functional of V
for g being V11() linear-Functional of W holds QForm (FormFunctional f,g) = FormFunctional (CQFunctional f),(CQFunctional g)
let f be V11() linear-Functional of V; :: thesis: for g being V11() linear-Functional of W holds QForm (FormFunctional f,g) = FormFunctional (CQFunctional f),(CQFunctional g)
let g be V11() linear-Functional of W; :: thesis: QForm (FormFunctional f,g) = FormFunctional (CQFunctional f),(CQFunctional g)
A1: CQFunctional f <> 0Functional (VectQuot V,(Ker f)) ;
A2: g <> 0Functional W ;
then A3: LQForm (FormFunctional f,g) = FormFunctional (CQFunctional f),g by Th55;
thus QForm (FormFunctional f,g) = RQForm (LQForm (FormFunctional f,g)) by Th49
.= RQForm (FormFunctional (CQFunctional f),g) by A2, A3, Th55
.= FormFunctional (CQFunctional f),(CQFunctional g) by A1, Th56 ; :: thesis: verum