let a, b be strict RLSStruct ; :: thesis: ( addLoopStr(# the carrier of a, the addF of a, the ZeroF of a #) = 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 a . (r,v) = [**r,0**] * v ) & addLoopStr(# the carrier of b, the addF of b, the ZeroF of b #) = 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 b . (r,v) = [**r,0**] * v ) implies a = b )
assume that
A2: addLoopStr(# the carrier of a, the addF of a, the ZeroF of a #) = addLoopStr(# the carrier of V, the addF of V, the ZeroF of V #) and
A3: for r being Real
for v being Vector of V holds the Mult of a . (r,v) = [**r,0**] * v and
A4: addLoopStr(# the carrier of b, the addF of b, the ZeroF of b #) = addLoopStr(# the carrier of V, the addF of V, the ZeroF of V #) and
A5: for r being Real
for v being Vector of V holds the Mult of b . (r,v) = [**r,0**] * v ; :: thesis: a = b

now :: thesis: for r being Element of REAL
for v being Vector of V holds the Mult of a . (r,v) = the Mult of b . (r,v)

let r be Element of REAL ; :: thesis: for v being Vector of V holds the Mult of a . (r,v) = the Mult of b . (r,v)
let v be Vector of V; :: thesis: the Mult of a . (r,v) = the Mult of b . (r,v)
thus the Mult of a . (r,v) = [**r,0**] * v by A3
.= the Mult of b . (r,v) by A5 ; :: thesis: verum

end;

hence a = b by A2, A4, BINOP_1:2; :: thesis: verum