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 b₁ being Function of [:COMPLEX,the_set_of_ComplexSequences:],the_set_of_ComplexSequences st
for z, x being set st z in COMPLEX & x in the_set_of_ComplexSequences holds
b₁ . (z,x) = (C_id z) (#) (seq_id x) ; :: thesis: verum