let n be Nat; :: thesis: for X being non empty set
for f being Function of (n -tuples_on X),X
for p being FinSeqLen of n holds
( the Charact of (1GateCircuit (p,f)) = (p,f) .--> f & ( for v being Vertex of (1GateCircStr (p,f)) holds the Sorts of (1GateCircuit (p,f)) . v = X ) )
let X be non empty set ; :: thesis: for f being Function of (n -tuples_on X),X
for p being FinSeqLen of n holds
( the Charact of (1GateCircuit (p,f)) = (p,f) .--> f & ( for v being Vertex of (1GateCircStr (p,f)) holds the Sorts of (1GateCircuit (p,f)) . v = X ) )
let f be Function of (n -tuples_on X),X; :: thesis: for p being FinSeqLen of n holds
( the Charact of (1GateCircuit (p,f)) = (p,f) .--> f & ( for v being Vertex of (1GateCircStr (p,f)) holds the Sorts of (1GateCircuit (p,f)) . v = X ) )
let p be FinSeqLen of n; :: thesis: ( the Charact of (1GateCircuit (p,f)) = (p,f) .--> f & ( for v being Vertex of (1GateCircStr (p,f)) holds the Sorts of (1GateCircuit (p,f)) . v = X ) )
set S = 1GateCircStr (p,f);
set A = 1GateCircuit (p,f);
the Charact of (1GateCircuit (p,f)) . [p,f] = f by Def13;
then A1: for x being object st x in {[p,f]} holds
the Charact of (1GateCircuit (p,f)) . x = f by TARSKI:def 1;
the carrier' of (1GateCircStr (p,f)) = {[p,f]} by Def6;
then dom the Charact of (1GateCircuit (p,f)) = {[p,f]} by PARTFUN1:def 2;
hence the Charact of (1GateCircuit (p,f)) = (p,f) .--> f by A1, FUNCOP_1:11; :: thesis: for v being Vertex of (1GateCircStr (p,f)) holds the Sorts of (1GateCircuit (p,f)) . v = X
let v be Vertex of (1GateCircStr (p,f)); :: thesis: the Sorts of (1GateCircuit (p,f)) . v = X
the Sorts of (1GateCircuit (p,f)) = the carrier of (1GateCircStr (p,f)) --> X by Def13;
hence the Sorts of (1GateCircuit (p,f)) . v = X ; :: thesis: verum