let A be Algebra; :: thesis: for A1, A2 being Subalgebra of A st the carrier of A1 c= the carrier of A2 holds
A1 is Subalgebra of A2
let A1, A2 be Subalgebra of A; :: thesis: ( the carrier of A1 c= the carrier of A2 implies A1 is Subalgebra of A2 )
assume L1: the carrier of A1 c= the carrier of A2 ; :: thesis: A1 is Subalgebra of A2
set CA1 = the carrier of A1;
set CA2 = the carrier of A2;
set AA = the addF of A;
set mA = the multF of A;
set MA = the Mult of A;
L2: ( 0. A1 = 0. A & 0. A2 = 0. A & 1. A1 = 1. A & 1. A2 = 1. A ) by C0SP1:def 9;
L3: the addF of A1 = the addF of A2 || the carrier of A1

proof

( the addF of A1 = the addF of A || the carrier of A1 & the addF of A2 = the addF of A || the carrier of A2 & [:the carrier of A1,the carrier of A1:] c= [:the carrier of A2,the carrier of A2:] ) by L1, C0SP1:def 9, ZFMISC_1:119;
hence the addF of A1 = the addF of A2 || the carrier of A1 by FUNCT_1:82; :: thesis: verum

end;

L4: the multF of A1 = the multF of A2 || the carrier of A1

proof

( the multF of A1 = the multF of A || the carrier of A1 & the multF of A2 = the multF of A || the carrier of A2 & [:the carrier of A1,the carrier of A1:] c= [:the carrier of A2,the carrier of A2:] ) by L1, C0SP1:def 9, ZFMISC_1:119;
hence the multF of A1 = the multF of A2 || the carrier of A1 by FUNCT_1:82; :: thesis: verum

end;

the Mult of A1 = the Mult of A2 | [:REAL ,the carrier of A1:]

proof

( the Mult of A1 = the Mult of A | [:REAL ,the carrier of A1:] & the Mult of A2 = the Mult of A | [:REAL ,the carrier of A2:] & [:REAL ,the carrier of A1:] c= [:REAL ,the carrier of A2:] ) by L1, C0SP1:def 9, ZFMISC_1:119;
hence the Mult of A1 = the Mult of A2 | [:REAL ,the carrier of A1:] by FUNCT_1:82; :: thesis: verum

end;

hence A1 is Subalgebra of A2 by L1, L2, L3, L4, C0SP1:def 9; :: thesis: verum