let S be non empty non void ManySortedSign ; :: thesis: for T being non-empty trivial MSAlgebra over S
for A being non-empty MSSubAlgebra of T holds MSAlgebra(# the Sorts of A, the Charact of A #) = MSAlgebra(# the Sorts of T, the Charact of T #)
let T be non-empty trivial MSAlgebra over S; :: thesis: for A being non-empty MSSubAlgebra of T holds MSAlgebra(# the Sorts of A, the Charact of A #) = MSAlgebra(# the Sorts of T, the Charact of T #)
let A be non-empty MSSubAlgebra of T; :: thesis: MSAlgebra(# the Sorts of A, the Charact of A #) = MSAlgebra(# the Sorts of T, the Charact of T #)
A1: the Sorts of A is ManySortedSubset of the Sorts of T by MSUALG_2:def 9;
A2: now :: thesis: for x being object st x in the carrier of S holds
the Sorts of A . x = the Sorts of T . x
let x be object ; :: thesis: ( x in the carrier of S implies the Sorts of A . x = the Sorts of T . x )
assume A3: x in the carrier of S ; :: thesis: the Sorts of A . x = the Sorts of T . x
then A4: ( the Sorts of A . x c= the Sorts of T . x & the Sorts of A . x <> {} & the Sorts of T . x <> {} ) by A1, PBOOLE:def 2, PBOOLE:def 18;
( not the Sorts of A . x is empty & the Sorts of A . x is trivial ) by A4;
then consider a being object such that
A5: the Sorts of A . x = {a} by ZFMISC_1:131;
consider b being object such that
A6: the Sorts of T . x = {b} by A3, ZFMISC_1:131;
thus the Sorts of A . x = the Sorts of T . x by A4, A5, A6, ZFMISC_1:3; :: thesis: verum
end;
MSAlgebra(# the Sorts of T, the Charact of T #) = MSAlgebra(# the Sorts of T, the Charact of T #) ;
then ( T is MSSubAlgebra of T & A is MSSubAlgebra of T ) by MSUALG_2:5;
hence MSAlgebra(# the Sorts of A, the Charact of A #) = MSAlgebra(# the Sorts of T, the Charact of T #) by A2, PBOOLE:3, MSUALG_2:9; :: thesis: verum