defpred S₁[ 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₁[n,x,y] ;
consider g being Function such that
A2: ( dom g = NAT & g . 0 = P . 0 & ( for n being Nat holds S₁[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