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

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

hence
union (rng A1) is Subset of X
by ZFMISC_1:76; :: thesis: verum
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;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