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) )
( rng phi c= On W & On W c= W ) by ORDINAL2:9;
then ( rng (phi | (Rank a)) c= rng phi & rng (phi | a) c= rng phi & rng phi c= W ) by RELAT_1:99, XBOOLE_1:1;
then ( rng (phi | (Rank a)) c= W & rng (phi | a) c= W & a c= Rank a ) by CLASSES1:44, XBOOLE_1:1;
then ( (phi | a) | (Rank a) = phi | a & W | (phi | (Rank a)) = phi | (Rank a) & phi | a = W | (phi | a) ) by FUNCT_1:82, RELAT_1:125;
hence ( union phi,a = Union (phi | a) & union (phi | a),a = Union (phi | a) ) by Th15; :: thesis: verum