let f, x be set ; 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; 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)); ( 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; ( 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; verum