let L be 1-sorted ; :: thesis: for A, B being AlgebraStr of L st AlgebraStr(# the carrier of A,the addF of A,the multF of A,the ZeroF of A,the OneF of A,the lmult of A #) = AlgebraStr(# the carrier of B,the addF of B,the multF of B,the ZeroF of B,the OneF of B,the lmult of B #) holds
A is Subalgebra of B
let A, B be AlgebraStr of L; :: thesis: ( AlgebraStr(# the carrier of A,the addF of A,the multF of A,the ZeroF of A,the OneF of A,the lmult of A #) = AlgebraStr(# the carrier of B,the addF of B,the multF of B,the ZeroF of B,the OneF of B,the lmult of B #) implies A is Subalgebra of B )
assume A1: AlgebraStr(# the carrier of A,the addF of A,the multF of A,the ZeroF of A,the OneF of A,the lmult of A #) = AlgebraStr(# the carrier of B,the addF of B,the multF of B,the ZeroF of B,the OneF of B,the lmult of B #) ; :: thesis: A is Subalgebra of B
thus the carrier of A c= the carrier of B by A1; :: according to POLYALG1:def 3 :: thesis: ( 1. A = 1. B & 0. A = 0. B & the addF of A = the addF of B || the carrier of A & the multF of A = the multF of B || the carrier of A & the lmult of A = the lmult of B | [:the carrier of L,the carrier of A:] )
thus 1. A = 1. B by A1; :: thesis: ( 0. A = 0. B & the addF of A = the addF of B || the carrier of A & the multF of A = the multF of B || the carrier of A & the lmult of A = the lmult of B | [:the carrier of L,the carrier of A:] )
thus 0. A = 0. B by A1; :: thesis: ( the addF of A = the addF of B || the carrier of A & the multF of A = the multF of B || the carrier of A & the lmult of A = the lmult of B | [:the carrier of L,the carrier of A:] )
dom the addF of B = [:the carrier of B,the carrier of B:] by Th1;
hence the addF of A = the addF of B || the carrier of A by A1, RELAT_1:97; :: thesis: ( the multF of A = the multF of B || the carrier of A & the lmult of A = the lmult of B | [:the carrier of L,the carrier of A:] )
dom the multF of B = [:the carrier of B,the carrier of B:] by Th1;
hence the multF of A = the multF of B || the carrier of A by A1, RELAT_1:97; :: thesis: the lmult of A = the lmult of B | [:the carrier of L,the carrier of A:]
dom the lmult of B = [:the carrier of L,the carrier of B:] by Th2;
hence the lmult of A = the lmult of B | [:the carrier of L,the carrier of A:] by A1, RELAT_1:97; :: thesis: verum