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