for X being set

for A being SetSequence of X ex S being SetSequence of X st

for n being Nat holds S . n = Union (A ^\ n)_{1} being SetSequence of X st

for n being Nat holds b_{1} . n = Union (A ^\ n)
; :: thesis: verum

for A being SetSequence of X ex S being SetSequence of X st

for n being Nat holds S . n = Union (A ^\ n)

proof

hence
ex b
let X be set ; :: thesis: for A being SetSequence of X ex S being SetSequence of X st

for n being Nat holds S . n = Union (A ^\ n)

let A be SetSequence of X; :: thesis: ex S being SetSequence of X st

for n being Nat holds S . n = Union (A ^\ n)

ex J being SetSequence of X st

( J . 0 = Union (A ^\ 0) & ( for n being Nat holds J . (n + 1) = Union (A ^\ (n + 1)) ) )

A4: ( J . 0 = Union (A ^\ 0) & ( for n being Nat holds J . (n + 1) = Union (A ^\ (n + 1)) ) ) ;

A5: ( J . 0 = Union (A ^\ 0) & ( for n being Nat holds J . (n + 1) = Union (A ^\ (n + 1)) ) implies for n being Nat holds J . n = Union (A ^\ n) )

thus for n being Nat holds J . n = Union (A ^\ n) by A4, A5; :: thesis: verum

end;for n being Nat holds S . n = Union (A ^\ n)

let A be SetSequence of X; :: thesis: ex S being SetSequence of X st

for n being Nat holds S . n = Union (A ^\ n)

ex J being SetSequence of X st

( J . 0 = Union (A ^\ 0) & ( for n being Nat holds J . (n + 1) = Union (A ^\ (n + 1)) ) )

proof

then consider J being SetSequence of X such that
defpred S_{1}[ set , set , set ] means for x, y being Subset of X

for k being Nat st k = $1 & x = $2 & y = $3 holds

y = Union (A ^\ (k + 1));

A1: for n being Nat

for x being Subset of X ex y being Subset of X st S_{1}[n,x,y]

A2: J . 0 = Union (A ^\ 0) and

A3: for n being Nat holds S_{1}[n,J . n,J . (n + 1)]
from RECDEF_1:sch 2(A1);

take J ; :: thesis: ( J . 0 = Union (A ^\ 0) & ( for n being Nat holds J . (n + 1) = Union (A ^\ (n + 1)) ) )

thus J . 0 = Union (A ^\ 0) by A2; :: thesis: for n being Nat holds J . (n + 1) = Union (A ^\ (n + 1))

let n be Nat; :: thesis: J . (n + 1) = Union (A ^\ (n + 1))

reconsider nn = n, nn1 = n + 1 as Element of NAT by ORDINAL1:def 12;

S_{1}[n,J . nn,J . nn1]
by A3;

hence J . (n + 1) = Union (A ^\ (n + 1)) ; :: thesis: verum

end;for k being Nat st k = $1 & x = $2 & y = $3 holds

y = Union (A ^\ (k + 1));

A1: for n being Nat

for x being Subset of X ex y being Subset of X st S

proof

consider J being SetSequence of X such that
let n be Nat; :: thesis: for x being Subset of X ex y being Subset of X st S_{1}[n,x,y]

let x be Subset of X; :: thesis: ex y being Subset of X st S_{1}[n,x,y]

take y = Union (A ^\ (n + 1)); :: thesis: S_{1}[n,x,y]

thus S_{1}[n,x,y]
; :: thesis: verum

end;let x be Subset of X; :: thesis: ex y being Subset of X st S

take y = Union (A ^\ (n + 1)); :: thesis: S

thus S

A2: J . 0 = Union (A ^\ 0) and

A3: for n being Nat holds S

take J ; :: thesis: ( J . 0 = Union (A ^\ 0) & ( for n being Nat holds J . (n + 1) = Union (A ^\ (n + 1)) ) )

thus J . 0 = Union (A ^\ 0) by A2; :: thesis: for n being Nat holds J . (n + 1) = Union (A ^\ (n + 1))

let n be Nat; :: thesis: J . (n + 1) = Union (A ^\ (n + 1))

reconsider nn = n, nn1 = n + 1 as Element of NAT by ORDINAL1:def 12;

S

hence J . (n + 1) = Union (A ^\ (n + 1)) ; :: thesis: verum

A4: ( J . 0 = Union (A ^\ 0) & ( for n being Nat holds J . (n + 1) = Union (A ^\ (n + 1)) ) ) ;

A5: ( J . 0 = Union (A ^\ 0) & ( for n being Nat holds J . (n + 1) = Union (A ^\ (n + 1)) ) implies for n being Nat holds J . n = Union (A ^\ n) )

proof

take
J
; :: thesis: for n being Nat holds J . n = Union (A ^\ n)
assume A6:
( J . 0 = Union (A ^\ 0) & ( for n being Nat holds J . (n + 1) = Union (A ^\ (n + 1)) ) )
; :: thesis: for n being Nat holds J . n = Union (A ^\ n)

let n be Nat; :: thesis: J . n = Union (A ^\ n)

end;let n be Nat; :: thesis: J . n = Union (A ^\ n)

thus for n being Nat holds J . n = Union (A ^\ n) by A4, A5; :: thesis: verum

for n being Nat holds b