deffunc H₁( object , object ) -> object = c₁ `2 ;
let S be non empty ManySortedSign ; :: thesis: ( S is gate`2isBoolean implies S is gate`2=den )
assume A1: for g being set st g in the carrier' of S holds
for p being FinSequence st p = the Arity of S . g holds
ex f being Function of ((len p) -tuples_on BOOLEAN),BOOLEAN st g = [(g `1),f] ; :: according to CIRCCOMB:def 9 :: thesis: S is gate`2=den

A2: now :: thesis: for g being set
for p being Element of the carrier of S * st g in the carrier' of S & p = the Arity of S . g holds
H₁(g,p) is Function of ((len p) -tuples_on BOOLEAN),BOOLEAN

let g be set ; :: thesis: for p being Element of the carrier of S * st g in the carrier' of S & p = the Arity of S . g holds
H₁(g,p) is Function of ((len p) -tuples_on BOOLEAN),BOOLEAN
let p be Element of the carrier of S * ; :: thesis: ( g in the carrier' of S & p = the Arity of S . g implies H₁(g,p) is Function of ((len p) -tuples_on BOOLEAN),BOOLEAN )
assume that
A3: g in the carrier' of S and
A4: p = the Arity of S . g ; :: thesis: H₁(g,p) is Function of ((len p) -tuples_on BOOLEAN),BOOLEAN
ex f being Function of ((len p) -tuples_on BOOLEAN),BOOLEAN st g = [(g `1),f] by A1, A3, A4;
hence H₁(g,p) is Function of ((len p) -tuples_on BOOLEAN),BOOLEAN ; :: thesis: verum

end;

consider A being strict MSAlgebra over S such that
A5: ( the Sorts of A = the carrier of S --> BOOLEAN & ( for g being set
for p being Element of the carrier of S * st g in the carrier' of S & p = the Arity of S . g holds
the Charact of A . g = H₁(g,p) ) ) from CIRCCOMB:sch 2(A2);
take A ; :: according to CIRCCOMB:def 11 :: thesis: A is gate`2=den
let g be set ; :: according to CIRCCOMB:def 10 :: thesis: ( g in the carrier' of S implies g = [(g `1),( the Charact of A . g)] )
assume A6: g in the carrier' of S ; :: thesis: g = [(g `1),( the Charact of A . g)]
then reconsider p = the Arity of S . g as Element of the carrier of S * by FUNCT_2:5;
consider f being Function of ((len p) -tuples_on BOOLEAN),BOOLEAN such that
A7: g = [(g `1),f] by A1, A6;
f = g `2 by A7;
hence g = [(g `1),( the Charact of A . g)] by A5, A6, A7; :: thesis: verum