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