set M = GramMatrix (f,b);
set MT = (GramMatrix (f,b)) @ ;
for i, j being Nat st [i,j] in Indices (GramMatrix (f,b)) holds
(GramMatrix (f,b)) * (i,j) = ((GramMatrix (f,b)) @) * (i,j)

proof

let i, j be Nat; :: thesis: ( [i,j] in Indices (GramMatrix (f,b)) implies (GramMatrix (f,b)) * (i,j) = ((GramMatrix (f,b)) @) * (i,j) )
assume A1: [i,j] in Indices (GramMatrix (f,b)) ; :: thesis: (GramMatrix (f,b)) * (i,j) = ((GramMatrix (f,b)) @) * (i,j)
A2: [j,i] in Indices (GramMatrix (f,b)) by A1, MATRIX_0:28;
Indices (GramMatrix (f,b)) = [:(Seg (rank V)),(Seg (rank V)):] by MATRIX_0:24;
then A3: ( i in Seg (rank V) & j in Seg (rank V) ) by A1, ZFMISC_1:87;
len b = rank V by ZMATRLIN:49;
then A4: ( i in dom b & j in dom b ) by A3, FINSEQ_1:def 3;
thus (GramMatrix (f,b)) * (i,j) = f . ((b /. i),(b /. j)) by A4, ZMODLAT1:def 32
.= f . ((b /. j),(b /. i)) by defSymForm
.= (BilinearM (f,b,b)) * (j,i) by A4, ZMODLAT1:def 32
.= ((GramMatrix (f,b)) @) * (i,j) by A2, MATRIX_0:def 6 ; :: thesis: verum

end;

then GramMatrix (f,b) = (GramMatrix (f,b)) @ by MATRIX_0:27;
hence GramMatrix (f,b) is symmetric by MATRIX_6:def 5; :: thesis: verum