let X be set ; :: thesis: for B being SetSequence of X holds (superior_setsequence B) . 0 = Union B
let B be SetSequence of X; :: thesis: (superior_setsequence B) . 0 = Union B
(superior_setsequence B) . 0 = union { (B . k) where k is Nat : 0 <= k } by Def3
.= union (rng B) by Th5
.= Union B by CARD_3:def 4 ;
hence (superior_setsequence B) . 0 = Union B ; :: thesis: verum