let K be Field; :: thesis: for V, W being non trivial VectSp of K
for f being constant linear-Functional of V
for g being constant 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 constant linear-Functional of V
for g being constant linear-Functional of W holds QForm (FormFunctional (f,g)) = FormFunctional ((CQFunctional f),(CQFunctional g))
let f be constant linear-Functional of V; :: thesis: for g being constant linear-Functional of W holds QForm (FormFunctional (f,g)) = FormFunctional ((CQFunctional f),(CQFunctional g))
let g be constant 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 Th54;
thus QForm (FormFunctional (f,g)) = RQForm (LQForm (FormFunctional (f,g))) by Th48
.= RQForm (FormFunctional ((CQFunctional f),g)) by A2, A3, Th54
.= FormFunctional ((CQFunctional f),(CQFunctional g)) by A1, Th55 ; :: thesis: verum