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 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 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 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 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 st A = 1GateCircuit p,f holds
S = 1GateCircStr p,f
let p be FinSeqLen of ; :: 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 , f1 being Function of (n1 -tuples_on X1),X1 such that
A2: ( S = 1GateCircStr p1,f1 & 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, A2, PARTFUN1:def 4
.= the carrier' of (1GateCircStr p1,f1) by PARTFUN1:def 4
.= {[p1,f1]} by CIRCCOMB:def 6 ;
then [p,f] = [p1,f1] by ZFMISC_1:6;
then ( p = p1 & f = f1 ) by ZFMISC_1:33;
hence S = 1GateCircStr p,f by A2; :: thesis: verum