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)

hence GramMatrix (f,b) is symmetric by MATRIX_6:def 5; :: thesis: verum

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

then
GramMatrix (f,b) = (GramMatrix (f,b)) @
by MATRIX_0:27;
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;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

hence GramMatrix (f,b) is symmetric by MATRIX_6:def 5; :: thesis: verum