let S be non empty non void ManySortedSign ; :: thesis: for V being non-empty ManySortedSet of the carrier of S
for X being non empty Subset of (S -Terms V) holds
( ( for v being Vertex of (X -CircuitStr) holds v is Term of S,V ) & ( for s being set st s in the carrier' of (X -CircuitStr) holds
s is CompoundTerm of S,V ) )
let V be non-empty ManySortedSet of the carrier of S; :: thesis: for X being non empty Subset of (S -Terms V) holds
( ( for v being Vertex of (X -CircuitStr) holds v is Term of S,V ) & ( for s being set st s in the carrier' of (X -CircuitStr) holds
s is CompoundTerm of S,V ) )
let X be non empty Subset of (S -Terms V); :: thesis: ( ( for v being Vertex of (X -CircuitStr) holds v is Term of S,V ) & ( for s being set st s in the carrier' of (X -CircuitStr) holds
s is CompoundTerm of S,V ) )
set C = [: the carrier' of S,{ the carrier of S}:];

hereby :: thesis: for s being set st s in the carrier' of (X -CircuitStr) holds
s is CompoundTerm of S,V

let v be Vertex of (X -CircuitStr); :: thesis: v is Term of S,V
consider t being Element of X, p being Node of t such that
A1: v = t | p by TREES_9:19;
thus v is Term of S,V by A1; :: thesis: verum

end;

let s be set ; :: thesis: ( s in the carrier' of (X -CircuitStr) implies s is CompoundTerm of S,V )
assume s in the carrier' of (X -CircuitStr) ; :: thesis: s is CompoundTerm of S,V
then consider t being Element of X, p being Node of t such that
A2: s = t | p and
A3: ( not p in Leaves (dom t) or t . p in [: the carrier' of S,{ the carrier of S}:] ) by TREES_9:24;
reconsider s = s as Term of S,V by A2;
reconsider e = {} as Node of (t | p) by TREES_1:22;
A4: dom (t | p) = (dom t) | p by TREES_2:def 10;
p = p ^ e by FINSEQ_1:34;
then A5: t . p = s . e by A2, A4, TREES_2:def 10;
( p in Leaves (dom t) iff s is root ) by A2, TREES_9:6;
hence s is CompoundTerm of S,V by A3, A5, MSATERM:28, MSATERM:def 6; :: thesis: verum