deffunc H₁( set , set ) -> object = S `2 ;

A1: 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
A2: g in the carrier' of S and
A3: 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 A2, A3, Def9;
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
A4: ( 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(A1);
take A ; :: thesis: ( A is Boolean & A is gate`2=den )
thus A is Boolean by A4; :: 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 A5: 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
A6: g = [(g `1),f] by A5, Def9;
g `2 = f by A6;
hence g = [(g `1),( the Charact of A . g)] by A4, A5, A6; :: thesis: verum