consider f being non trivial V14() linear-Functional of V;
take ff = FormFunctional (f,f); :: 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

let v, w be Vector of V; :: thesis: ff . (v,w) = ff . (w,v)
thus ff . (v,w) = (f . v) * (f . w) by Def11
.= ff . (w,v) by Def11 ; :: 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 ) by Def26; :: thesis: verum