let W be Universe; :: thesis: for a being Ordinal of W
for phi being Ordinal-Sequence of W holds
( union phi,a = Union (phi | a) & union (phi | a),a = Union (phi | a) )
let a be Ordinal of W; :: thesis: for phi being Ordinal-Sequence of W holds
( union phi,a = Union (phi | a) & union (phi | a),a = Union (phi | a) )
let phi be Ordinal-Sequence of W; :: thesis: ( union phi,a = Union (phi | a) & union (phi | a),a = Union (phi | a) )
On W c= W by ORDINAL2:9;
then ( rng (phi | a) c= rng phi & rng phi c= W ) by RELAT_1:99, XBOOLE_1:1;
then ( a c= Rank a & phi | a = W | (phi | a) ) by CLASSES1:44, RELAT_1:125, XBOOLE_1:1;
hence ( union phi,a = Union (phi | a) & union (phi | a),a = Union (phi | a) ) by Th15, FUNCT_1:82; :: thesis: verum