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