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 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 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 holds
( 1GateCircuit p,f is gate`2=den & 1GateCircStr p,f is gate`2=den )
let p be FinSeqLen of ; :: 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 Th48;
hence g = [(g `1 ),f] by MCART_1:7
.= [(g `1 ),(the Charact of (1GateCircuit p,f) . g)] by A2, Def14 ;
:: 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