0 in {0} by TARSKI:def 1;
then reconsider lm = [: the carrier of L,{0}:] --> 0 as Function of [: the carrier of L,{0}:],{0} by FUNCOP_1:45;
reconsider z = 0 as Element of {0} by TARSKI:def 1;
set a = the BinOp of {0};
reconsider A = AlgebraStr(# {0}, the BinOp of {0}, the BinOp of {0},z,z,lm #) as non empty AlgebraStr of L ;
take A ; :: thesis:
A1: for x, y being Element of A holds x = y

proof

let x, y be Element of A; :: thesis:
x = 0 by TARSKI:def 1;
hence x = y by TARSKI:def 1; :: thesis:

end;

thus A is unital :: thesis:

proof

take 1. A ; :: according to GROUP_1:def 1 :: thesis:
thus for b₁ being Element of the carrier of A holds
( b₁ * (1. A) = b₁ & (1. A) * b₁ = b₁ ) by A1; :: thesis:

end;

thus A is distributive :: thesis:

proof

let x, y, z be Element of A; :: according to VECTSP_1:def 7 :: thesis:
thus ( x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) ) by A1; :: thesis:

end;

thus A is vector-distributive :: thesis:

proof

let x be Element of L; :: according to VECTSP_1:def 14 :: thesis:
let v, w be Element of A; :: thesis:
thus x * (v + w) = (x * v) + (x * w) by A1; :: thesis:

end;

thus A is scalar-distributive :: thesis:

proof

let x, y be Element of L; :: according to VECTSP_1:def 15 :: thesis:
let v be Element of A; :: thesis:
thus (x + y) * v = (x * v) + (y * v) by A1; :: thesis:

end;

thus A is scalar-associative :: thesis:

proof

let x, y be Element of L; :: according to VECTSP_1:def 16 :: thesis:
thus for b₁ being Element of the carrier of A holds (x * y) * b₁ = x * (y * b₁) by A1; :: thesis:

end;

thus A is scalar-unital :: thesis:

proof

let v be Element of A; :: according to VECTSP_1:def 17 :: thesis:
thus (1. L) * v = v by A1; :: thesis:

end;

thus A is mix-associative :: thesis:

proof

let a be Element of L; :: according to POLYALG1:def 1 :: thesis:
let x, y be Element of A; :: thesis:
thus a * (x * y) = (a * x) * y by A1; :: thesis:

end;