set f = the non trivial constant linear-Functional of V;
take ff = FormFunctional ( the non trivial constant linear-Functional of V, the non trivial constant linear-Functional of V); :: thesis: ( ff is symmetric & not ff is trivial & not ff is constant & ff is additiveFAF & ff is homogeneousFAF & ff is additiveSAF & ff is homogeneousSAF )

now :: thesis: for v, w being Vector of V holds ff . (v,w) = ff . (w,v)

let v, w be Vector of V; :: thesis: ff . (v,w) = ff . (w,v)
thus ff . (v,w) = ( the non trivial constant linear-Functional of V . v) * ( the non trivial constant linear-Functional of V . w) by Def10
.= ff . (w,v) by Def10 ; :: thesis: verum

end;

hence ( ff is symmetric & not ff is trivial & not ff is constant & ff is additiveFAF & ff is homogeneousFAF & ff is additiveSAF & ff is homogeneousSAF ) ; :: thesis: verum