let mult1, mult2 be Function of [:REAL,(REAL n):],(REAL n); :: thesis: ( ( for r being Real
for x being Element of REAL n holds mult1 . (r,x) = r * x ) & ( for r being Real
for x being Element of REAL n holds mult2 . (r,x) = r * x ) implies mult1 = mult2 )
assume that
A2: for r being Real
for x being Element of REAL n holds mult1 . (r,x) = r * x and
A3: for r being 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 A2
.= mult2 . (r,x) by A3 ; :: thesis: verum

end;

hence mult1 = mult2 ; :: thesis: verum