let X be set ; :: thesis: for B being SetSequence of X

for n being Nat st B is V56() holds

(superior_setsequence B) . n = Union B

let B be SetSequence of X; :: thesis: for n being Nat st B is V56() holds

(superior_setsequence B) . n = Union B

let n be Nat; :: thesis: ( B is V56() implies (superior_setsequence B) . n = Union B )

defpred S_{1}[ Nat] means (superior_setsequence B) . $1 = Union B;

assume B is V56() ; :: thesis: (superior_setsequence B) . n = Union B

then A1: for k being Nat st S_{1}[k] holds

S_{1}[k + 1]
by Th41;

A2: S_{1}[ 0 ]
by Th18;

for k being Nat holds S_{1}[k]
from NAT_1:sch 2(A2, A1);

hence (superior_setsequence B) . n = Union B ; :: thesis: verum

for n being Nat st B is V56() holds

(superior_setsequence B) . n = Union B

let B be SetSequence of X; :: thesis: for n being Nat st B is V56() holds

(superior_setsequence B) . n = Union B

let n be Nat; :: thesis: ( B is V56() implies (superior_setsequence B) . n = Union B )

defpred S

assume B is V56() ; :: thesis: (superior_setsequence B) . n = Union B

then A1: for k being Nat st S

S

A2: S

for k being Nat holds S

hence (superior_setsequence B) . n = Union B ; :: thesis: verum