defpred S_{1}[ Nat, set , set ] means $3 = Product-Probability (((Product_dom D) . $1),(D . ($1 + 1)),(modetrans ($2,(Trivial-SigmaField ((Product_dom D) . $1)))),(P . ($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 = P . 0 & ( for n being Nat holds S_{1}[n,g . n,g . (n + 1)] ) )
from RECDEF_1:sch 1(A1);

reconsider g = g as NAT -defined Function by RELAT_1:def 18, A2;

reconsider g = g as ManySortedSet of NAT by PARTFUN1:def 2, A2;

take g ; :: thesis: ( g . 0 = P . 0 & ( for i being Nat holds g . (i + 1) = Product-Probability (((Product_dom D) . i),(D . (i + 1)),(modetrans ((g . i),(Trivial-SigmaField ((Product_dom D) . i)))),(P . (i + 1))) ) )

thus g . 0 = P . 0 by A2; :: thesis: for i being Nat holds g . (i + 1) = Product-Probability (((Product_dom D) . i),(D . (i + 1)),(modetrans ((g . i),(Trivial-SigmaField ((Product_dom D) . i)))),(P . (i + 1)))

thus for i being Nat holds g . (i + 1) = Product-Probability (((Product_dom D) . i),(D . (i + 1)),(modetrans ((g . i),(Trivial-SigmaField ((Product_dom D) . i)))),(P . (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 = P . 0 & ( for n being Nat holds S

reconsider g = g as NAT -defined Function by RELAT_1:def 18, A2;

reconsider g = g as ManySortedSet of NAT by PARTFUN1:def 2, A2;

take g ; :: thesis: ( g . 0 = P . 0 & ( for i being Nat holds g . (i + 1) = Product-Probability (((Product_dom D) . i),(D . (i + 1)),(modetrans ((g . i),(Trivial-SigmaField ((Product_dom D) . i)))),(P . (i + 1))) ) )

thus g . 0 = P . 0 by A2; :: thesis: for i being Nat holds g . (i + 1) = Product-Probability (((Product_dom D) . i),(D . (i + 1)),(modetrans ((g . i),(Trivial-SigmaField ((Product_dom D) . i)))),(P . (i + 1)))

thus for i being Nat holds g . (i + 1) = Product-Probability (((Product_dom D) . i),(D . (i + 1)),(modetrans ((g . i),(Trivial-SigmaField ((Product_dom D) . i)))),(P . (i + 1))) by A2; :: thesis: verum