let mult1, mult2 be Function of [:REAL ,(REAL n):],(REAL n); :: thesis: ( ( for r being Element of REAL
for x being Element of REAL n holds mult1 . r,x = r * x ) & ( for r being Element of REAL
for x being Element of REAL n holds mult2 . r,x = r * x ) implies mult1 = mult2 )
assume that
A1: for r being Element of REAL
for x being Element of REAL n holds mult1 . r,x = r * x and
A2: for r being Element of REAL
for x being Element of REAL n holds mult2 . r,x = r * x ; :: thesis: mult1 = mult2
for r being Element of REAL
for x being Element of REAL n holds mult1 . r,x = mult2 . r,x

proof

let r be Element of REAL ; :: thesis: for x being Element of REAL n holds mult1 . r,x = mult2 . r,x
let x be Element of REAL n; :: thesis: mult1 . r,x = mult2 . r,x
thus mult1 . r,x = r * x by A1
.= mult2 . r,x by A2 ; :: thesis: verum

end;

hence mult1 = mult2 by BINOP_1:2; :: thesis: verum