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)
proof
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)) ) )
proof
defpred S1[ 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 S1[n,x,y]
proof
let n be Nat; :: thesis: for x being Subset of X ex y being Subset of X st S1[n,x,y]
let x be Subset of X; :: thesis: ex y being Subset of X st S1[n,x,y]
take y = Union (A ^\ (n + 1)); :: thesis: S1[n,x,y]
thus S1[n,x,y] ; :: thesis: verum
end;
consider J being SetSequence of X such that
A2: J . 0 = Union (A ^\ 0) and
A3: for n being Nat holds S1[n,J . n,J . (n + 1)] from 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;
S1[n,J . nn,J . nn1] by A3;
hence J . (n + 1) = Union (A ^\ (n + 1)) ; :: thesis: verum
end;
then consider J being SetSequence of X such that
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
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)
per cases ( n = 0 or ex q being Nat st n = q + 1 ) by NAT_1:6;
suppose n = 0 ; :: thesis: J . n = Union (A ^\ n)
hence J . n = Union (A ^\ n) by A6; :: thesis: verum
end;
suppose ex q being Nat st n = q + 1 ; :: thesis: J . n = Union (A ^\ n)
then consider q being Nat such that
A7: n = q + 1 ;
reconsider q = q as Element of NAT by ORDINAL1:def 12;
J . (q + 1) = Union (A ^\ (q + 1)) by A6;
hence J . n = Union (A ^\ n) by A7; :: thesis: verum
end;
end;
end;
take J ; :: thesis: 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;
hence ex b1 being SetSequence of X st
for n being Nat holds b1 . n = Union (A ^\ n) ; :: thesis: verum