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