set f = the non trivial V17() linear-Functional of V;

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

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

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: verumlet v, w be Vector of V; :: thesis: ff . (v,w) = ff . (w,v)

thus ff . (v,w) = ( the non trivial V17() linear-Functional of V . v) * ( the non trivial V17() linear-Functional of V . w) by Def10

.= ff . (w,v) by Def10 ; :: thesis: verum

end;thus ff . (v,w) = ( the non trivial V17() linear-Functional of V . v) * ( the non trivial V17() linear-Functional of V . w) by Def10

.= ff . (w,v) by Def10 ; :: thesis: verum