let a be Element of A; :: thesis: a is Element of Union X

per cases ( I = {} or I <> {} ) ;

suppose I = {} ; :: thesis: a is Element of Union X

then A1: ( rng X = {} & X = {} & Union ({} --> I) = {} ) by FUNCT_6:26;
thus a is Element of Union X by A1, SUBSET_1:def 1; :: thesis: verum

end;

suppose I <> {} ; :: thesis: a is Element of Union X

then consider x being object such that
A2: ( x in dom X & A = X . x ) by FUNCT_1:def 3;
thus a is Element of Union X by A2, CARD_5:2; :: thesis: verum

end;

end;