set f = InnerProduct L;
for v, w being Vector of L holds (InnerProduct L) . (v,w) = (InnerProduct L) . (w,v)

proof

let v, w be Vector of L; :: thesis: (InnerProduct L) . (v,w) = (InnerProduct L) . (w,v)
thus (InnerProduct L) . (v,w) = <;v,w;>
.= <;w,v;> by ZMODLAT1:def 3
.= (InnerProduct L) . (w,v) ; :: thesis: verum

end;

hence InnerProduct L is symmetric ; :: thesis: verum