let X1, X2 be non empty constituted-DTrees set ; :: thesis: ( ( for t being Element of X1 holds t is finite ) & ( for t being Element of X2 holds t is finite ) implies for C being set holds C -ImmediateSubtrees (X1 \/ X2) = (C -ImmediateSubtrees X1) +* (C -ImmediateSubtrees X2) )
assume that
A1: for t being Element of X1 holds t is finite and
A2: for t being Element of X2 holds t is finite ; :: thesis: for C being set holds C -ImmediateSubtrees (X1 \/ X2) = (C -ImmediateSubtrees X1) +* (C -ImmediateSubtrees X2)

A3: now :: thesis: for t being Element of X1 \/ X2 holds t is finite

let t be Element of X1 \/ X2; :: thesis: t is finite
( t in X1 or t in X2 ) by XBOOLE_0:def 3;
hence t is finite by A1, A2; :: thesis: verum

end;

let C be set ; :: thesis: C -ImmediateSubtrees (X1 \/ X2) = (C -ImmediateSubtrees X1) +* (C -ImmediateSubtrees X2)
set X = X1 \/ X2;
set f = C -ImmediateSubtrees (X1 \/ X2);
set f1 = C -ImmediateSubtrees X1;
set f2 = C -ImmediateSubtrees X2;
A4: dom (C -ImmediateSubtrees (X1 \/ X2)) = C -Subtrees (X1 \/ X2) by FUNCT_2:def 1;
A5: dom (C -ImmediateSubtrees X1) = C -Subtrees X1 by FUNCT_2:def 1;
A6: dom (C -ImmediateSubtrees X2) = C -Subtrees X2 by FUNCT_2:def 1;
A7: C -Subtrees (X1 \/ X2) = (C -Subtrees X1) \/ (C -Subtrees X2) by Th8;

now :: thesis: for x being object st x in (dom (C -ImmediateSubtrees X1)) \/ (dom (C -ImmediateSubtrees X2)) holds
( ( x in dom (C -ImmediateSubtrees X2) implies (C -ImmediateSubtrees (X1 \/ X2)) . x = (C -ImmediateSubtrees X2) . x ) & ( not x in dom (C -ImmediateSubtrees X2) implies (C -ImmediateSubtrees (X1 \/ X2)) . x = (C -ImmediateSubtrees X1) . x ) )

let x be object ; :: thesis: ( x in (dom (C -ImmediateSubtrees X1)) \/ (dom (C -ImmediateSubtrees X2)) implies ( ( x in dom (C -ImmediateSubtrees X2) implies (C -ImmediateSubtrees (X1 \/ X2)) . x = (C -ImmediateSubtrees X2) . x ) & ( not x in dom (C -ImmediateSubtrees X2) implies (C -ImmediateSubtrees (X1 \/ X2)) . x = (C -ImmediateSubtrees X1) . x ) ) )
assume A8: x in (dom (C -ImmediateSubtrees X1)) \/ (dom (C -ImmediateSubtrees X2)) ; :: thesis: ( ( x in dom (C -ImmediateSubtrees X2) implies (C -ImmediateSubtrees (X1 \/ X2)) . x = (C -ImmediateSubtrees X2) . x ) & ( not x in dom (C -ImmediateSubtrees X2) implies (C -ImmediateSubtrees (X1 \/ X2)) . x = (C -ImmediateSubtrees X1) . x ) )
then reconsider t = x as Element of Subtrees (X1 \/ X2) by A5, A6, A7;
(C -ImmediateSubtrees (X1 \/ X2)) . x in (Subtrees (X1 \/ X2)) * by A5, A6, A7, A8, FUNCT_2:5;
then reconsider p = (C -ImmediateSubtrees (X1 \/ X2)) . x as FinSequence of Subtrees (X1 \/ X2) by FINSEQ_1:def 11;

hereby :: thesis: ( not x in dom (C -ImmediateSubtrees X2) implies (C -ImmediateSubtrees (X1 \/ X2)) . x = (C -ImmediateSubtrees X1) . x )

assume A9: x in dom (C -ImmediateSubtrees X2) ; :: thesis: (C -ImmediateSubtrees (X1 \/ X2)) . x = (C -ImmediateSubtrees X2) . x
then (C -ImmediateSubtrees X2) . x in (Subtrees X2) * by A6, FUNCT_2:5;
then reconsider p2 = (C -ImmediateSubtrees X2) . x as FinSequence of Subtrees X2 by FINSEQ_1:def 11;
A10: t = (t . {}) -tree p by A3, A5, A6, A7, A8, TREES_9:def 13;
t = (t . {}) -tree p2 by A2, A6, A9, TREES_9:def 13;
hence (C -ImmediateSubtrees (X1 \/ X2)) . x = (C -ImmediateSubtrees X2) . x by A10, TREES_4:15; :: thesis: verum

end;

assume not x in dom (C -ImmediateSubtrees X2) ; :: thesis: (C -ImmediateSubtrees (X1 \/ X2)) . x = (C -ImmediateSubtrees X1) . x
then A11: x in dom (C -ImmediateSubtrees X1) by A8, XBOOLE_0:def 3;
then (C -ImmediateSubtrees X1) . x in (Subtrees X1) * by A5, FUNCT_2:5;
then reconsider p1 = (C -ImmediateSubtrees X1) . x as FinSequence of Subtrees X1 by FINSEQ_1:def 11;
A12: t = (t . {}) -tree p by A3, A5, A6, A7, A8, TREES_9:def 13;
t = (t . {}) -tree p1 by A1, A5, A11, TREES_9:def 13;
hence (C -ImmediateSubtrees (X1 \/ X2)) . x = (C -ImmediateSubtrees X1) . x by A12, TREES_4:15; :: thesis: verum

end;

hence C -ImmediateSubtrees (X1 \/ X2) = (C -ImmediateSubtrees X1) +* (C -ImmediateSubtrees X2) by A4, A5, A6, A7, FUNCT_4:def 1; :: thesis: verum