let Omega be non empty set ; :: thesis:
let Sigma be SigmaField of Omega; :: thesis:
let Prob be Probability of Sigma; :: thesis:
let n, n1, n2 be Nat; :: thesis:
A1: for A, B being SetSequence of Sigma st n > n1 & B = A * (Special_Function (n1,n2)) holds
(Partial_Product (Prob * B)) . n = ((Partial_Product (Prob * A)) . n1) * ((Partial_Product (Prob * (A ^\ ((n1 + n2) + 1)))) . ((n - n1) - 1))

let A, B be SetSequence of Sigma; :: thesis:
assume that
A2: n > n1 and
A3: B = A * (Special_Function (n1,n2)) ; :: thesis:
A4: for q being Element of NAT st q <= n1 holds
(Partial_Product (Prob * B)) . q = (Partial_Product (Prob * A)) . q

let q be Element of NAT ; :: thesis:
assume A5: q <= n1 ; :: thesis:
defpred S₁[ Nat] means (Partial_Product (Prob * B)) . ($1 * ((Special_Function3 n1) . $1)) = (Partial_Product (Prob * A)) . ($1 * ((Special_Function3 n1) . $1));
A6: S₁[ 0 ]

proof

A7: (Partial_Product (Prob * B)) . 0 = (Prob * B) . 0 by SERIES_3:def 1;
A8: (Partial_Product (Prob * A)) . 0 = (Prob * A) . 0 by SERIES_3:def 1;
dom (Prob * B) = NAT by FUNCT_2:def 1;
then A9: (Prob * B) . 0 = Prob . (B . 0) by FUNCT_1:12;
A10: dom (A * (Special_Function (n1,n2))) = NAT by FUNCT_2:def 1;
( (Special_Function (n1,n2)) . 0 = IFGT (0,n1,(0 + n2),0) & IFGT (0,n1,(0 + n2),0) = 0 ) by Def2, XXREAL_0:def 11;
then A11: (Prob * B) . 0 = Prob . (A . 0) by A10, A3, A9, FUNCT_1:12;
dom (Prob * A) = NAT by FUNCT_2:def 1;
hence S₁[ 0 ] by A11, A7, A8, FUNCT_1:12; :: thesis:

end;

A12: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis:
assume A13: S₁[k] ; :: thesis:

per cases ;

suppose A14: k < n1 ; :: thesis:

then A15: ( (Special_Function3 n1) . k = IFGT (k,n1,0,1) & IFGT (k,n1,0,1) = 1 ) by Def4, XXREAL_0:def 11;
V: k + 1 <= n1 by A14, NAT_1:13;
then A16: ( (Special_Function3 n1) . (k + 1) = IFGT ((k + 1),n1,0,1) & IFGT ((k + 1),n1,0,1) = 1 ) by Def4, XXREAL_0:def 11;
A17: (Prob * B) . (k + 1) = (Prob * A) . (k + 1)

proof

dom (Prob * B) = NAT by FUNCT_2:def 1;
then A18: (Prob * B) . (k + 1) = Prob . (B . (k + 1)) by FUNCT_1:12;
A19: dom (A * (Special_Function (n1,n2))) = NAT by FUNCT_2:def 1;
( (Special_Function (n1,n2)) . (k + 1) = IFGT ((k + 1),n1,((k + 1) + n2),(k + 1)) & IFGT ((k + 1),n1,((k + 1) + n2),(k + 1)) = k + 1 ) by Def2, XXREAL_0:def 11, V;
then A20: (Prob * B) . (k + 1) = Prob . (A . (k + 1)) by A19, A3, A18, FUNCT_1:12;
dom (Prob * A) = NAT by FUNCT_2:def 1;
hence (Prob * B) . (k + 1) = (Prob * A) . (k + 1) by A20, FUNCT_1:12; :: thesis:

end;

(Partial_Product (Prob * B)) . (k + 1) = ((Partial_Product (Prob * A)) . k) * ((Prob * A) . (k + 1)) by A15, A13, A17, SERIES_3:def 1;
hence S₁[k + 1] by A16, SERIES_3:def 1; :: thesis:

end;

suppose not k < n1 ; :: thesis:

then n1 < k + 1 by XREAL_1:145;
then A22: ( (Special_Function3 n1) . (k + 1) = IFGT ((k + 1),n1,0,1) & IFGT ((k + 1),n1,0,1) = 0 ) by Def4, XXREAL_0:def 11;
A23: (Prob * B) . 0 = (Prob * A) . 0

proof

dom (Prob * B) = NAT by FUNCT_2:def 1;
then A24: (Prob * B) . 0 = Prob . (B . 0) by FUNCT_1:12;
A25: dom (A * (Special_Function (n1,n2))) = NAT by FUNCT_2:def 1;
( (Special_Function (n1,n2)) . 0 = IFGT (0,n1,(0 + n2),0) & IFGT (0,n1,(0 + n2),0) = 0 ) by Def2, XXREAL_0:def 11;
then A26: (Prob * B) . 0 = Prob . (A . 0) by A25, A3, A24, FUNCT_1:12;
dom (Prob * A) = NAT by FUNCT_2:def 1;
hence (Prob * B) . 0 = (Prob * A) . 0 by A26, FUNCT_1:12; :: thesis:

end;

( (Partial_Product (Prob * B)) . ((k + 1) * ((Special_Function3 n1) . (k + 1))) = (Prob * B) . 0 & (Partial_Product (Prob * A)) . ((k + 1) * ((Special_Function3 n1) . (k + 1))) = (Prob * A) . 0 ) by A22, SERIES_3:def 1;
hence S₁[k + 1] by A23; :: thesis:

end;

A27: for k being Nat holds S₁[k] from NAT_1:sch 2(A6, A12);
(Partial_Product (Prob * B)) . q = (Partial_Product (Prob * A)) . q

proof

( (Special_Function3 n1) . q = IFGT (q,n1,0,1) & IFGT (q,n1,0,1) = 1 ) by Def4, A5, XXREAL_0:def 11;
then q * ((Special_Function3 n1) . q) = q ;
hence (Partial_Product (Prob * B)) . q = (Partial_Product (Prob * A)) . q by A27; :: thesis:

end;

hence (Partial_Product (Prob * B)) . q = (Partial_Product (Prob * A)) . q ; :: thesis:

end;

defpred S₁[ Nat] means (Partial_Product (Prob * B)) . (($1 + n1) + 1) = ((Partial_Product (Prob * A)) . n1) * ((Partial_Product (Prob * (A ^\ ((n1 + n2) + 1)))) . (((($1 + n1) + 1) - n1) - 1));
A28: n1 in NAT by ORDINAL1:def 12;
( (Partial_Product (Prob * B)) . ((0 + n1) + 1) = ((Partial_Product (Prob * B)) . n1) * ((Prob * B) . (n1 + 1)) & n1 <= n1 ) by SERIES_3:def 1;
then A29: (Partial_Product (Prob * B)) . ((0 + n1) + 1) = ((Partial_Product (Prob * A)) . n1) * ((Prob * B) . (n1 + 1)) by A4, A28;
A30: dom (A * (Special_Function (n1,n2))) = NAT by FUNCT_2:def 1;
n1 < n1 + 1 by NAT_1:13;
then ( (Special_Function (n1,n2)) . (n1 + 1) = IFGT ((n1 + 1),n1,((n1 + 1) + n2),(n1 + 1)) & IFGT ((n1 + 1),n1,((n1 + 1) + n2),(n1 + 1)) = (n1 + 1) + n2 ) by Def2, XXREAL_0:def 11;
then A32: Prob . (B . (n1 + 1)) = Prob . (A . ((n1 + 1) + n2)) by A30, A3, FUNCT_1:12;
A33: A . (((n1 + n2) + 1) + 0) = (A ^\ ((n1 + n2) + 1)) . 0 by NAT_1:def 3;
dom (Prob * (A ^\ ((n1 + n2) + 1))) = NAT by FUNCT_2:def 1;
then A34: Prob . (B . (n1 + 1)) = (Prob * (A ^\ ((n1 + n2) + 1))) . 0 by A33, A32, FUNCT_1:12;
dom (Prob * B) = NAT by FUNCT_2:def 1;
then (Prob * B) . (n1 + 1) = (Prob * (A ^\ ((n1 + n2) + 1))) . 0 by A34, FUNCT_1:12;
then A35: S₁[ 0 ] by A29, SERIES_3:def 1;
A36: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis:
assume A37: S₁[k] ; :: thesis:
A38: (Partial_Product (Prob * B)) . (((k + 1) + n1) + 1) = (((Partial_Product (Prob * A)) . n1) * ((Partial_Product (Prob * (A ^\ ((n1 + n2) + 1)))) . k)) * ((Prob * B) . (((k + 1) + n1) + 1)) by A37, SERIES_3:def 1;
A39: (Prob * B) . (((k + 1) + n1) + 1) = (Prob * (A ^\ ((n1 + n2) + 1))) . (k + 1)

proof

set j = ((k + 1) + n1) + 1;
A40: dom (A * (Special_Function (n1,n2))) = NAT by FUNCT_2:def 1;
n1 < n1 + ((k + 1) + 1) by NAT_1:19, XREAL_1:31;
then ( (Special_Function (n1,n2)) . (((k + 1) + n1) + 1) = IFGT ((((k + 1) + n1) + 1),n1,((((k + 1) + n1) + 1) + n2),(((k + 1) + n1) + 1)) & IFGT ((((k + 1) + n1) + 1),n1,((((k + 1) + n1) + 1) + n2),(((k + 1) + n1) + 1)) = (((k + 1) + n1) + 1) + n2 ) by Def2, XXREAL_0:def 11;
then B . (((k + 1) + n1) + 1) = A . (((n1 + n2) + 1) + (k + 1)) by A40, A3, FUNCT_1:12;
then A41: Prob . (B . (((k + 1) + n1) + 1)) = Prob . ((A ^\ ((n1 + n2) + 1)) . (k + 1)) by NAT_1:def 3;
dom (Prob * B) = NAT by FUNCT_2:def 1;
then A42: (Prob * B) . (((k + 1) + n1) + 1) = Prob . ((A ^\ ((n1 + n2) + 1)) . (k + 1)) by A41, FUNCT_1:12;
dom (Prob * (A ^\ ((n1 + n2) + 1))) = NAT by FUNCT_2:def 1;
hence (Prob * B) . (((k + 1) + n1) + 1) = (Prob * (A ^\ ((n1 + n2) + 1))) . (k + 1) by A42, FUNCT_1:12; :: thesis:

end;

((Partial_Product (Prob * (A ^\ ((n1 + n2) + 1)))) . k) * ((Prob * (A ^\ ((n1 + n2) + 1))) . (k + 1)) = (Partial_Product (Prob * (A ^\ ((n1 + n2) + 1)))) . (k + 1) by SERIES_3:def 1;
hence S₁[k + 1] by A39, A38; :: thesis:

end;

A43: for k being Nat holds S₁[k] from NAT_1:sch 2(A35, A36);
(n - n1) - 1 is Element of NAT

proof

n1 + 1 <= n by A2, NAT_1:13;
then (n1 + 1) - 1 <= n - 1 by XREAL_1:9;
then ( n1 <= n - 1 & n - 1 is Element of NAT ) by A2, NAT_1:20;
then (n - 1) - n1 is Element of NAT by NAT_1:21;
hence (n - n1) - 1 is Element of NAT ; :: thesis:

end;

then consider k being Element of NAT such that
A44: k = (n - n1) - 1 ;
(Partial_Product (Prob * B)) . n = ((Partial_Product (Prob * A)) . n1) * ((Partial_Product (Prob * (A ^\ ((n1 + n2) + 1)))) . ((((((n - n1) - 1) + n1) + 1) - n1) - 1)) by A43, A44;
hence (Partial_Product (Prob * B)) . n = ((Partial_Product (Prob * A)) . n1) * ((Partial_Product (Prob * (A ^\ ((n1 + n2) + 1)))) . ((n - n1) - 1)) ; :: thesis:

end;

for A, B, C being SetSequence of Sigma
for n1, n2, n being Nat
for e being sequence of NAT st n > n1 & C = A * e & B = C * (Special_Function (n1,n2)) holds
(Partial_Intersection B) . n = ((Partial_Intersection C) . n1) /\ ((Partial_Intersection (C ^\ ((n1 + n2) + 1))) . ((n - n1) - 1))

proof

let A, B, C be SetSequence of Sigma; :: thesis:
let n1, n2, n be Nat; :: thesis:
let e be sequence of NAT; :: thesis:
assume A45: n > n1 ; :: thesis:
assume C = A * e ; :: thesis:
assume A46: B = C * (Special_Function (n1,n2)) ; :: thesis:
reconsider B = B as SetSequence of Sigma ;
A47: (Partial_Intersection B) . n1 = (Partial_Intersection C) . n1

proof

for x being object holds
( x in (Partial_Intersection B) . n1 iff x in (Partial_Intersection C) . n1 )

proof

let x be object ; :: thesis:

hereby :: thesis:

assume A48: x in (Partial_Intersection B) . n1 ; :: thesis:
x in (Partial_Intersection C) . n1

proof

for knat being Nat st knat <= n1 holds
x in C . knat

proof

let knat be Nat; :: thesis:
assume A50: knat <= n1 ; :: thesis:
reconsider knat = knat as Element of NAT by ORDINAL1:def 12;
A51: x in B . knat by A50, A48, PROB_3:25;
A52: dom (C * (Special_Function (n1,n2))) = NAT by FUNCT_2:def 1;
( (Special_Function (n1,n2)) . knat = IFGT (knat,n1,(knat + n2),knat) & IFGT (knat,n1,(knat + n2),knat) = knat ) by Def2, A50, XXREAL_0:def 11;
hence x in C . knat by A52, A46, A51, FUNCT_1:12; :: thesis:

end;

hence x in (Partial_Intersection C) . n1 by PROB_3:25; :: thesis:

end;

hence x in (Partial_Intersection C) . n1 ; :: thesis:

end;

assume A53: x in (Partial_Intersection C) . n1 ; :: thesis:
x in (Partial_Intersection B) . n1

proof

for knat being Nat st knat <= n1 holds
x in B . knat

proof

let knat be Nat; :: thesis:
assume A54: knat <= n1 ; :: thesis:
reconsider knat = knat as Element of NAT by ORDINAL1:def 12;
A55: x in C . knat by A53, A54, PROB_3:25;
A56: dom (C * (Special_Function (n1,n2))) = NAT by FUNCT_2:def 1;
( (Special_Function (n1,n2)) . knat = IFGT (knat,n1,(knat + n2),knat) & IFGT (knat,n1,(knat + n2),knat) = knat ) by Def2, A54, XXREAL_0:def 11;
hence x in B . knat by A56, A46, A55, FUNCT_1:12; :: thesis:

end;

hence x in (Partial_Intersection B) . n1 by PROB_3:25; :: thesis:

end;

hence x in (Partial_Intersection B) . n1 ; :: thesis:

end;

hence (Partial_Intersection B) . n1 = (Partial_Intersection C) . n1 by TARSKI:2; :: thesis:

end;

A57: for x being set st ( for knat being Nat st knat <= n holds
x in B . knat ) holds
( ( for knat being Nat st knat <= n1 holds
x in B . knat ) & ( for knat being Nat st n1 < knat & knat <= n holds
x in B . knat ) ) by A45, XXREAL_0:2;
A58: for x being object st x in (Partial_Intersection (C ^\ ((n1 + n2) + 1))) . ((n - n1) - 1) holds
for qnat being Nat st n1 < qnat & qnat <= n holds
x in B . qnat

proof

let x be object ; :: thesis:
assume A59: x in (Partial_Intersection (C ^\ ((n1 + n2) + 1))) . ((n - n1) - 1) ; :: thesis:
A60: ( (n - n1) - 1 >= 0 & (n - n1) - 1 is Element of NAT )

proof

n - n1 is Element of NAT by A45, NAT_1:21;
hence ( (n - n1) - 1 >= 0 & (n - n1) - 1 is Element of NAT ) by A45, NAT_1:20, XREAL_1:50; :: thesis:

end;

A61: for knat being Nat st knat <= (n - n1) - 1 holds
x in C . (knat + ((n1 + n2) + 1))

proof

let knat be Nat; :: thesis:
assume knat <= (n - n1) - 1 ; :: thesis:
then x in (C ^\ ((n1 + n2) + 1)) . knat by A60, A59, PROB_3:25;
hence x in C . (knat + ((n1 + n2) + 1)) by NAT_1:def 3; :: thesis:

end;

for qnat being Nat st n1 < qnat & qnat <= n holds
x in B . qnat

proof

let qnat be Nat; :: thesis:
assume that
A62: n1 < qnat and
A63: qnat <= n ; :: thesis:
( n1 + 1 <= qnat & qnat <= n ) by A62, A63, NAT_1:13;
then qnat - (n1 + 1) is Element of NAT by NAT_1:21;
then consider knat being Nat such that
A66: knat = (qnat - n1) - 1 ;
A67: (qnat - n1) - 1 <= (n - n1) - 1

proof

qnat - (n1 + 1) <= n - (n1 + 1) by A63, XREAL_1:9;
hence (qnat - n1) - 1 <= (n - n1) - 1 ; :: thesis:

end;

A68: x in C . (knat + ((n1 + n2) + 1)) by A66, A67, A61;
x in B . qnat

proof

reconsider qnat = qnat as Element of NAT by ORDINAL1:def 12;
A69: dom (C * (Special_Function (n1,n2))) = NAT by FUNCT_2:def 1;
( (Special_Function (n1,n2)) . qnat = IFGT (qnat,n1,(qnat + n2),qnat) & IFGT (qnat,n1,(qnat + n2),qnat) = qnat + n2 ) by Def2, A62, XXREAL_0:def 11;
hence x in B . qnat by A69, A46, A66, A68, FUNCT_1:12; :: thesis:

end;

hence x in B . qnat ; :: thesis:

end;

hence for qnat being Nat st n1 < qnat & qnat <= n holds
x in B . qnat ; :: thesis:

end;

A70: for x being object st ( for qnat being Nat st n1 < qnat & qnat <= n holds
x in B . qnat ) holds
x in (Partial_Intersection (C ^\ ((n1 + n2) + 1))) . ((n - n1) - 1)

proof

let x be object ; :: thesis:
assume A71: for qnat being Nat st n1 < qnat & qnat <= n holds
x in B . qnat ; :: thesis:
A72: ( (n - n1) - 1 >= 0 & (n - n1) - 1 is Element of NAT )

proof

n - n1 is Element of NAT by A45, NAT_1:21;
hence ( (n - n1) - 1 >= 0 & (n - n1) - 1 is Element of NAT ) by A45, NAT_1:20, XREAL_1:50; :: thesis:

end;

x in (Partial_Intersection (C ^\ ((n1 + n2) + 1))) . ((n - n1) - 1)

proof

A73: for qnat being Nat st 0 <= (qnat - n1) - 1 & (qnat - n1) - 1 <= (n - n1) - 1 holds
x in B . qnat

proof

let qnat be Nat; :: thesis:
assume that
A74: 0 <= (qnat - n1) - 1 and
A75: (qnat - n1) - 1 <= (n - n1) - 1 ; :: thesis:
0 + (n1 + 1) <= (qnat - (n1 + 1)) + (n1 + 1) by A74, XREAL_1:6;
then (n1 + 1) - 1 <= qnat - 1 by XREAL_1:9;
then ( n1 <= qnat - 1 & qnat < qnat + 1 ) by NAT_1:13;
then ( n1 <= qnat - 1 & qnat - 1 < (qnat + 1) - 1 ) by XREAL_1:9;
then A76: n1 < qnat by XXREAL_0:2;
(qnat - (n1 + 1)) + (n1 + 1) <= (n - (n1 + 1)) + (n1 + 1) by A75, XREAL_1:6;
hence x in B . qnat by A76, A71; :: thesis:

end;

for knat being Nat st 0 <= knat & knat <= (n - n1) - 1 holds
x in (C ^\ ((n1 + n2) + 1)) . knat

proof

let knat be Nat; :: thesis:
assume that
0 <= knat and
A77: knat <= (n - n1) - 1 ; :: thesis:
set qnat = (knat + n1) + 1;
(((knat + n1) + 1) - n1) - 1 <= (n - n1) - 1 by A77;
then A79: x in B . ((knat + n1) + 1) by A73;
A80: dom (C * (Special_Function (n1,n2))) = NAT by FUNCT_2:def 1;
n1 < (knat + n1) + 1 by NAT_1:13, XREAL_1:31;
then ( (Special_Function (n1,n2)) . ((knat + n1) + 1) = IFGT (((knat + n1) + 1),n1,(((knat + n1) + 1) + n2),((knat + n1) + 1)) & IFGT (((knat + n1) + 1),n1,(((knat + n1) + 1) + n2),((knat + n1) + 1)) = ((knat + n1) + 1) + n2 ) by Def2, XXREAL_0:def 11;
then B . ((knat + n1) + 1) = C . (((n1 + n2) + 1) + knat) by A46, A80, FUNCT_1:12;
hence x in (C ^\ ((n1 + n2) + 1)) . knat by A79, NAT_1:def 3; :: thesis:

end;

then for knat being Nat st knat <= (n - n1) - 1 holds
x in (C ^\ ((n1 + n2) + 1)) . knat ;
hence x in (Partial_Intersection (C ^\ ((n1 + n2) + 1))) . ((n - n1) - 1) by A72, PROB_3:25; :: thesis:

end;

hence x in (Partial_Intersection (C ^\ ((n1 + n2) + 1))) . ((n - n1) - 1) ; :: thesis:

end;

A82: for x being set holds
( x in (Partial_Intersection B) . n iff ( ( for knat being Nat st knat <= n1 holds
x in B . knat ) & ( for knat being Nat st n1 < knat & knat <= n holds
x in B . knat ) ) )

proof

let x be set ; :: thesis:
( x in (Partial_Intersection B) . n iff for knat being Nat st knat <= n holds
x in B . knat ) by PROB_3:25;
hence ( x in (Partial_Intersection B) . n iff ( ( for knat being Nat st knat <= n1 holds
x in B . knat ) & ( for knat being Nat st n1 < knat & knat <= n holds
x in B . knat ) ) ) by A57; :: thesis:

end;

A83: for x being set holds
( x in (Partial_Intersection B) . n iff ( x in (Partial_Intersection B) . n1 & ( for knat being Nat st n1 < knat & knat <= n holds
x in B . knat ) ) )

proof

let x be set ; :: thesis:
( x in (Partial_Intersection B) . n1 iff for knat being Nat st knat <= n1 holds
x in B . knat ) by PROB_3:25;
hence ( x in (Partial_Intersection B) . n iff ( x in (Partial_Intersection B) . n1 & ( for knat being Nat st n1 < knat & knat <= n holds
x in B . knat ) ) ) by A82; :: thesis:

end;

for x being object holds
( x in (Partial_Intersection B) . n iff ( x in (Partial_Intersection B) . n1 & x in (Partial_Intersection (C ^\ ((n1 + n2) + 1))) . ((n - n1) - 1) ) )

proof

let x be object ; :: thesis:
( x in (Partial_Intersection (C ^\ ((n1 + n2) + 1))) . ((n - n1) - 1) iff for knat being Nat st n1 < knat & knat <= n holds
x in B . knat ) by A58, A70;
hence ( x in (Partial_Intersection B) . n iff ( x in (Partial_Intersection B) . n1 & x in (Partial_Intersection (C ^\ ((n1 + n2) + 1))) . ((n - n1) - 1) ) ) by A83; :: thesis:

end;

hence (Partial_Intersection B) . n = ((Partial_Intersection C) . n1) /\ ((Partial_Intersection (C ^\ ((n1 + n2) + 1))) . ((n - n1) - 1)) by A47, XBOOLE_0:def 4; :: thesis:

end;

hence ( ( for A, B being SetSequence of Sigma st n > n1 & B = A * (Special_Function (n1,n2)) holds
(Partial_Product (Prob * B)) . n = ((Partial_Product (Prob * A)) . n1) * ((Partial_Product (Prob * (A ^\ ((n1 + n2) + 1)))) . ((n - n1) - 1)) ) & ( for A, B, C being SetSequence of Sigma
for e being sequence of NAT st n > n1 & C = A * e & B = C * (Special_Function (n1,n2)) holds
(Partial_Intersection B) . n = ((Partial_Intersection C) . n1) /\ ((Partial_Intersection (C ^\ ((n1 + n2) + 1))) . ((n - n1) - 1)) ) ) by A1; :: thesis: