let scalar1, scalar2 be Function of [:(REAL n),(REAL n):],REAL ; :: thesis: ( ( for x, y being Element of REAL n holds scalar1 . x,y = Sum (mlt x,y) ) & ( for x, y being Element of REAL n holds scalar2 . x,y = Sum (mlt x,y) ) implies scalar1 = scalar2 )
assume that
A1: for x, y being Element of REAL n holds scalar1 . x,y = Sum (mlt x,y) and
A2: for x, y being Element of REAL n holds scalar2 . x,y = Sum (mlt x,y) ; :: thesis: scalar1 = scalar2
for x, y being Element of REAL n holds scalar1 . x,y = scalar2 . x,y

proof

let x, y be Element of REAL n; :: thesis: scalar1 . x,y = scalar2 . x,y
scalar1 . x,y = Sum (mlt x,y) by A1;
hence scalar1 . x,y = scalar2 . x,y by A2; :: thesis: verum

end;

hence scalar1 = scalar2 by BINOP_1:2; :: thesis: verum