let U1 be Universal_Algebra; :: thesis: MSAlg (id the carrier of U1) = id the Sorts of (MSAlg U1)
set f = id the Sorts of (MSAlg U1);
set h = id the carrier of U1;
A1: the carrier of (MSSign U1) = {0} by MSUALG_1:def 8;
then reconsider Z1 = the Sorts of (MSAlg U1) as ManySortedSet of {0} ;
A2: now :: thesis: for i being set st i in {0} holds
(id the Sorts of (MSAlg U1)) . 0 = id the carrier of U1
let i be set ; :: thesis: ( i in {0} implies (id the Sorts of (MSAlg U1)) . 0 = id the carrier of U1 )
MSAlg U1 = MSAlgebra(# (MSSorts U1),(MSCharact U1) #) by MSUALG_1:def 11;
then A3: Z1 . 0 = (0 .--> the carrier of U1) . 0 by MSUALG_1:def 9
.= the carrier of U1 by FUNCOP_1:72 ;
assume A4: i in {0} ; :: thesis: (id the Sorts of (MSAlg U1)) . 0 = id the carrier of U1
then i = 0 by TARSKI:def 1;
hence (id the Sorts of (MSAlg U1)) . 0 = id the carrier of U1 by A1, A4, A3, MSUALG_3:def 1; :: thesis: verum
end;
MSAlg (id the carrier of U1) = 0 .--> (id the carrier of U1) by Def3;
then A5: (MSAlg (id the carrier of U1)) . 0 = id the carrier of U1 by FUNCOP_1:72;
now :: thesis: for a being object st a in {0} holds
(id the Sorts of (MSAlg U1)) . a = (MSAlg (id the carrier of U1)) . a
let a be object ; :: thesis: ( a in {0} implies (id the Sorts of (MSAlg U1)) . a = (MSAlg (id the carrier of U1)) . a )
assume A6: a in {0} ; :: thesis: (id the Sorts of (MSAlg U1)) . a = (MSAlg (id the carrier of U1)) . a
then a = 0 by TARSKI:def 1;
hence (id the Sorts of (MSAlg U1)) . a = (MSAlg (id the carrier of U1)) . a by A2, A5, A6; :: thesis: verum
end;
hence id the Sorts of (MSAlg U1) = MSAlg (id the carrier of U1) by A1, PBOOLE:3; :: thesis: verum