set X = BOOLEAN ;
let n be Nat; for p being FinSeqLen of n
for f being Function of (n -tuples_on BOOLEAN),BOOLEAN holds 1GateCircStr (p,f) is gate`2isBoolean
let p be FinSeqLen of n; for f being Function of (n -tuples_on BOOLEAN),BOOLEAN holds 1GateCircStr (p,f) is gate`2isBoolean
let f be Function of (n -tuples_on BOOLEAN),BOOLEAN; 1GateCircStr (p,f) is gate`2isBoolean
let g be set ; CIRCCOMB:def 9 ( g in the carrier' of (1GateCircStr (p,f)) implies for p being FinSequence st p = the Arity of (1GateCircStr (p,f)) . g holds
ex f being Function of ((len p) -tuples_on BOOLEAN),BOOLEAN st g = [(g `1),f] )
A1:
len p = n
by CARD_1:def 7;
A2:
the Arity of (1GateCircStr (p,f)) . [p,f] = p
by Def6;
assume
g in the carrier' of (1GateCircStr (p,f))
; for p being FinSequence st p = the Arity of (1GateCircStr (p,f)) . g holds
ex f being Function of ((len p) -tuples_on BOOLEAN),BOOLEAN st g = [(g `1),f]
then A3:
g = [p,f]
by Th41;
let q be FinSequence; ( q = the Arity of (1GateCircStr (p,f)) . g implies ex f being Function of ((len q) -tuples_on BOOLEAN),BOOLEAN st g = [(g `1),f] )
assume
q = the Arity of (1GateCircStr (p,f)) . g
; ex f being Function of ((len q) -tuples_on BOOLEAN),BOOLEAN st g = [(g `1),f]
then reconsider f = f as Function of ((len q) -tuples_on BOOLEAN),BOOLEAN by A3, A2, A1;
take
f
; g = [(g `1),f]
thus
g = [(g `1),f]
by A3; verum