deffunc H₁( Real, Element of REAL n) -> Element of REAL n = $1 * $2;
consider f being Function of [:REAL,(REAL n):],(REAL n) such that
A1: 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();
take f ; :: thesis: for r being Real
for x being Element of REAL n holds f . (r,x) = r * x
let r be Real; :: thesis: for x being Element of REAL n holds f . (r,x) = r * x
let x be Element of REAL n; :: thesis: f . (r,x) = r * x
reconsider r = r as Element of REAL by XREAL_0:def 1;
f . (r,x) = H₁(r,x) by A1;
hence f . (r,x) = r * x ; :: thesis: verum