let F1, F2 be Function of (Union X),(Union D); :: thesis:
assume that
A7: for i being Element of I
for x being set st x in X . i holds
F1 . x = (F . i) . x and
A8: for i being Element of I
for x being set st x in X . i holds
F2 . x = (F . i) . x ; :: thesis:

let x be object ; :: thesis:
assume x in Union X ; :: thesis:
then consider i being object such that
A9: i in dom X and
A10: x in X . i by CARD_5:2;
reconsider i = i as Element of I by A9, PARTFUN1:def 2;
thus F1 . x = (F . i) . x by A7, A10
.= F2 . x by A8, A10 ; :: thesis:

end;