let S be non empty non void ManySortedSign ; :: thesis: for V being non-empty ManySortedSet of the carrier of S
for X being SetWithCompoundTerm of S,V
for g being Gate of (X -CircuitStr) holds g = (g . {}) -tree (the_arity_of g)
let V be non-empty ManySortedSet of the carrier of S; :: thesis: for X being SetWithCompoundTerm of S,V
for g being Gate of (X -CircuitStr) holds g = (g . {}) -tree (the_arity_of g)
let X be SetWithCompoundTerm of S,V; :: thesis: for g being Gate of (X -CircuitStr) holds g = (g . {}) -tree (the_arity_of g)
let g be Gate of (X -CircuitStr); :: thesis: g = (g . {}) -tree (the_arity_of g)
for t being Element of X holds t is finite ;
hence g = (g . {}) -tree (the_arity_of g) by TREES_9:def 13; :: thesis: verum