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 A1: 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;
A2: ( 0. A1 = 0. A & 0. A2 = 0. A & 1. A1 = 1. A & 1. A2 = 1. A ) by C0SP1:def 9;
A3: 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 A1, C0SP1:def 9, ZFMISC_1:96;
hence the addF of A1 = the addF of A2 || the carrier of A1 by FUNCT_1:51; :: thesis: verum

end;

A4: 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 A1, C0SP1:def 9, ZFMISC_1:96;
hence the multF of A1 = the multF of A2 || the carrier of A1 by FUNCT_1:51; :: 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 A1, C0SP1:def 9, ZFMISC_1:96;
hence the Mult of A1 = the Mult of A2 | [:REAL, the carrier of A1:] by FUNCT_1:51; :: thesis: verum

end;

hence A1 is Subalgebra of A2 by A1, A2, A3, A4, C0SP1:def 9; :: thesis: verum