let f, x be set ; :: thesis: for p being FinSequence holds
( the Arity of (1GateCircStr (p,f,x)) = (p,f) .--> p & the ResultSort of (1GateCircStr (p,f,x)) = (p,f) .--> x )
let p be FinSequence; :: thesis: ( the Arity of (1GateCircStr (p,f,x)) = (p,f) .--> p & the ResultSort of (1GateCircStr (p,f,x)) = (p,f) .--> x )
set S = 1GateCircStr (p,f,x);
the Arity of (1GateCircStr (p,f,x)) . [p,f] = p by Def5;
then A1: for x being object st x in {[p,f]} holds
the Arity of (1GateCircStr (p,f,x)) . x = p by TARSKI:def 1;
A2: the carrier' of (1GateCircStr (p,f,x)) = {[p,f]} by Def5;
then dom the Arity of (1GateCircStr (p,f,x)) = {[p,f]} by FUNCT_2:def 1;
hence the Arity of (1GateCircStr (p,f,x)) = (p,f) .--> p by A1, FUNCOP_1:11; :: thesis: the ResultSort of (1GateCircStr (p,f,x)) = (p,f) .--> x
the ResultSort of (1GateCircStr (p,f,x)) . [p,f] = x by Def5;
then A3: for y being object st y in {[p,f]} holds
the ResultSort of (1GateCircStr (p,f,x)) . y = x by TARSKI:def 1;
dom the ResultSort of (1GateCircStr (p,f,x)) = {[p,f]} by A2, FUNCT_2:def 1;
hence the ResultSort of (1GateCircStr (p,f,x)) = (p,f) .--> x by A3, FUNCOP_1:11; :: thesis: verum