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

proof

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;

[: the carrier of L,A:] c= [: the carrier of L, the carrier of B:] by ZFMISC_1:96;
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

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;

A12: [:A,A:] c= [: the carrier of B, the carrier of B:] by ZFMISC_1:96;
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

[: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;

then reconsider ad = f1 as BinOp of A by FUNCT_2:3;
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