let S be non empty ManySortedSign ; :: thesis: for A being MSAlgebra over S holds
( A is Boolean iff the Sorts of A = the carrier of S --> BOOLEAN )
let A be MSAlgebra over 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 2;
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 14 :: thesis: the Sorts of A = the carrier of S --> BOOLEAN
then for v being object 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:11; :: 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 14 :: thesis: the Sorts of A . v = BOOLEAN
thus the Sorts of A . v = BOOLEAN by A2; :: thesis: verum