deffunc H₁( set , set ) -> Element of bool [:NAT ,COMPLEX :] = (C_id $1) (#) (seq_id $2);
A1: for r, x being set st r in COMPLEX & x in the_set_of_ComplexSequences holds
H₁(r,x) in the_set_of_ComplexSequences by Def1;
ex f being Function of [:COMPLEX ,the_set_of_ComplexSequences :],the_set_of_ComplexSequences st
for r, x being set st r in COMPLEX & x in the_set_of_ComplexSequences holds
f . r,x = H₁(r,x) from BINOP_1:sch 2(A1);
hence ex f being Function of [:COMPLEX ,the_set_of_ComplexSequences :],the_set_of_ComplexSequences st
for r, x being set st r in COMPLEX & x in the_set_of_ComplexSequences holds
f . r,x = (C_id r) (#) (seq_id x) ; :: thesis: verum