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 (b + c) * a = (b * a) + (c * a)

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: (b + c) * a = (b * a) + (c * a)
reconsider x = a, y = b, z = c as Element of L ;
thus (b + c) * a = (y + z) * x
.= (y * x) + (z * x) by VECTSP_1:def 3
.= (b * a) + (c * a) ; :: 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 left-distributive ; :: thesis: verum