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