deffunc H₁( set , set ) -> M5( 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