let X be set ; :: thesis: for A1 being SetSequence of X holds union (rng A1) is Subset of X
let A1 be SetSequence of X; :: thesis: union (rng A1) is Subset of X
for Y being set st Y in rng A1 holds
Y c= X

proof

let Y be set ; :: thesis: ( Y in rng A1 implies Y c= X )
assume Y in rng A1 ; :: thesis: Y c= X
then consider y being object such that
A1: y in dom A1 and
A2: Y = A1 . y by FUNCT_1:def 3;
reconsider y = y as Element of NAT by A1, FUNCT_2:def 1;
Y = A1 . y by A2;
hence Y c= X ; :: thesis: verum

end;

hence union (rng A1) is Subset of X by ZFMISC_1:76; :: thesis: verum