defpred S₁[ Nat, set , set ] means $3 = [:$2,(D . ($1 + 1)):];
A1: for n being Nat
for x being set ex y being set st S₁[n,x,y] ;
consider g being Function such that
A2: ( dom g = NAT & g . 0 = D . 0 & ( for n being Nat holds S₁[n,g . n,g . (n + 1)] ) ) from RECDEF_1:sch 1(A1);
reconsider g = g as ManySortedSet of NAT by PARTFUN1:def 2, RELAT_1:def 18, A2;
take g ; :: thesis: ( g . 0 = D . 0 & ( for i being Nat holds g . (i + 1) = [:(g . i),(D . (i + 1)):] ) )
thus ( g . 0 = D . 0 & ( for i being Nat holds g . (i + 1) = [:(g . i),(D . (i + 1)):] ) ) by A2; :: thesis: verum