let X be non empty functional compatible set ; :: thesis: rng (union X) = union { (rng f) where f is Element of X : verum }
set F = { (rng f) where f is Element of X : verum } ;
now :: thesis: for y being object holds
( ( y in rng (union X) implies y in union { (rng f) where f is Element of X : verum } ) & ( y in union { (rng f) where f is Element of X : verum } implies y in rng (union X) ) )
let y be object ; :: thesis: ( ( y in rng (union X) implies y in union { (rng f) where f is Element of X : verum } ) & ( y in union { (rng f) where f is Element of X : verum } implies y in rng (union X) ) )
hereby :: thesis: ( y in union { (rng f) where f is Element of X : verum } implies y in rng (union X) )
assume y in rng (union X) ; :: thesis: y in union { (rng f) where f is Element of X : verum }
then consider x being object such that
A1: [x,y] in union X by XTUPLE_0:def 13;
consider Z being set such that
A2: [x,y] in Z and
A3: Z in X by A1, TARSKI:def 4;
reconsider Z = Z as Element of X by A3;
A4: rng Z in { (rng f) where f is Element of X : verum } ;
y in rng Z by A2, XTUPLE_0:def 13;
hence y in union { (rng f) where f is Element of X : verum } by A4, TARSKI:def 4; :: thesis: verum
end;
assume y in union { (rng f) where f is Element of X : verum } ; :: thesis: y in rng (union X)
then consider Z being set such that
A5: y in Z and
A6: Z in { (rng f) where f is Element of X : verum } by TARSKI:def 4;
consider f being Element of X such that
A7: Z = rng f by A6;
consider x being object such that
A8: [x,y] in f by A5, A7, XTUPLE_0:def 13;
[x,y] in union X by A8, TARSKI:def 4;
hence y in rng (union X) by XTUPLE_0:def 13; :: thesis: verum
end;
hence rng (union X) = union { (rng f) where f is Element of X : verum } by TARSKI:2; :: thesis: verum