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