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;
A1: ( the carrier' of (1GateCircStr p,f,x) = {[p,f]} & the Arity of (1GateCircStr p,f,x) . [p,f] = p & the ResultSort of (1GateCircStr p,f,x) . [p,f] = x ) by Def5;
then A2: ( dom the Arity of (1GateCircStr p,f,x) = {[p,f]} & dom the ResultSort of (1GateCircStr p,f,x) = {[p,f]} ) by FUNCT_2:def 1;
for x being set st x in {[p,f]} holds
the Arity of (1GateCircStr p,f,x) . x = p by A1, TARSKI:def 1;
hence the Arity of (1GateCircStr p,f,x) = p,f .--> p by A2, FUNCOP_1:17; :: thesis: the ResultSort of (1GateCircStr p,f,x) = p,f .--> x
for y being set st y in {[p,f]} holds
the ResultSort of (1GateCircStr p,f,x) . y = x by A1, TARSKI:def 1;
hence the ResultSort of (1GateCircStr p,f,x) = p,f .--> x by A2, FUNCOP_1:17; :: thesis: verum