let n be Nat; :: thesis: ex f being Function of [:REAL,(REAL n):],(REAL n) st
for r being Element of REAL
for x being Element of REAL n holds f . (r,x) = r * x
deffunc H₁( real number , Element of REAL n) -> Element of REAL n = $1 * $2;
ex f being Function of [:REAL,(REAL n):],(REAL n) st
for r being Element of REAL
for x being Element of REAL n holds f . (r,x) = H₁(r,x) from BINOP_1:sch 4();
hence ex f being Function of [:REAL,(REAL n):],(REAL n) st
for r being Element of REAL
for x being Element of REAL n holds f . (r,x) = r * x ; :: thesis: verum