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