let S be non empty non void ManySortedSign ; :: thesis: for V being V5() ManySortedSet of
for X being non empty Subset of holds
( ( for v being Vertex of holds v is Term of the carrier of K345(S,b₁), ) & ( for s being set st s in the carrier' of (X -CircuitStr ) holds
s is CompoundTerm of S,V ) )
let V be V5() ManySortedSet of ; :: thesis: for X being non empty Subset of holds
( ( for v being Vertex of holds v is Term of the carrier of K345(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 ; :: thesis: ( ( for v being Vertex of holds v is Term of the carrier of K345(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 ; :: thesis: v is Term of the carrier of K345(S,V),
consider t being Element of X, p being Node of such that
A1: v = t | p by TREES_9:20;
t in X ;
hence v is Term of the carrier of K345(S,V), by A1, MSATERM:29; :: 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 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:25;
t in X ;
then reconsider s = s as Term of the carrier of K345(S,V), by A2, MSATERM:29;
reconsider e = {} as Node of by TREES_1:47;
A4: dom (t | p) = (dom t) | p by TREES_2:def 11;
p = p ^ e by FINSEQ_1:47;
then A5: t . p = s . e by A2, A4, TREES_2:def 11;
( 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