defpred S₁[ object , object ] means for i being Element of I st $1 in X . i holds
$2 = (F . i) . $1;
A1: for x being object st x in Union X holds
ex y being object st
( y in Union D & S₁[x,y] )

proof

let e be object ; :: thesis: ( e in Union X implies ex y being object st
( y in Union D & S₁[e,y] ) )
assume e in Union X ; :: thesis: ex y being object st
( y in Union D & S₁[e,y] )
then consider i being object such that
A2: i in dom X and
A3: e in X . i by CARD_5:2;
reconsider i = i as Element of I by A2, PARTFUN1:def 2;
take u = (F . i) . e; :: thesis: ( u in Union D & S₁[e,u] )
i in I ;
then A4: i in dom D by PARTFUN1:def 2;
(F . i) . e in D . i by A3, FUNCT_2:5;
hence u in Union D by A4, CARD_5:2; :: thesis: S₁[e,u]
let i9 be Element of I; :: thesis: ( e in X . i9 implies u = (F . i9) . e )
assume e in X . i9 ; :: thesis: u = (F . i9) . e
then X . i9 meets X . i by A3, XBOOLE_0:3;
hence u = (F . i9) . e by PROB_2:def 2; :: thesis: verum

end;

consider f being Function of (Union X),(Union D) such that
A5: for e being object st e in Union X holds
S₁[e,f . e] from FUNCT_2:sch 1(A1);
take f ; :: thesis: for i being Element of I
for x being set st x in X . i holds
f . x = (F . i) . x
let i be Element of I; :: thesis: for x being set st x in X . i holds
f . x = (F . i) . x
let x be set ; :: thesis: ( x in X . i implies f . x = (F . i) . x )
assume A6: x in X . i ; :: thesis: f . x = (F . i) . x
i in I ;
then i in dom X by PARTFUN1:def 2;
then x in Union X by A6, CARD_5:2;
hence f . x = (F . i) . x by A5, A6; :: thesis: verum