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

let r be 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