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;
consider f being Function of [:COMPLEX,the_set_of_ComplexSequences:],the_set_of_ComplexSequences such that
A2: 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);
take f ; :: thesis: for z, x being set st z is Complex & x in the_set_of_ComplexSequences holds
f . (z,x) = (C_id z) (#) (seq_id x)
let r, x be set ; :: thesis: ( r is Complex & x in the_set_of_ComplexSequences implies f . (r,x) = (C_id r) (#) (seq_id x) )
assume r is Complex ; :: thesis: ( not x in the_set_of_ComplexSequences or f . (r,x) = (C_id r) (#) (seq_id x) )
then r in COMPLEX by XCMPLX_0:def 2;
hence ( not x in the_set_of_ComplexSequences or f . (r,x) = (C_id r) (#) (seq_id x) ) by A2; :: thesis: verum