let x be set ; :: thesis: for X being non empty finite set
for n being Element of NAT
for p being FinSeqLen of n
for g being Function of (n -tuples_on X),X
for s being State of (1GateCircuit (p,g)) holds s * p is Element of n -tuples_on X
let X be non empty finite set ; :: thesis: for n being Element of NAT
for p being FinSeqLen of n
for g being Function of (n -tuples_on X),X
for s being State of (1GateCircuit (p,g)) holds s * p is Element of n -tuples_on X
let n be Element of NAT ; :: thesis: for p being FinSeqLen of n
for g being Function of (n -tuples_on X),X
for s being State of (1GateCircuit (p,g)) holds s * p is Element of n -tuples_on X
let p be FinSeqLen of n; :: thesis: for g being Function of (n -tuples_on X),X
for s being State of (1GateCircuit (p,g)) holds s * p is Element of n -tuples_on X
let g be Function of (n -tuples_on X),X; :: thesis: for s being State of (1GateCircuit (p,g)) holds s * p is Element of n -tuples_on X
let s be State of (1GateCircuit (p,g)); :: thesis: s * p is Element of n -tuples_on X
set S = 1GateCircStr (p,g);
set A = 1GateCircuit (p,g);
A1: rng (s * p) c= X

proof

let o be object ; :: according to TARSKI:def 3 :: thesis: ( not o in rng (s * p) or o in X )
A2: rng s c= X

proof

reconsider tc = the carrier of (1GateCircStr (p,g)) as non empty set ;
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in rng s or z in X )
reconsider tS = the Sorts of (1GateCircuit (p,g)) as non-empty ManySortedSet of tc ;
assume z in rng s ; :: thesis: z in X
then consider a being object such that
A3: a in dom s and
A4: z = s . a by FUNCT_1:def 3;
reconsider a = a as Vertex of (1GateCircStr (p,g)) by A3, CIRCUIT1:3;
dom s = dom tS by CARD_3:9;
then s . a in the Sorts of (1GateCircuit (p,g)) . a by A3, CARD_3:9;
hence z in X by A4, CIRCCOMB:54; :: thesis: verum

end;

assume o in rng (s * p) ; :: thesis: o in X
then o in rng s by FUNCT_1:14;
hence o in X by A2; :: thesis: verum

end;

A5: rng p c= dom s

proof

let o be object ; :: according to TARSKI:def 3 :: thesis: ( not o in rng p or o in dom s )
assume o in rng p ; :: thesis: o in dom s
then o in (rng p) \/ {[p,g]} by XBOOLE_0:def 3;
then o in the carrier of (1GateCircStr (p,g)) by CIRCCOMB:def 6;
hence o in dom s by CIRCUIT1:3; :: thesis: verum

end;

then s * p is FinSequence by FINSEQ_1:16;
then reconsider sx = s * p as FinSequence of X by A1, FINSEQ_1:def 4;
len sx = len p by A5, FINSEQ_2:29
.= n by CARD_1:def 7 ;
hence s * p is Element of n -tuples_on X by FINSEQ_2:92; :: thesis: verum