defpred S_{1}[ set , set , set ] means for x, y being Subset of X

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

y = (A1 . (s + 1)) \ ((Partial_Union A1) . s);

set A = A1 . 0;

A1: for n being Nat

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

A2: ( F . 0 = A1 . 0 & ( for n being Nat holds S_{1}[n,F . n,F . (n + 1)] ) )
from RECDEF_1:sch 2(A1);

for n being Nat holds F . (n + 1) = (A1 . (n + 1)) \ ((Partial_Union A1) . n)_{1} being SetSequence of X st

( b_{1} . 0 = A1 . 0 & ( for n being Nat holds b_{1} . (n + 1) = (A1 . (n + 1)) \ ((Partial_Union A1) . n) ) )
by A2; :: thesis: verum

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

y = (A1 . (s + 1)) \ ((Partial_Union A1) . s);

set A = A1 . 0;

A1: for n being Nat

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

proof

consider F 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 (A1 . (n + 1)) \ ((Partial_Union A1) . n) ; :: thesis: S_{1}[n,x,(A1 . (n + 1)) \ ((Partial_Union A1) . n)]

thus S_{1}[n,x,(A1 . (n + 1)) \ ((Partial_Union A1) . n)]
; :: thesis: verum

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

take (A1 . (n + 1)) \ ((Partial_Union A1) . n) ; :: thesis: S

thus S

A2: ( F . 0 = A1 . 0 & ( for n being Nat holds S

for n being Nat holds F . (n + 1) = (A1 . (n + 1)) \ ((Partial_Union A1) . n)

proof

hence
ex b
let n be Nat; :: thesis: F . (n + 1) = (A1 . (n + 1)) \ ((Partial_Union A1) . n)

reconsider n1 = n as Element of NAT by ORDINAL1:def 12;

for x, y being Subset of X

for s being Nat st s = n1 & x = F . n1 & y = F . (n1 + 1) holds

y = (A1 . (s + 1)) \ ((Partial_Union A1) . s) by A2;

hence F . (n + 1) = (A1 . (n + 1)) \ ((Partial_Union A1) . n) ; :: thesis: verum

end;reconsider n1 = n as Element of NAT by ORDINAL1:def 12;

for x, y being Subset of X

for s being Nat st s = n1 & x = F . n1 & y = F . (n1 + 1) holds

y = (A1 . (s + 1)) \ ((Partial_Union A1) . s) by A2;

hence F . (n + 1) = (A1 . (n + 1)) \ ((Partial_Union A1) . n) ; :: thesis: verum

( b