let S be one-gate ManySortedSign ; 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; 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 ; 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 ; 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; for p being FinSeqLen of n st A = 1GateCircuit (p,f) holds
S = 1GateCircStr (p,f)
let p be FinSeqLen of n; ( A = 1GateCircuit (p,f) implies S = 1GateCircStr (p,f) )
assume A1:
A = 1GateCircuit (p,f)
; 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; verum