now :: thesis: for a, b, c being Element of doubleLoopStr(# the carrier of L, the addF of L, the multF of L, the OneF of L, the ZeroF of L #) holds a * (b + c) = (a * b) + (a * c)

let a, b, c be Element of doubleLoopStr(# the carrier of L, the addF of L, the multF of L, the OneF of L, the ZeroF of L #); :: thesis: a * (b + c) = (a * b) + (a * c)
reconsider x = a, y = b, z = c as Element of L ;
thus a * (b + c) = x * (y + z)
.= (x * y) + (x * z) by VECTSP_1:def 2
.= (a * b) + (a * c) ; :: thesis: verum

end;

hence doubleLoopStr(# the carrier of L, the addF of L, the multF of L, the OneF of L, the ZeroF of L #) is right-distributive ; :: thesis: verum