let S be one-gate ManySortedSign ; :: thesis: for A being one-gate Circuit of S
for n being Element of NAT
for X being non empty finite set
for f being Function of (n -tuples_on X),X
for p being FinSeqLen of n st A = 1GateCircuit p,f holds
S = 1GateCircStr p,f
let A be one-gate Circuit of S; :: thesis: for n being Element of NAT
for X being non empty finite set
for f being Function of (n -tuples_on X),X
for p being FinSeqLen of n st A = 1GateCircuit p,f holds
S = 1GateCircStr p,f
let n be Element of NAT ; :: thesis: for X being non empty finite set
for f being Function of (n -tuples_on X),X
for p being FinSeqLen of n st A = 1GateCircuit p,f holds
S = 1GateCircStr p,f
let X be non empty finite set ; :: thesis: for f being Function of (n -tuples_on X),X
for p being FinSeqLen of n st A = 1GateCircuit p,f holds
S = 1GateCircStr p,f
let f be Function of (n -tuples_on X),X; :: thesis: for p being FinSeqLen of n st A = 1GateCircuit p,f holds
S = 1GateCircStr p,f
let p be FinSeqLen of n; :: thesis: ( A = 1GateCircuit p,f implies S = 1GateCircStr p,f )
assume A1: A = 1GateCircuit p,f ; :: thesis: S = 1GateCircStr p,f
consider X1 being non empty finite set , n1 being Element of NAT , p1 being FinSeqLen of n1, f1 being Function of (n1 -tuples_on X1),X1 such that
A2: S = 1GateCircStr p1,f1 and
A3: A = 1GateCircuit p1,f1 by Def7;
{[p,f]} = the carrier' of (1GateCircStr p,f) by CIRCCOMB:def 6
.= dom the Charact of (1GateCircuit p1,f1) by A1, A3, PARTFUN1:def 4
.= the carrier' of (1GateCircStr p1,f1) by PARTFUN1:def 4
.= {[p1,f1]} by CIRCCOMB:def 6 ;
then A4: [p,f] = [p1,f1] by ZFMISC_1:6;
then p = p1 by ZFMISC_1:33;
hence S = 1GateCircStr p,f by A2, A4, ZFMISC_1:33; :: thesis: verum