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;