let L be non empty multMagma ; :: thesis: for B being non empty AlgebraStr over L

for A being Subset of B st A is opers_closed holds

ex C being strict Subalgebra of B st the carrier of C = A

let B be non empty AlgebraStr over L; :: thesis: for A being Subset of B st A is opers_closed holds

ex C being strict Subalgebra of B st the carrier of C = A

let A be Subset of B; :: thesis: ( A is opers_closed implies ex C being strict Subalgebra of B st the carrier of C = A )

assume A1: A is opers_closed ; :: thesis: ex C being strict Subalgebra of B st the carrier of C = A

reconsider z = 0. B as Element of A by A1;

reconsider f4 = the lmult of B | [: the carrier of L,A:] as Function ;

A2: for x being object st x in [: the carrier of L,A:] holds

f4 . x in A

then [: the carrier of L,A:] c= dom the lmult of B by Th2;

then dom f4 = [: the carrier of L,A:] by RELAT_1:62;

then reconsider lm = f4 as Function of [: the carrier of L,A:],A by A2, FUNCT_2:3;

reconsider f1 = the addF of B || A as Function ;

reconsider f2 = the multF of B || A as Function ;

A8: for x being object st x in [:A,A:] holds

f2 . x in A

then [:A,A:] c= dom the multF of B by Th1;

then dom f2 = [:A,A:] by RELAT_1:62;

then reconsider mu = f2 as BinOp of A by A8, FUNCT_2:3;

( dom f1 = [:A,A:] & ( for x being object st x in [:A,A:] holds

f1 . x in A ) )

reconsider u = 1. B as Element of A by A1;

set c = AlgebraStr(# A,ad,mu,z,u,lm #);

( 1. AlgebraStr(# A,ad,mu,z,u,lm #) = 1. B & 0. AlgebraStr(# A,ad,mu,z,u,lm #) = 0. B ) ;

then reconsider C = AlgebraStr(# A,ad,mu,z,u,lm #) as strict Subalgebra of B by Def3;

take C ; :: thesis: the carrier of C = A

thus the carrier of C = A ; :: thesis: verum

for A being Subset of B st A is opers_closed holds

ex C being strict Subalgebra of B st the carrier of C = A

let B be non empty AlgebraStr over L; :: thesis: for A being Subset of B st A is opers_closed holds

ex C being strict Subalgebra of B st the carrier of C = A

let A be Subset of B; :: thesis: ( A is opers_closed implies ex C being strict Subalgebra of B st the carrier of C = A )

assume A1: A is opers_closed ; :: thesis: ex C being strict Subalgebra of B st the carrier of C = A

reconsider z = 0. B as Element of A by A1;

reconsider f4 = the lmult of B | [: the carrier of L,A:] as Function ;

A2: for x being object st x in [: the carrier of L,A:] holds

f4 . x in A

proof

[: the carrier of L,A:] c= [: the carrier of L, the carrier of B:]
by ZFMISC_1:96;
A3:
A is linearly-closed
by A1;

let x be object ; :: thesis: ( x in [: the carrier of L,A:] implies f4 . x in A )

assume A4: x in [: the carrier of L,A:] ; :: thesis: f4 . x in A

consider y, z being object such that

A5: y in the carrier of L and

A6: z in A and

A7: x = [y,z] by A4, ZFMISC_1:def 2;

reconsider z = z as Element of B by A6;

reconsider y = y as Element of L by A5;

f4 . x = y * z by A4, A7, FUNCT_1:49;

hence f4 . x in A by A6, A3, VECTSP_4:def 1; :: thesis: verum

end;let x be object ; :: thesis: ( x in [: the carrier of L,A:] implies f4 . x in A )

assume A4: x in [: the carrier of L,A:] ; :: thesis: f4 . x in A

consider y, z being object such that

A5: y in the carrier of L and

A6: z in A and

A7: x = [y,z] by A4, ZFMISC_1:def 2;

reconsider z = z as Element of B by A6;

reconsider y = y as Element of L by A5;

f4 . x = y * z by A4, A7, FUNCT_1:49;

hence f4 . x in A by A6, A3, VECTSP_4:def 1; :: thesis: verum

then [: the carrier of L,A:] c= dom the lmult of B by Th2;

then dom f4 = [: the carrier of L,A:] by RELAT_1:62;

then reconsider lm = f4 as Function of [: the carrier of L,A:],A by A2, FUNCT_2:3;

reconsider f1 = the addF of B || A as Function ;

reconsider f2 = the multF of B || A as Function ;

A8: for x being object st x in [:A,A:] holds

f2 . x in A

proof

A12:
[:A,A:] c= [: the carrier of B, the carrier of B:]
by ZFMISC_1:96;
let x be object ; :: thesis: ( x in [:A,A:] implies f2 . x in A )

assume A9: x in [:A,A:] ; :: thesis: f2 . x in A

consider y, z being object such that

A10: ( y in A & z in A ) and

A11: x = [y,z] by A9, ZFMISC_1:def 2;

reconsider y = y, z = z as Element of B by A10;

f2 . x = y * z by A9, A11, FUNCT_1:49;

hence f2 . x in A by A1, A10; :: thesis: verum

end;assume A9: x in [:A,A:] ; :: thesis: f2 . x in A

consider y, z being object such that

A10: ( y in A & z in A ) and

A11: x = [y,z] by A9, ZFMISC_1:def 2;

reconsider y = y, z = z as Element of B by A10;

f2 . x = y * z by A9, A11, FUNCT_1:49;

hence f2 . x in A by A1, A10; :: thesis: verum

then [:A,A:] c= dom the multF of B by Th1;

then dom f2 = [:A,A:] by RELAT_1:62;

then reconsider mu = f2 as BinOp of A by A8, FUNCT_2:3;

( dom f1 = [:A,A:] & ( for x being object st x in [:A,A:] holds

f1 . x in A ) )

proof

then reconsider ad = f1 as BinOp of A by FUNCT_2:3;
[:A,A:] c= dom the addF of B
by A12, Th1;

hence dom f1 = [:A,A:] by RELAT_1:62; :: thesis: for x being object st x in [:A,A:] holds

f1 . x in A

let x be object ; :: thesis: ( x in [:A,A:] implies f1 . x in A )

assume A13: x in [:A,A:] ; :: thesis: f1 . x in A

consider y, z being object such that

A14: ( y in A & z in A ) and

A15: x = [y,z] by A13, ZFMISC_1:def 2;

A16: A is linearly-closed by A1;

reconsider y = y, z = z as Element of B by A14;

f1 . x = y + z by A13, A15, FUNCT_1:49;

hence f1 . x in A by A14, A16, VECTSP_4:def 1; :: thesis: verum

end;hence dom f1 = [:A,A:] by RELAT_1:62; :: thesis: for x being object st x in [:A,A:] holds

f1 . x in A

let x be object ; :: thesis: ( x in [:A,A:] implies f1 . x in A )

assume A13: x in [:A,A:] ; :: thesis: f1 . x in A

consider y, z being object such that

A14: ( y in A & z in A ) and

A15: x = [y,z] by A13, ZFMISC_1:def 2;

A16: A is linearly-closed by A1;

reconsider y = y, z = z as Element of B by A14;

f1 . x = y + z by A13, A15, FUNCT_1:49;

hence f1 . x in A by A14, A16, VECTSP_4:def 1; :: thesis: verum

reconsider u = 1. B as Element of A by A1;

set c = AlgebraStr(# A,ad,mu,z,u,lm #);

( 1. AlgebraStr(# A,ad,mu,z,u,lm #) = 1. B & 0. AlgebraStr(# A,ad,mu,z,u,lm #) = 0. B ) ;

then reconsider C = AlgebraStr(# A,ad,mu,z,u,lm #) as strict Subalgebra of B by Def3;

take C ; :: thesis: the carrier of C = A

thus the carrier of C = A ; :: thesis: verum