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 over L ;
take A ; :: thesis: ( A is unital & A is distributive & A is vector-distributive & A is scalar-distributive & A is scalar-associative & A is scalar-unital & 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 by TARSKI:def 1;
hence x = y by TARSKI:def 1; :: thesis: verum
end;
thus A is unital :: thesis: ( A is distributive & A is vector-distributive & A is scalar-distributive & A is scalar-associative & A is scalar-unital & A is mix-associative )
proof
take 1. A ; :: according to GROUP_1:def 1 :: thesis: for b1 being Element of the carrier of A holds
( b1 * (1. A) = b1 & (1. A) * b1 = b1 )
thus for b1 being Element of the carrier of A holds
( b1 * (1. A) = b1 & (1. A) * b1 = b1 ) by A1; :: thesis: verum
end;
thus A is distributive by A1; :: thesis: ( A is vector-distributive & A is scalar-distributive & A is scalar-associative & A is scalar-unital & A is mix-associative )
thus A is vector-distributive by A1; :: thesis: ( A is scalar-distributive & A is scalar-associative & A is scalar-unital & A is mix-associative )
thus A is scalar-distributive by A1; :: thesis: ( A is scalar-associative & A is scalar-unital & A is mix-associative )
thus A is scalar-associative by A1; :: thesis: ( A is scalar-unital & A is mix-associative )
thus A is scalar-unital by A1; :: thesis: A is mix-associative
thus A is mix-associative by A1; :: thesis: verum