let F1, F2 be Function of (Union X),(Union D); :: thesis: ( ( for i being Element of I
for x being set st x in X . i holds
F1 . x = (F . i) . x ) & ( for i being Element of I
for x being set st x in X . i holds
F2 . x = (F . i) . x ) implies F1 = F2 )
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: F1 = F2

now :: thesis: for x being object st x in Union X holds
F1 . x = F2 . x

let x be object ; :: thesis: ( x in Union X implies F1 . x = F2 . x )
assume x in Union X ; :: thesis: F1 . x = F2 . x
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: verum

end;

hence F1 = F2 by FUNCT_2:12; :: thesis: verum