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
deffunc H1( set , set ) -> set = c1 `2 ;
A2:
now 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
H1(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 H1(g,p) is Function of (len p) -tuples_on BOOLEAN , BOOLEAN )assume
(
g in the
carrier' of
S &
p = the
Arity of
S . g )
;
:: thesis: H1(g,p) is Function of (len p) -tuples_on BOOLEAN , BOOLEAN then consider f being
Function of
(len p) -tuples_on BOOLEAN ,
BOOLEAN such that A3:
g = [(g `1 ),f]
by A1;
thus
H1(
g,
p) is
Function of
(len p) -tuples_on BOOLEAN ,
BOOLEAN
by A3, MCART_1:7;
:: thesis: verum end;
consider A being strict MSAlgebra of 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 = H1(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 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:7;
consider f being Function of (len p) -tuples_on BOOLEAN , BOOLEAN such that
A6:
g = [(g `1 ),f]
by A1, A5;
f = g `2
by A6, MCART_1:7;
hence
g = [(g `1 ),(the Charact of A . g)]
by A4, A5, A6; :: thesis: verum