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 2
.= the carrier' of (1GateCircStr (p1,f1)) by PARTFUN1:def 2
.= {[p1,f1]} by CIRCCOMB:def 6 ;
then A4: [p,f] = [p1,f1] by ZFMISC_1:3;
then p = p1 by XTUPLE_0:1;
hence S = 1GateCircStr (p,f) by A2, A4, XTUPLE_0:1; :: thesis: verum