let S be non empty non void ManySortedSign ; for V being V2() 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 V2() 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 X be 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 t be Vertex of (X -CircuitStr); ( 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; ( 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
; 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; verum