let S be ManySortedSign ; :: thesis: ( S is void implies ( S is unsplit & S is gate`1=arity & S is gate`2isBoolean ) )
assume A1: the carrier' of S is empty ; :: according to STRUCT_0:def 13 :: thesis: ( S is unsplit & S is gate`1=arity & S is gate`2isBoolean )
hence the ResultSort of S = {}
.= id the carrier' of S by A1 ;
:: according to CIRCCOMB:def 7 :: thesis: ( S is gate`1=arity & S is gate`2isBoolean )
thus S is gate`1=arity by A1; :: thesis: S is gate`2isBoolean
let g be set ; :: according to CIRCCOMB:def 9 :: thesis: ( not g in the carrier' of S or for b₁ being set holds
( not b₁ = the Arity of S . g or ex b₂ being Element of K23(K24(((len b₁) -tuples_on BOOLEAN),BOOLEAN)) st g = [(g `1),b<sub>2</sub>] ) )
thus ( not g in the carrier' of S or for b<sub>1</sub> being set holds
( not b<sub>1</sub> = the Arity of S . g or ex b<sub>2</sub> being Element of K23(K24(((len b<sub>1</sub>) -tuples_on BOOLEAN),BOOLEAN)) st g = [(g `1),b₂] ) ) by A1; :: thesis: verum