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 :: thesis: S is gate`2isBoolean

proof

let g be set ; :: according to CIRCCOMB:def 8 :: thesis: ( not g in the carrier' of S or g = [(the Arity of S . g),(g `2 )] )
thus ( not g in the carrier' of S or g = [(the Arity of S . g),(g `2 )] ) by A1; :: thesis: verum

end;

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