let S be non empty non void ManySortedSign ; :: thesis: for V being non-empty ManySortedSet of the carrier of S
for X1, X2 being non empty Subset of (S -Terms V) holds (X1 \/ X2) -CircuitStr = (X1 -CircuitStr) +* (X2 -CircuitStr)
let V be non-empty ManySortedSet of the carrier of S; :: thesis: for X1, X2 being non empty Subset of (S -Terms V) holds (X1 \/ X2) -CircuitStr = (X1 -CircuitStr) +* (X2 -CircuitStr)
let X1, X2 be non empty Subset of (S -Terms V); :: thesis: (X1 \/ X2) -CircuitStr = (X1 -CircuitStr) +* (X2 -CircuitStr)
set X = X1 \/ X2;
set C = [: the carrier' of S,{ the carrier of S}:];
A1: Subtrees (X1 \/ X2) = (Subtrees X1) \/ (Subtrees X2) by Th7;
A2: [: the carrier' of S,{ the carrier of S}:] -Subtrees (X1 \/ X2) = ([: the carrier' of S,{ the carrier of S}:] -Subtrees X1) \/ ([: the carrier' of S,{ the carrier of S}:] -Subtrees X2) by Th8;
( ( for t being Element of X1 holds t is finite ) & ( for t being Element of X2 holds t is finite ) ) ;
then A3: [: the carrier' of S,{ the carrier of S}:] -ImmediateSubtrees (X1 \/ X2) = ([: the carrier' of S,{ the carrier of S}:] -ImmediateSubtrees X1) +* ([: the carrier' of S,{ the carrier of S}:] -ImmediateSubtrees X2) by Th9;
id ([: the carrier' of S,{ the carrier of S}:] -Subtrees (X1 \/ X2)) = (id ([: the carrier' of S,{ the carrier of S}:] -Subtrees X1)) +* (id ([: the carrier' of S,{ the carrier of S}:] -Subtrees X2)) by A2, FUNCT_4:22;
hence (X1 \/ X2) -CircuitStr = (X1 -CircuitStr) +* (X2 -CircuitStr) by A1, A2, A3, CIRCCOMB:def 2; :: thesis: verum