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 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;
hence o = [p,f] by TARSKI:def 1; :: thesis: ( the_arity_of o = p & the_result_sort_of o = x )
thus ( the_arity_of o = p & the_result_sort_of o = x ) by A1, TARSKI:def 1; :: thesis: verum