let K be Field; :: thesis: for V, W being non trivial VectSp of K
for f being V14() linear-Functional of V
for g being V14() 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 V14() linear-Functional of V
for g being V14() linear-Functional of W holds QForm (FormFunctional (f,g)) = FormFunctional ((CQFunctional f),(CQFunctional g))
let f be V14() linear-Functional of V; :: thesis: for g being V14() linear-Functional of W holds QForm (FormFunctional (f,g)) = FormFunctional ((CQFunctional f),(CQFunctional g))
let g be V14() 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