defpred S₁[ set , set , set ] means $3 = $2 \/ { ((Den (o,A)) . p) where o is Element of dom the charact of A, p is Element of the carrier of A * : ( p in dom (Den (o,A)) & rng p c= $2 ) } ;
A1: for n being Nat
for B1 being Subset of A ex B2 being Subset of A st S₁[n,B1,B2]

proof

let n be Nat; :: thesis: for B1 being Subset of A ex B2 being Subset of A st S₁[n,B1,B2]
let B1 be Subset of A; :: thesis: ex B2 being Subset of A st S₁[n,B1,B2]
set B2 = B1 \/ { ((Den (o,A)) . p) where o is Element of dom the charact of A, p is Element of the carrier of A * : ( p in dom (Den (o,A)) & rng p c= B1 ) } ;
B1 \/ { ((Den (o,A)) . p) where o is Element of dom the charact of A, p is Element of the carrier of A * : ( p in dom (Den (o,A)) & rng p c= B1 ) } c= the carrier of A

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( x nin B1 \/ { ((Den (o,A)) . p) where o is Element of dom the charact of A, p is Element of the carrier of A * : ( p in dom (Den (o,A)) & rng p c= B1 ) } or not x nin the carrier of A )
assume that
A2: x in B1 \/ { ((Den (o,A)) . p) where o is Element of dom the charact of A, p is Element of the carrier of A * : ( p in dom (Den (o,A)) & rng p c= B1 ) } and
A3: not x in the carrier of A ; :: thesis: contradiction
( x in B1 implies x in the carrier of A ) ;
then x in { ((Den (o,A)) . p) where o is Element of dom the charact of A, p is Element of the carrier of A * : ( p in dom (Den (o,A)) & rng p c= B1 ) } by A2, A3, XBOOLE_0:def 3;
then consider o being Element of dom the charact of A, p being Element of the carrier of A * such that
A4: x = (Den (o,A)) . p and
A5: p in dom (Den (o,A)) and
rng p c= B1 ;
x in rng (Den (o,A)) by A4, A5, FUNCT_1:def 3;
hence contradiction by A3; :: thesis: verum

end;

then reconsider B2 = B1 \/ { ((Den (o,A)) . p) where o is Element of dom the charact of A, p is Element of the carrier of A * : ( p in dom (Den (o,A)) & rng p c= B1 ) } as Subset of A ;
take B2 ; :: thesis: S₁[n,B1,B2]
thus S₁[n,B1,B2] ; :: thesis: verum

end;

consider F being sequence of (bool the carrier of A) such that
A6: ( F . 0 = B & ( for n being Nat holds S₁[n,F . n,F . (n + 1)] ) ) from RECDEF_1:sch 2(A1);
reconsider n9 = n as Element of NAT by ORDINAL1:def 12;
take a = F . n9; :: thesis: ex F being sequence of (bool the carrier of A) st
( a = F . n & F . 0 = B & ( for n being Nat holds F . (n + 1) = (F . n) \/ { ((Den (o,A)) . p) where o is Element of dom the charact of A, p is Element of the carrier of A * : ( p in dom (Den (o,A)) & rng p c= F . n ) } ) )
take F ; :: thesis: ( a = F . n & F . 0 = B & ( for n being Nat holds F . (n + 1) = (F . n) \/ { ((Den (o,A)) . p) where o is Element of dom the charact of A, p is Element of the carrier of A * : ( p in dom (Den (o,A)) & rng p c= F . n ) } ) )
thus ( a = F . n & F . 0 = B ) by A6; :: thesis: for n being Nat holds F . (n + 1) = (F . n) \/ { ((Den (o,A)) . p) where o is Element of dom the charact of A, p is Element of the carrier of A * : ( p in dom (Den (o,A)) & rng p c= F . n ) }
let n be Nat; :: thesis: F . (n + 1) = (F . n) \/ { ((Den (o,A)) . p) where o is Element of dom the charact of A, p is Element of the carrier of A * : ( p in dom (Den (o,A)) & rng p c= F . n ) }
thus F . (n + 1) = (F . n) \/ { ((Den (o,A)) . p) where o is Element of dom the charact of A, p is Element of the carrier of A * : ( p in dom (Den (o,A)) & rng p c= F . n ) } by A6; :: thesis: verum