set X = BOOLEAN ;
let n be Nat; :: thesis: 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; :: thesis: 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; :: thesis: 1GateCircStr (p,f) is gate`2isBoolean
let g be set ; :: according to CIRCCOMB:def 9 :: thesis: ( 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)) ; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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 ; :: thesis: g = [(g `1),f]
thus g = [(g `1),f] by A3; :: thesis: verum