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 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
thus the Mult of R . r,v = [**r,0 **] * v by A1; :: thesis: verum