let mult1, mult2 be Function of [:REAL ,the_set_of_RealSequences :],the_set_of_RealSequences ; :: thesis: ( ( for r, x being set st r in REAL & x in the_set_of_RealSequences holds
mult1 . r,x = (R_id r) (#) (seq_id x) ) & ( for r, x being set st r in REAL & x in the_set_of_RealSequences holds
mult2 . r,x = (R_id r) (#) (seq_id x) ) implies mult1 = mult2 )
assume that
A1: for r, x being set st r in REAL & x in the_set_of_RealSequences holds
mult1 . r,x = (R_id r) (#) (seq_id x) and
A2: for r, x being set st r in REAL & x in the_set_of_RealSequences holds
mult2 . r,x = (R_id r) (#) (seq_id x) ; :: thesis: mult1 = mult2
for r being Element of REAL
for x being Element of the_set_of_RealSequences holds mult1 . r,x = mult2 . r,x

proof

let r be Element of REAL ; :: thesis: for x being Element of the_set_of_RealSequences holds mult1 . r,x = mult2 . r,x
let x be Element of the_set_of_RealSequences ; :: thesis: mult1 . r,x = mult2 . r,x
thus mult1 . r,x = (R_id r) (#) (seq_id x) by A1
.= mult2 . r,x by A2 ; :: thesis: verum

end;

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