let S be non empty non void ManySortedSign ; :: thesis: for V being V5() ManySortedSet of
for X1, X2 being non empty Subset of (S -Terms V) holds (X1 \/ X2) -CircuitStr = (X1 -CircuitStr ) +* (X2 -CircuitStr )
let V be V5() ManySortedSet of ; :: 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 Th8;
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 Th9;

now

hereby :: thesis: for t being Element of X2 holds t is finite

let t be Element of X1; :: thesis: t is finite
t in X1 ;
then t is Term of S,V ;
hence t is finite ; :: thesis: verum

end;

hereby :: thesis: verum

let t be Element of X2; :: thesis: t is finite
t in X2 ;
then t is Term of S,V ;
hence t is finite ; :: thesis: verum

end;

end;

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 Th10;
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:23;
hence (X1 \/ X2) -CircuitStr = (X1 -CircuitStr ) +* (X2 -CircuitStr ) by A1, A2, A3, CIRCCOMB:def 2; :: thesis: verum