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

let v, w be Vector of V; :: thesis: ff . (v,w) = ff . (w,v)
thus ff . (v,w) = ( the non trivial V14() linear-Functional of V . v) * ( the non trivial V14() linear-Functional of V . 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