let S be non empty non void ManySortedSign ; :: thesis: for V being non-empty ManySortedSet of the carrier of S
for A being non-empty MSAlgebra over 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 non-empty ManySortedSet of the carrier of S; :: thesis: for A being non-empty MSAlgebra over 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 over 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 Th12;
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) by MSATERM:22;
A4: a = ag by A1, A2, TREES_4:15;
A5: dom (the_arity_of o) = Seg (len a) by A3, FINSEQ_1:def 3;
A6: dom (the_arity_of g) = Seg (len a) by A4, FINSEQ_1:def 3;
A7: rng (the_arity_of g) c= the carrier of (t -CircuitStr) by FINSEQ_1:def 4;
A8: rng (the_arity_of o) c= the carrier of S by FINSEQ_1:def 4;
A9: dom (t -CircuitSorts A) = the carrier of (t -CircuitStr) by PARTFUN1:def 2;
A10: dom the Sorts of A = the carrier of S by PARTFUN1:def 2;
A11: dom ((t -CircuitSorts A) * (the_arity_of g)) = Seg (len a) by A6, A7, A9, RELAT_1:27;
A12: dom ( the Sorts of A * (the_arity_of o)) = Seg (len a) by A5, A8, A10, RELAT_1:27;

now :: thesis: for i being object st i in Seg (len a) holds
((t -CircuitSorts A) * (the_arity_of g)) . i = ( the Sorts of A * (the_arity_of o)) . i

let i be object ; :: 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 A13: 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 A6, A13, FUNCT_1:def 3;
then reconsider v = ag . j as Vertex of (t -CircuitStr) by A7;
(the_arity_of o) . i in rng (the_arity_of o) by A5, A13, FUNCT_1:def 3;
then reconsider s = (the_arity_of o) . j as SortSymbol of S by A8;
reconsider u = v as Term of S,V by A4, A6, A13, MSATERM:22;
A14: the_sort_of u = s by A4, A6, A13, MSATERM:23;
A15: ((t -CircuitSorts A) * (the_arity_of g)) . i = (t -CircuitSorts A) . v by A11, A13, FUNCT_1:12;
A16: ( the Sorts of A * (the_arity_of o)) . i = the Sorts of A . s by A12, A13, FUNCT_1:12;
thus ((t -CircuitSorts A) * (the_arity_of g)) . i = the_sort_of (v,A) by A15, Def4
.= ( the Sorts of A * (the_arity_of o)) . i by A14, A16, Def2 ; :: thesis: verum

end;

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