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)
for t being Vertex of (X -CircuitStr) holds
( t in the carrier' of (X -CircuitStr) iff t 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)
for t being Vertex of (X -CircuitStr) holds
( t in the carrier' of (X -CircuitStr) iff t is CompoundTerm of S,V )
let X be non empty Subset of (S -Terms V); :: thesis: for t being Vertex of (X -CircuitStr) holds
( t in the carrier' of (X -CircuitStr) iff t is CompoundTerm of S,V )
let t be Vertex of (X -CircuitStr); :: thesis: ( t in the carrier' of (X -CircuitStr) iff t is CompoundTerm of S,V )
thus ( t in the carrier' of (X -CircuitStr) implies t is CompoundTerm of S,V ) by Th4; :: thesis: ( t is CompoundTerm of S,V implies t in the carrier' of (X -CircuitStr) )
set C = [: the carrier' of S,{ the carrier of S}:];
consider tt being Element of X, p being Node of tt such that
A1: t = tt | p by TREES_9:19;
assume t is CompoundTerm of S,V ; :: thesis: t in the carrier' of (X -CircuitStr)
then reconsider t9 = t as CompoundTerm of S,V ;
A2: t9 . {} in [: the carrier' of S,{ the carrier of S}:] by MSATERM:def 6;
A3: p ^ (<*> NAT) = p by FINSEQ_1:34;
{} in (dom tt) | p by TREES_1:22;
then tt . p in [: the carrier' of S,{ the carrier of S}:] by A1, A2, A3, TREES_2:def 10;
hence t in the carrier' of (X -CircuitStr) by A1, TREES_9:24; :: thesis: verum