let n, m be Element of F_Real; :: thesis: ( ( for b being OrdBasis of V holds n = Det (GramMatrix (f,b)) ) & ( for b being OrdBasis of V holds m = Det (GramMatrix (f,b)) ) implies n = m )
assume that
A1: for b being OrdBasis of V holds Det (GramMatrix (f,b)) = n and
A2: for b being OrdBasis of V holds Det (GramMatrix (f,b)) = m ; :: thesis: n = m
set b1 = the OrdBasis of V;
Det (GramMatrix (f, the OrdBasis of V)) = n by A1;
hence n = m by A2; :: thesis: verum