let S be non empty non void ManySortedSign ; :: thesis: for V being V5() 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 V5() 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)

now

let t be Element of X; :: thesis: t is finite
t in X ;
hence t is finite ; :: thesis: verum

end;

hence g = (g . {} ) -tree (the_arity_of g) by TREES_9:def 13; :: thesis: verum