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: MSAlg (id the carrier of U1) = 0 .--> (id the carrier of U1) by Def3;
reconsider g = (*--> 0 ) * (signature U1) as Function of (dom (signature U1)),({0 } * ) by MSUALG_1:7;
A2: ( the carrier of (MSSign U1) = {0 } & the carrier' of (MSSign U1) = dom (signature U1) & the Arity of (MSSign U1) = g & the ResultSort of (MSSign U1) = (dom (signature U1)) --> 0 ) by MSUALG_1:def 13;
then reconsider Z1 = the Sorts of (MSAlg U1) as ManySortedSet of ;

A3: now

let i be set ; :: thesis: ( i in {0 } implies (id the Sorts of (MSAlg U1)) . 0 = id the carrier of U1 )
assume A4: i in {0 } ; :: thesis: (id the Sorts of (MSAlg U1)) . 0 = id the carrier of U1
then A5: i = 0 by TARSKI:def 1;
MSAlg U1 = MSAlgebra(# (MSSorts U1),(MSCharact U1) #) by MSUALG_1:def 16;
then Z1 . 0 = (0 .--> the carrier of U1) . 0 by MSUALG_1:def 14
.= the carrier of U1 by FUNCOP_1:87 ;
hence (id the Sorts of (MSAlg U1)) . 0 = id the carrier of U1 by A2, A4, A5, MSUALG_3:def 1; :: thesis: verum

end;

A6: (MSAlg (id the carrier of U1)) . 0 = id the carrier of U1 by A1, FUNCOP_1:87;

now

let a be set ; :: thesis: ( a in {0 } implies (id the Sorts of (MSAlg U1)) . a = (MSAlg (id the carrier of U1)) . a )
assume A7: 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 A3, A6, A7; :: thesis: verum

end;

hence id the Sorts of (MSAlg U1) = MSAlg (id the carrier of U1) by A2, PBOOLE:3; :: thesis: verum