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

proof

let z be Element of COMPLEX ; :: thesis: for x being Element of the_set_of_ComplexSequences holds mult1 . (z,x) = mult2 . (z,x)
let x be Element of the_set_of_ComplexSequences ; :: thesis: mult1 . (z,x) = mult2 . (z,x)
thus mult1 . (z,x) = (C_id z) (#) (seq_id x) by A1
.= mult2 . (z,x) by A2 ; :: thesis: verum

end;

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