let S be non empty ManySortedSign ; :: thesis: for A being MSAlgebra of S holds
( A is Boolean iff the Sorts of A = the carrier of S --> BOOLEAN )
let A be MSAlgebra of S; :: thesis: ( A is Boolean iff the Sorts of A = the carrier of S --> BOOLEAN )
A1: dom the Sorts of A = the carrier of S by PARTFUN1:def 4;
thus ( A is Boolean implies the Sorts of A = the carrier of S --> BOOLEAN ) :: thesis: ( the Sorts of A = the carrier of S --> BOOLEAN implies A is Boolean )

proof

assume for v being Vertex of S holds the Sorts of A . v = BOOLEAN ; :: according to CIRCCOMB:def 15 :: thesis: the Sorts of A = the carrier of S --> BOOLEAN
then for v being set st v in the carrier of S holds
the Sorts of A . v = BOOLEAN ;
hence the Sorts of A = the carrier of S --> BOOLEAN by A1, FUNCOP_1:17; :: thesis: verum

end;

assume A2: the Sorts of A = the carrier of S --> BOOLEAN ; :: thesis: A is Boolean
let v be Vertex of S; :: according to CIRCCOMB:def 15 :: thesis: the Sorts of A . v = BOOLEAN
thus the Sorts of A . v = BOOLEAN by A2, FUNCOP_1:13; :: thesis: verum