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) 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 V2() 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 X be non empty Subset of (S -Terms V); ( ( 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}:];
let s be set ; ( s in the carrier' of (X -CircuitStr) implies s is CompoundTerm of S,V )
assume
s in the carrier' of (X -CircuitStr)
; 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; verum