let X be non empty set ; for d1, d2 being Element of X
for A being BinOp of X
for M being Function of [:X,X:],X
for V being Algebra
for V1 being Subset of V
for MR being Function of [:REAL,X:],X st V1 = X & d1 = 0. V & d2 = 1. V & A = the addF of V || V1 & M = the multF of V || V1 & MR = the Mult of V | [:REAL,V1:] & V1 is having-inverse holds
AlgebraStr(# X,M,A,MR,d2,d1 #) is Subalgebra of V
let d1, d2 be Element of X; for A being BinOp of X
for M being Function of [:X,X:],X
for V being Algebra
for V1 being Subset of V
for MR being Function of [:REAL,X:],X st V1 = X & d1 = 0. V & d2 = 1. V & A = the addF of V || V1 & M = the multF of V || V1 & MR = the Mult of V | [:REAL,V1:] & V1 is having-inverse holds
AlgebraStr(# X,M,A,MR,d2,d1 #) is Subalgebra of V
let A be BinOp of X; for M being Function of [:X,X:],X
for V being Algebra
for V1 being Subset of V
for MR being Function of [:REAL,X:],X st V1 = X & d1 = 0. V & d2 = 1. V & A = the addF of V || V1 & M = the multF of V || V1 & MR = the Mult of V | [:REAL,V1:] & V1 is having-inverse holds
AlgebraStr(# X,M,A,MR,d2,d1 #) is Subalgebra of V
let M be Function of [:X,X:],X; for V being Algebra
for V1 being Subset of V
for MR being Function of [:REAL,X:],X st V1 = X & d1 = 0. V & d2 = 1. V & A = the addF of V || V1 & M = the multF of V || V1 & MR = the Mult of V | [:REAL,V1:] & V1 is having-inverse holds
AlgebraStr(# X,M,A,MR,d2,d1 #) is Subalgebra of V
let V be Algebra; for V1 being Subset of V
for MR being Function of [:REAL,X:],X st V1 = X & d1 = 0. V & d2 = 1. V & A = the addF of V || V1 & M = the multF of V || V1 & MR = the Mult of V | [:REAL,V1:] & V1 is having-inverse holds
AlgebraStr(# X,M,A,MR,d2,d1 #) is Subalgebra of V
let V1 be Subset of V; for MR being Function of [:REAL,X:],X st V1 = X & d1 = 0. V & d2 = 1. V & A = the addF of V || V1 & M = the multF of V || V1 & MR = the Mult of V | [:REAL,V1:] & V1 is having-inverse holds
AlgebraStr(# X,M,A,MR,d2,d1 #) is Subalgebra of V
let MR be Function of [:REAL,X:],X; ( V1 = X & d1 = 0. V & d2 = 1. V & A = the addF of V || V1 & M = the multF of V || V1 & MR = the Mult of V | [:REAL,V1:] & V1 is having-inverse implies AlgebraStr(# X,M,A,MR,d2,d1 #) is Subalgebra of V )
assume that
A1:
V1 = X
and
A2:
d1 = 0. V
and
A3:
d2 = 1. V
and
A4:
A = the addF of V || V1
and
A5:
M = the multF of V || V1
and
A6:
MR = the Mult of V | [:REAL,V1:]
and
A7:
for v being Element of V st v in V1 holds
- v in V1
; C0SP1:def 1 AlgebraStr(# X,M,A,MR,d2,d1 #) is Subalgebra of V
reconsider W = AlgebraStr(# X,M,A,MR,d2,d1 #) as non empty AlgebraStr ;
A11:
( W is Abelian & W is add-associative & W is right_zeroed & W is right_complementable & W is commutative & W is associative & W is right_unital & W is right-distributive & W is vector-distributive & W is scalar-distributive & W is scalar-associative & W is vector-associative )
( 0. W = 0. V & 1. W = 1. V )
by A2, A3;
hence
AlgebraStr(# X,M,A,MR,d2,d1 #) is Subalgebra of V
by A1, A4, A5, A6, A11, Def9; verum