let S be non empty non void ManySortedSign ; :: thesis: for V being V5() ManySortedSet of
for X being non empty Subset of
for t being Vertex of holds
( t in the carrier' of (X -CircuitStr ) iff t is CompoundTerm of S,V )
let V be V5() ManySortedSet of ; :: thesis: for X being non empty Subset of
for t being Vertex of holds
( t in the carrier' of (X -CircuitStr ) iff t is CompoundTerm of S,V )
let X be non empty Subset of ; :: thesis: for t being Vertex of holds
( t in the carrier' of (X -CircuitStr ) iff t is CompoundTerm of S,V )
let t be Vertex of ; :: 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 such that
A1: t = tt | p by TREES_9:20;
assume t is CompoundTerm of S,V ; :: thesis: t in the carrier' of (X -CircuitStr )
then reconsider t' = t as CompoundTerm of S,V ;
A2: t' . {} in [:the carrier' of S,{the carrier of S}:] by MSATERM:def 6;
A3: p ^ (<*> NAT ) = p by FINSEQ_1:47;
{} in (dom tt) | p by TREES_1:47;
then tt . p in [:the carrier' of S,{the carrier of S}:] by A1, A2, A3, TREES_2:def 11;
hence t in the carrier' of (X -CircuitStr ) by A1, TREES_9:25; :: thesis: verum