let X be set ; :: thesis: for A1 being SetSequence of X ex A2 being SetSequence of X st
( A2 . 0 = A1 . 0 & ( for n being Nat holds A2 . (n + 1) = (A1 . (n + 1)) \ ((Partial_Union A1) . n) ) )
let A1 be SetSequence of X; :: thesis: ex A2 being SetSequence of X st
( A2 . 0 = A1 . 0 & ( for n being Nat holds A2 . (n + 1) = (A1 . (n + 1)) \ ((Partial_Union A1) . n) ) )
defpred S₁[ 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);
A1: for n being Element of NAT
for x being Subset of X ex y being Subset of X st S₁[n,x,y]

proof

let n be Element of NAT ; :: thesis: for x being Subset of X ex y being Subset of X st S₁[n,x,y]
let x be Subset of X; :: thesis: ex y being Subset of X st S₁[n,x,y]
take y = (A1 . (n + 1)) \ ((Partial_Union A1) . n); :: thesis: S₁[n,x,y]
thus S₁[n,x,y] ; :: thesis: verum

end;

set A = A1 . 0 ;
consider F being SetSequence of X such that
A2: ( F . 0 = A1 . 0 & ( for n being Element of NAT holds S₁[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)

proof

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 13;
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;

hence ex A2 being SetSequence of X st
( A2 . 0 = A1 . 0 & ( for n being Nat holds A2 . (n + 1) = (A1 . (n + 1)) \ ((Partial_Union A1) . n) ) ) by A2; :: thesis: verum