let n be Nat; :: thesis: for X being non empty set
for f being Function of (n -tuples_on X),X
for p being FinSeqLen of n holds
( 1GateCircuit (p,f) is gate`2=den & 1GateCircStr (p,f) is gate`2=den )
let X be non empty set ; :: thesis: for f being Function of (n -tuples_on X),X
for p being FinSeqLen of n holds
( 1GateCircuit (p,f) is gate`2=den & 1GateCircStr (p,f) is gate`2=den )
let f be Function of (n -tuples_on X),X; :: thesis: for p being FinSeqLen of n holds
( 1GateCircuit (p,f) is gate`2=den & 1GateCircStr (p,f) is gate`2=den )
let p be FinSeqLen of n; :: thesis: ( 1GateCircuit (p,f) is gate`2=den & 1GateCircStr (p,f) is gate`2=den )
thus A1: 1GateCircuit (p,f) is gate`2=den :: thesis: 1GateCircStr (p,f) is gate`2=den

proof

let g be set ; :: according to CIRCCOMB:def 10 :: thesis: ( g in the carrier' of (1GateCircStr (p,f)) implies g = [(g `1),( the Charact of (1GateCircuit (p,f)) . g)] )
assume g in the carrier' of (1GateCircStr (p,f)) ; :: thesis: g = [(g `1),( the Charact of (1GateCircuit (p,f)) . g)]
then A2: g = [p,f] by Th41;
hence g = [(g `1),f]
.= [(g `1),( the Charact of (1GateCircuit (p,f)) . g)] by A2, Def13 ;
:: thesis: verum

end;

take 1GateCircuit (p,f) ; :: according to CIRCCOMB:def 11 :: thesis: 1GateCircuit (p,f) is gate`2=den
thus 1GateCircuit (p,f) is gate`2=den by A1; :: thesis: verum