let S be non empty non void ManySortedSign ; :: thesis: for V being V5() ManySortedSet of
for A being non-empty MSAlgebra of S
for X being SetWithCompoundTerm of S,V
for g being Gate of (X -CircuitStr )
for o being OperSymbol of S st g . {} = [o,the carrier of S] holds
(X -CircuitSorts A) * (the_arity_of g) = the Sorts of A * (the_arity_of o)
let V be V5() ManySortedSet of ; :: thesis: for A being non-empty MSAlgebra of S
for X being SetWithCompoundTerm of S,V
for g being Gate of (X -CircuitStr )
for o being OperSymbol of S st g . {} = [o,the carrier of S] holds
(X -CircuitSorts A) * (the_arity_of g) = the Sorts of A * (the_arity_of o)
let A be non-empty MSAlgebra of S; :: thesis: for X being SetWithCompoundTerm of S,V
for g being Gate of (X -CircuitStr )
for o being OperSymbol of S st g . {} = [o,the carrier of S] holds
(X -CircuitSorts A) * (the_arity_of g) = the Sorts of A * (the_arity_of o)
let t be SetWithCompoundTerm of S,V; :: thesis: for g being Gate of (t -CircuitStr )
for o being OperSymbol of S st g . {} = [o,the carrier of S] holds
(t -CircuitSorts A) * (the_arity_of g) = the Sorts of A * (the_arity_of o)
let g be Gate of (t -CircuitStr ); :: thesis: for o being OperSymbol of S st g . {} = [o,the carrier of S] holds
(t -CircuitSorts A) * (the_arity_of g) = the Sorts of A * (the_arity_of o)
set X = t;
reconsider f = g as CompoundTerm of S,V by Th4;
reconsider ag = the_arity_of g as FinSequence of Subtrees t ;
A1: g = (f . {} ) -tree ag by Th13;
let o be OperSymbol of S; :: thesis: ( g . {} = [o,the carrier of S] implies (t -CircuitSorts A) * (the_arity_of g) = the Sorts of A * (the_arity_of o) )
assume g . {} = [o,the carrier of S] ; :: thesis: (t -CircuitSorts A) * (the_arity_of g) = the Sorts of A * (the_arity_of o)
then consider a being ArgumentSeq of Sym o,V such that
A2: f = [o,the carrier of S] -tree a by MSATERM:10;
A3: ( len a = len (the_arity_of o) & a = ag ) by A1, A2, MSATERM:22, TREES_4:15;
then A4: ( dom (the_arity_of o) = Seg (len a) & dom (the_arity_of g) = Seg (len a) & dom a = Seg (len a) ) by FINSEQ_1:def 3;
A5: ( rng (the_arity_of g) c= the carrier of (t -CircuitStr ) & rng (the_arity_of o) c= the carrier of S ) by FINSEQ_1:def 4;
( dom (t -CircuitSorts A) = the carrier of (t -CircuitStr ) & dom the Sorts of A = the carrier of S ) by PARTFUN1:def 4;
then A6: ( dom ((t -CircuitSorts A) * (the_arity_of g)) = Seg (len a) & dom (the Sorts of A * (the_arity_of o)) = Seg (len a) ) by A4, A5, RELAT_1:46;

now

let i be set ; :: thesis: ( i in Seg (len a) implies ((t -CircuitSorts A) * (the_arity_of g)) . i = (the Sorts of A * (the_arity_of o)) . i )
assume A7: i in Seg (len a) ; :: thesis: ((t -CircuitSorts A) * (the_arity_of g)) . i = (the Sorts of A * (the_arity_of o)) . i
then reconsider j = i as Element of NAT ;
ag . i in rng (the_arity_of g) by A4, A7, FUNCT_1:def 5;
then reconsider v = ag . j as Vertex of (t -CircuitStr ) by A5;
(the_arity_of o) . i in rng (the_arity_of o) by A4, A7, FUNCT_1:def 5;
then reconsider s = (the_arity_of o) . j as SortSymbol of S by A5;
reconsider u = v as Term of S,V by A3, A4, A7, MSATERM:22;
A8: the_sort_of u = s by A3, A4, A7, MSATERM:23;
A9: ( ((t -CircuitSorts A) * (the_arity_of g)) . i = (t -CircuitSorts A) . v & (the Sorts of A * (the_arity_of o)) . i = the Sorts of A . s ) by A6, A7, FUNCT_1:22;
hence ((t -CircuitSorts A) * (the_arity_of g)) . i = the_sort_of v,A by Def4
.= (the Sorts of A * (the_arity_of o)) . i by A8, A9, Def2 ;
:: thesis: verum

end;

hence (t -CircuitSorts A) * (the_arity_of g) = the Sorts of A * (the_arity_of o) by A6, FUNCT_1:9; :: thesis: verum