deffunc H₁( Element of REAL , Element of V) -> Element of the carrier of V = [**$1,0**] * $2;
consider f being Function of [:REAL, the carrier of V:], the carrier of V such that
A1: for r being Element of REAL
for v being Vector of V holds f . (r,v) = H₁(r,v) from BINOP_1:sch 4();
take R = RLSStruct(# the carrier of V,(0. V), the addF of V,f #); :: thesis: ( addLoopStr(# the carrier of R, the addF of R, the ZeroF of R #) = addLoopStr(# the carrier of V, the addF of V, the ZeroF of V #) & ( for r being Real
for v being Vector of V holds the Mult of R . (r,v) = [**r,0**] * v ) )
thus addLoopStr(# the carrier of R, the addF of R, the ZeroF of R #) = addLoopStr(# the carrier of V, the addF of V, the ZeroF of V #) ; :: thesis: for r being Real
for v being Vector of V holds the Mult of R . (r,v) = [**r,0**] * v
let r be Real; :: thesis: for v being Vector of V holds the Mult of R . (r,v) = [**r,0**] * v
let v be Vector of V; :: thesis: the Mult of R . (r,v) = [**r,0**] * v
reconsider r = r as Element of REAL by XREAL_0:def 1;
f . (r,v) = H₁(r,v) by A1;
hence the Mult of R . (r,v) = [**r,0**] * v ; :: thesis: verum