let L be 1-sorted ; for A, B being AlgebraStr over 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 over L; ( 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 #)
; A is Subalgebra of B
thus
the carrier of A c= the carrier of B
by A1; POLYALG1:def 3 ( 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; ( 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; ( 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
the addF of A = the addF of B || the carrier of A
by A1; ( 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
the multF of A = the multF of B || the carrier of A
by A1; the lmult of A = the lmult of B | [: the carrier of L, the carrier of A:]
thus
the lmult of A = the lmult of B | [: the carrier of L, the carrier of A:]
by A1; verum