let f, x be set ; :: thesis: for p being FinSequence
for g being Gate of (1GateCircStr p,f,x) holds
( g = [p,f] & the_arity_of g = p & the_result_sort_of g = x )
let p be FinSequence; :: thesis: for g being Gate of (1GateCircStr p,f,x) holds
( g = [p,f] & the_arity_of g = p & the_result_sort_of g = x )
set S = 1GateCircStr p,f,x;
let o be Gate of (1GateCircStr p,f,x); :: thesis: ( o = [p,f] & the_arity_of o = p & the_result_sort_of o = x )
A1: the ResultSort of (1GateCircStr p,f,x) . [p,f] = x by Def5;
A2: the carrier' of (1GateCircStr p,f,x) = {[p,f]} by Def5;
hence o = [p,f] by TARSKI:def 1; :: thesis: ( the_arity_of o = p & the_result_sort_of o = x )
the Arity of (1GateCircStr p,f,x) . [p,f] = p by Def5;
hence ( the_arity_of o = p & the_result_sort_of o = x ) by A2, A1, TARSKI:def 1; :: thesis: verum