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

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

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

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 )
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;x = 0 by TARSKI:def 1;

hence x = y by TARSKI:def 1; :: thesis: verum

proof

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 )
take
1. A
; :: according to GROUP_1:def 1 :: thesis: for b_{1} being Element of the carrier of A holds

( b_{1} * (1. A) = b_{1} & (1. A) * b_{1} = b_{1} )

thus for b_{1} being Element of the carrier of A holds

( b_{1} * (1. A) = b_{1} & (1. A) * b_{1} = b_{1} )
by A1; :: thesis: verum

end;( b

thus for b

( b

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