let K be Field; :: thesis: for V, W being non trivial VectSp of K

for f being V17() linear-Functional of V

for g being V17() 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 V17() linear-Functional of V

for g being V17() linear-Functional of W holds QForm (FormFunctional (f,g)) = FormFunctional ((CQFunctional f),(CQFunctional g))

let f be V17() linear-Functional of V; :: thesis: for g being V17() linear-Functional of W holds QForm (FormFunctional (f,g)) = FormFunctional ((CQFunctional f),(CQFunctional g))

let g be V17() 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

for f being V17() linear-Functional of V

for g being V17() 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 V17() linear-Functional of V

for g being V17() linear-Functional of W holds QForm (FormFunctional (f,g)) = FormFunctional ((CQFunctional f),(CQFunctional g))

let f be V17() linear-Functional of V; :: thesis: for g being V17() linear-Functional of W holds QForm (FormFunctional (f,g)) = FormFunctional ((CQFunctional f),(CQFunctional g))

let g be V17() 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