let n be Nat; :: thesis: for X being set
for A1 being SetSequence of X holds (superior_setsequence A1) . n = Union (A1 ^\ n)
let X be set ; :: thesis: for A1 being SetSequence of X holds (superior_setsequence A1) . n = Union (A1 ^\ n)
let A1 be SetSequence of X; :: thesis: (superior_setsequence A1) . n = Union (A1 ^\ n)
reconsider Y = { (A1 . k) where k is Nat : n <= k } as Subset-Family of X by SETLIM_1:28;
(superior_setsequence A1) . n = union Y by SETLIM_1:def 3
.= union (rng (A1 ^\ n)) by SETLIM_1:6 ;
hence (superior_setsequence A1) . n = Union (A1 ^\ n) by CARD_3:def 4; :: thesis: verum