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 Def14;
then A1: for x being set 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 4;
hence the Charact of (1GateCircuit p,f) = p,f .--> f by A1, FUNCOP_1:17; :: 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 Def14;
hence the Sorts of (1GateCircuit p,f) . v = X by FUNCOP_1:13; :: thesis: verum