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

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