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:7;
then ( rng (phi | a) c= rng phi & rng phi c= W ) by RELAT_1:70;
then ( a c= Rank a & phi | a = W |` (phi | a) ) by CLASSES1:38, RELAT_1:94, XBOOLE_1:1;
hence ( union (phi,a) = Union (phi | a) & union ((phi | a),a) = Union (phi | a) ) by Th13, FUNCT_1:51; :: thesis: verum