consider a being BinOp of {0 };
reconsider z = 0 as Element of {0 } by TARSKI:def 1;
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:57;
reconsider A = AlgebraStr(# {0 },a,a,z,z,lm #) as non empty AlgebraStr of L ;
take A ; :: thesis: ( A is unital & A is distributive & A is VectSp-like & A is mix-associative )
A1: for x, y being Element of A holds x = y

proof

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

end;

thus A is unital :: thesis: ( A is distributive & A is VectSp-like & A is mix-associative )

proof

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

end;

thus A is distributive :: thesis: ( A is VectSp-like & A is mix-associative )

proof

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

end;

thus A is VectSp-like :: thesis: A is mix-associative

proof

let x, y be Element of L; :: according to VECTSP_1:def 26 :: thesis: for b₁, b₂ being Element of the carrier of A holds
( x * (b₁ + b₂) = (x * b₁) + (x * b₂) & (x + y) * b₁ = (x * b₁) + (y * b₁) & (x * y) * b₁ = x * (y * b₁) & (1. L) * b₁ = b₁ )
let v, w be Element of A; :: thesis: ( x * (v + w) = (x * v) + (x * w) & (x + y) * v = (x * v) + (y * v) & (x * y) * v = x * (y * v) & (1. L) * v = v )
thus ( x * (v + w) = (x * v) + (x * w) & (x + y) * v = (x * v) + (y * v) & (x * y) * v = x * (y * v) & (1. L) * v = v ) by A1; :: thesis: verum

end;

thus A is mix-associative :: thesis: verum

proof

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

end;