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)

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

hence
mult1 = mult2
; :: thesis: verum
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;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