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 FINSEQ_1:def 18;
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 Th48;
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, MCART_1:7; :: thesis: verum