defpred S_{1}[ Nat, set , set ] means $3 = [:$2,(D . ($1 + 1)):];

A1: for n being Nat

for x being set ex y being set st S_{1}[n,x,y]
;

consider g being Function such that

A2: ( dom g = NAT & g . 0 = D . 0 & ( for n being Nat holds S_{1}[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

A1: for n being Nat

for x being set ex y being set st S

consider g being Function such that

A2: ( dom g = NAT & g . 0 = D . 0 & ( for n being Nat holds S

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