let Omega be non empty set ; :: thesis:
let Sigma be SigmaField of Omega; :: thesis:
let Prob be Probability of Sigma; :: thesis:
let A be SetSequence of Sigma; :: thesis:
let n, n1, n2 be Element of NAT ; :: thesis:
assume that
A1: n > n1 and
A2: A is_all_independent_wrt Prob ; :: thesis:
A3: for A, B being SetSequence of Sigma
for k, n being Element of NAT st B = A * (Special_Function2 k) holds
(Partial_Product (Prob * (A ^\ k))) . n = (Partial_Product (Prob * B)) . n

let A, B be SetSequence of Sigma; :: thesis:
let k, n be Element of NAT ; :: thesis:
assume A4: B = A * (Special_Function2 k) ; :: thesis:
defpred S₁[ Element of NAT ] means (Partial_Product (Prob * (A ^\ k))) . $1 = (Partial_Product (Prob * B)) . $1;
dom (Prob * (A ^\ k)) = NAT by FUNCT_2:def 1;
then A5: (Prob * (A ^\ k)) . 0 = Prob . ((A ^\ k) . 0) by FUNCT_1:12;
(Prob * (A ^\ k)) . 0 = Prob . (A . (0 + k)) by A5, NAT_1:def 3;
then A6: (Partial_Product (Prob * (A ^\ k))) . 0 = Prob . (A . k) by SERIES_3:def 1;
A7: (Partial_Product (Prob * B)) . 0 = (Prob * B) . 0 by SERIES_3:def 1;
A8: (Special_Function2 k) . 0 = 0 + k by Def3;
dom (A * (Special_Function2 k)) = NAT by FUNCT_2:def 1;
then A9: Prob . (B . 0) = Prob . (A . k) by A8, A4, FUNCT_1:12;
dom (Prob * B) = NAT by FUNCT_2:def 1;
then A10: S₁[ 0 ] by A9, A7, A6, FUNCT_1:12;
A11: for q being Element of NAT st S₁[q] holds
S₁[q + 1]

let q be Element of NAT ; :: thesis:
assume A12: S₁[q] ; :: thesis:
A13: (Partial_Product (Prob * (A ^\ k))) . (q + 1) = ((Partial_Product (Prob * B)) . q) * ((Prob * (A ^\ k)) . (q + 1)) by A12, SERIES_3:def 1;
(Prob * (A ^\ k)) . (q + 1) = (Prob * B) . (q + 1)

proof

dom (Prob * (A ^\ k)) = NAT by FUNCT_2:def 1;
then A14: (Prob * (A ^\ k)) . (q + 1) = Prob . ((A ^\ k) . (q + 1)) by FUNCT_1:12;
dom (Prob * B) = NAT by FUNCT_2:def 1;
then A15: (Prob * B) . (q + 1) = Prob . (B . (q + 1)) by FUNCT_1:12;
dom (A * (Special_Function2 k)) = NAT by FUNCT_2:def 1;
then A16: B . (q + 1) = A . ((Special_Function2 k) . (q + 1)) by A4, FUNCT_1:12;
( (Special_Function2 k) . (q + 1) = (q + 1) + k & (q + 1) + k = (q + 1) + k ) by Def3;
hence (Prob * (A ^\ k)) . (q + 1) = (Prob * B) . (q + 1) by A16, A15, A14, NAT_1:def 3; :: thesis:

end;

hence S₁[q + 1] by A13, SERIES_3:def 1; :: thesis:

end;

for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A10, A11);
hence (Partial_Product (Prob * (A ^\ k))) . n = (Partial_Product (Prob * B)) . n ; :: thesis:

end;

A17: for m, m1, m2 being Element of NAT
for e being sequence of NAT
for C, B being SetSequence of Sigma st m1 < m & e is one-to-one & C = A * e & B = C * (Special_Function (m1,m2)) holds
Prob . ((Partial_Intersection B) . m) = ((Partial_Product (Prob * C)) . m1) * ((Partial_Product (Prob * (C ^\ ((m1 + m2) + 1)))) . ((m - m1) - 1))

proof

let m, m1, m2 be Element of NAT ; :: thesis:
let e be sequence of NAT; :: thesis:
let C, B be SetSequence of Sigma; :: thesis:
assume that
A18: m1 < m and
A19: e is one-to-one and
A20: C = A * e and
A21: B = C * (Special_Function (m1,m2)) ; :: thesis:
( B is SetSequence of Sigma & e * (Special_Function (m1,m2)) is sequence of NAT & e * (Special_Function (m1,m2)) is one-to-one & ( for n being Element of NAT holds A . ((e * (Special_Function (m1,m2))) . n) = B . n ) )

proof

for n being Element of NAT holds A . ((e * (Special_Function (m1,m2))) . n) = B . n

proof

let n be Element of NAT ; :: thesis:
A22: dom ((A * e) * (Special_Function (m1,m2))) = NAT by FUNCT_2:def 1;
A23: B . n = (A * e) . ((Special_Function (m1,m2)) . n) by A21, A20, A22, FUNCT_1:12;
dom (A * e) = NAT by FUNCT_2:def 1;
then A24: B . n = A . (e . ((Special_Function (m1,m2)) . n)) by A23, FUNCT_1:12;
dom (e * (Special_Function (m1,m2))) = NAT by FUNCT_2:def 1;
hence A . ((e * (Special_Function (m1,m2))) . n) = B . n by A24, FUNCT_1:12; :: thesis:

end;

hence ( B is SetSequence of Sigma & e * (Special_Function (m1,m2)) is sequence of NAT & e * (Special_Function (m1,m2)) is one-to-one & ( for n being Element of NAT holds A . ((e * (Special_Function (m1,m2))) . n) = B . n ) ) by A19, FUNCT_1:24; :: thesis:

end;

then Prob . ((Partial_Intersection B) . m) = (Partial_Product (Prob * B)) . m by A2, Def8;
hence Prob . ((Partial_Intersection B) . m) = ((Partial_Product (Prob * C)) . m1) * ((Partial_Product (Prob * (C ^\ ((m1 + m2) + 1)))) . ((m - m1) - 1)) by A18, A21, Th5; :: thesis:

end;

A25: for m, m1 being Element of NAT
for e being sequence of NAT
for C, B being SetSequence of Sigma st C = A * e & e is one-to-one & B = C * (Special_Function2 m1) holds
Prob . ((Partial_Intersection B) . m) = (Partial_Product (Prob * (C ^\ m1))) . m

proof

let m, m1 be Element of NAT ; :: thesis:
let e be sequence of NAT; :: thesis:
let C, B be SetSequence of Sigma; :: thesis:
assume that
A26: C = A * e and
A27: e is one-to-one and
A28: B = C * (Special_Function2 m1) ; :: thesis:
A29: ( B is SetSequence of Sigma & Special_Function2 m1 is sequence of NAT & dom (e * (Special_Function2 m1)) <> {} & e * (Special_Function2 m1) is one-to-one & ( for n being Element of NAT holds A . ((e * (Special_Function2 m1)) . n) = B . n ) )

proof

A30: for n being Element of NAT holds A . ((e * (Special_Function2 m1)) . n) = B . n

proof

let n be Element of NAT ; :: thesis:
dom (A * (e * (Special_Function2 m1))) = NAT by FUNCT_2:def 1;
then A31: (A * (e * (Special_Function2 m1))) . n = A . ((e * (Special_Function2 m1)) . n) by FUNCT_1:12;
dom (A * e) = NAT by FUNCT_2:def 1;
then A32: (A * e) . ((Special_Function2 m1) . n) = A . (e . ((Special_Function2 m1) . n)) by FUNCT_1:12;
dom (e * (Special_Function2 m1)) = NAT by FUNCT_2:def 1;
then A33: (A * e) . ((Special_Function2 m1) . n) = (A * (e * (Special_Function2 m1))) . n by A32, A31, FUNCT_1:12;
dom ((A * e) * (Special_Function2 m1)) = NAT by FUNCT_2:def 1;
then A34: B . n = (A * (e * (Special_Function2 m1))) . n by A33, A28, A26, FUNCT_1:12;
dom (A * (e * (Special_Function2 m1))) = NAT by FUNCT_2:def 1;
hence A . ((e * (Special_Function2 m1)) . n) = B . n by A34, FUNCT_1:12; :: thesis:

end;

thus ( B is SetSequence of Sigma & Special_Function2 m1 is sequence of NAT & dom (e * (Special_Function2 m1)) <> {} & e * (Special_Function2 m1) is one-to-one & ( for n being Element of NAT holds A . ((e * (Special_Function2 m1)) . n) = B . n ) ) by A27, A30, FUNCT_1:24; :: thesis:

end;

Prob . ((Partial_Intersection B) . m) = (Partial_Product (Prob * B)) . m by A2, A29, Def8;
hence Prob . ((Partial_Intersection B) . m) = (Partial_Product (Prob * (C ^\ m1))) . m by A28, A3; :: thesis:

end;

A35: for q being Element of NAT holds Prob . (((Partial_Intersection (Complement A)) . n1) /\ ((Partial_Intersection (A ^\ ((n1 + n2) + 1))) . q)) = ((Partial_Product (Prob * (Complement A))) . n1) * ((Partial_Product (Prob * (A ^\ ((n1 + n2) + 1)))) . q)

proof

let q be Element of NAT ; :: thesis:
defpred S₁[ Element of NAT ] means for e being sequence of NAT
for q, n2 being Element of NAT
for C being SetSequence of Sigma st e is one-to-one & C = A * e holds
Prob . (((Partial_Intersection (Complement C)) . $1) /\ ((Partial_Intersection (C ^\ (($1 + n2) + 1))) . q)) = ((Partial_Product (Prob * (Complement C))) . $1) * ((Partial_Product (Prob * (C ^\ (($1 + n2) + 1)))) . q);
A36: S₁[ 0 ]

proof

proof

( m1 < m1 + 1 & m1 + 1 <= (m1 + 1) + q ) by NAT_1:13, XREAL_1:31;
hence ( m1 < m & C = A * e & B = C * (Special_Function (m1,m2)) ) by A43, A38, A45, XXREAL_0:2; :: thesis:

end;

proof

( C . 0 = ((C . 0) `) ` & ((C . 0) `) ` = Omega \ ((C . 0) `) ) by SUBSET_1:def 4;
then ( Prob . (C . 0) = Prob . (([#] Sigma) \ ((C . 0) `)) & (C . 0) ` is Event of Sigma ) by PROB_1:20;
then A48: Prob . (C . 0) = 1 - (Prob . ((C . 0) `)) by PROB_1:32;
dom (Prob * C) = NAT by FUNCT_2:def 1;
then A49: (Prob * C) . 0 = 1 - (Prob . ((C . 0) `)) by A48, FUNCT_1:12;
dom (Prob * (Complement C)) = NAT by FUNCT_2:def 1;
then (Prob * (Complement C)) . 0 = Prob . ((Complement C) . 0) by FUNCT_1:12;
hence (Prob * C) . 0 = 1 - ((Prob * (Complement C)) . 0) by A49, PROB_1:def 2; :: thesis:

end;

then A50: Prob . (((Partial_Intersection (Complement C)) . 0) /\ ((Partial_Intersection (C ^\ ((0 + n2) + 1))) . q)) = (Prob . ((Partial_Intersection (C ^\ ((0 + n2) + 1))) . q)) - (((Partial_Product (Prob * (C ^\ ((0 + n2) + 1)))) . q) - (((Prob * (Complement C)) . 0) * ((Partial_Product (Prob * (C ^\ ((0 + n2) + 1)))) . q))) by A47;
set m1 = (0 + n2) + 1;
set m = q;
set B = C * (Special_Function2 ((0 + n2) + 1));
reconsider B = C * (Special_Function2 ((0 + n2) + 1)) as SetSequence of Sigma ;
A51: for A, B, C being SetSequence of Sigma
for k, n being Element of NAT
for e being sequence of NAT st C = A * e & B = C * (Special_Function2 k) holds
(Partial_Intersection (C ^\ k)) . n = (Partial_Intersection B) . n

proof

let A, B, C be SetSequence of Sigma; :: thesis:
let k, n be Element of NAT ; :: thesis:
let e be sequence of NAT; :: thesis:
assume C = A * e ; :: thesis:
assume A52: B = C * (Special_Function2 k) ; :: thesis:
A53: for x being set holds
( ( for knat being Nat st knat <= n holds
x in (C ^\ k) . knat ) iff for knat being Nat st knat <= n holds
x in B . knat )

proof

let x be set ; :: thesis:

hereby :: thesis:

assume A54: for knat being Nat st knat <= n holds
x in (C ^\ k) . knat ; :: thesis:
thus for knat being Nat st knat <= n holds
x in B . knat :: thesis:

proof

let knat be Nat; :: thesis:
assume A55: knat <= n ; :: thesis:
reconsider knat = knat as Element of NAT by ORDINAL1:def 12;
dom (C * (Special_Function2 k)) = NAT by FUNCT_2:def 1;
then A56: (C * (Special_Function2 k)) . knat = C . ((Special_Function2 k) . knat) by FUNCT_1:12;
( (Special_Function2 k) . knat = knat + k & knat + k = knat + k ) by Def3;
then ( x in B . knat iff x in (C ^\ k) . knat ) by A52, A56, NAT_1:def 3;
hence x in B . knat by A55, A54; :: thesis:

end;

assume A57: for knat being Nat st knat <= n holds
x in B . knat ; :: thesis:
thus for knat being Nat st knat <= n holds
x in (C ^\ k) . knat :: thesis:

proof

let knat be Nat; :: thesis:
assume A58: knat <= n ; :: thesis:
reconsider knat = knat as Element of NAT by ORDINAL1:def 12;
dom (C * (Special_Function2 k)) = NAT by FUNCT_2:def 1;
then A59: (C * (Special_Function2 k)) . knat = C . ((Special_Function2 k) . knat) by FUNCT_1:12;
( (Special_Function2 k) . knat = knat + k & knat + k = knat + k ) by Def3;
then ( x in B . knat iff x in (C ^\ k) . knat ) by A52, A59, NAT_1:def 3;
hence x in (C ^\ k) . knat by A57, A58; :: thesis:

end;

for x being set holds
( x in (Partial_Intersection (C ^\ k)) . n iff x in (Partial_Intersection B) . n )

proof

let x be set ; :: thesis:
( ( x in (Partial_Intersection (C ^\ k)) . n implies for knat being Nat st knat <= n holds
x in (C ^\ k) . knat ) & ( ( for knat being Nat st knat <= n holds
x in (C ^\ k) . knat ) implies x in (Partial_Intersection (C ^\ k)) . n ) & ( x in (Partial_Intersection B) . n implies for knat being Nat st knat <= n holds
x in B . knat ) & ( ( for knat being Nat st knat <= n holds
x in B . knat ) implies x in (Partial_Intersection B) . n ) ) by PROB_3:25;
hence ( x in (Partial_Intersection (C ^\ k)) . n iff x in (Partial_Intersection B) . n ) by A53; :: thesis:

end;

hence (Partial_Intersection (C ^\ k)) . n = (Partial_Intersection B) . n by TARSKI:1; :: thesis:

end;

A60: Prob . ((Partial_Intersection B) . q) = (Partial_Product (Prob * (C ^\ ((0 + n2) + 1)))) . q by A38, A37, A25;
Prob . ((Partial_Intersection (C ^\ ((0 + n2) + 1))) . q) = (Partial_Product (Prob * (C ^\ ((0 + n2) + 1)))) . q by A38, A51, A60;
hence Prob . (((Partial_Intersection (Complement C)) . 0) /\ ((Partial_Intersection (C ^\ ((0 + n2) + 1))) . q)) = ((Partial_Product (Prob * (Complement C))) . 0) * ((Partial_Product (Prob * (C ^\ ((0 + n2) + 1)))) . q) by A50, SERIES_3:def 1; :: thesis:

end;

A61: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

proof

Prob . (((Partial_Intersection (Complement C)) . k) /\ ((Partial_Intersection (C ^\ (((k + 1) + n2) + 1))) . q)) = ((Partial_Product (Prob * (Complement C))) . k) * ((Partial_Product (Prob * (C ^\ ((k + (1 + n2)) + 1)))) . q) by A63, A64, A62;
hence Prob . (((Partial_Intersection (Complement C)) . k) /\ ((Partial_Intersection (C ^\ (((k + 1) + n2) + 1))) . q)) = ((Partial_Product (Prob * (Complement C))) . k) * ((Partial_Product (Prob * (C ^\ (((k + 1) + n2) + 1)))) . q) ; :: thesis:

end;

A68: Prob . (((Partial_Intersection (Complement C)) . (k + 1)) /\ ((Partial_Intersection (C ^\ (((k + 1) + n2) + 1))) . q)) = (((Partial_Product (Prob * (Complement C))) . k) * ((Partial_Product (Prob * (C ^\ (((k + 1) + n2) + 1)))) . q)) - ((((Prob * C) . (k + 1)) * ((Partial_Product (Prob * (Complement C))) . k)) * ((Partial_Product (Prob * (C ^\ (((k + 1) + n2) + 1)))) . q))

proof

(((Prob * C) . (k + 1)) * ((Partial_Product (Prob * (Complement C))) . k)) * ((Partial_Product (Prob * (C ^\ (((k + 1) + n2) + 1)))) . q) = Prob . ((C . (k + 1)) /\ (((Partial_Intersection (Complement C)) . k) /\ ((Partial_Intersection (C ^\ (((k + 1) + n2) + 1))) . q)))

proof

consider F being SetSequence of Omega such that
A69: F = C * (Special_Function4 (k,n2)) ;
F is SetSequence of Sigma

proof

for n being Element of NAT holds F . n is Event of Sigma

proof

let n be Element of NAT ; :: thesis:
A70: dom (C * (Special_Function4 (k,n2))) = NAT by FUNCT_2:def 1;
F . n = C . ((Special_Function4 (k,n2)) . n) by A69, A70, FUNCT_1:12;
hence F . n is Event of Sigma ; :: thesis:

end;

hence F is SetSequence of Sigma by PROB_1:25; :: thesis:

end;

then reconsider F = F as SetSequence of Sigma ;
( e * (Special_Function4 (k,n2)) is one-to-one & dom (e * (Special_Function4 (k,n2))) <> {} ) by A63, FUNCT_1:24;
then consider f being sequence of NAT such that
A71: ( f = e * (Special_Function4 (k,n2)) & f is one-to-one & dom f <> {} ) ;
A72: for q being set st q in NAT holds
F . q = (A * f) . q

proof

end;

A76: Prob . (((Partial_Intersection (Complement F)) . k) /\ ((Partial_Intersection (F ^\ ((k + 0) + 1))) . (q + 1))) = ((Partial_Product (Prob * (Complement F))) . k) * ((Partial_Product (Prob * (F ^\ ((k + 0) + 1)))) . (q + 1)) by A71, A72, A62, FUNCT_2:12;
A77: (Partial_Intersection (Complement C)) . k = (Partial_Intersection (Complement F)) . k

proof

A78: for x being set
for knat being Nat st knat <= k holds
( x in (Complement C) . knat iff x in (Complement F) . knat )

proof

let x be set ; :: thesis:
let knat be Nat; :: thesis:
assume knat <= k ; :: thesis:
then A79: knat <= k + 1 by NAT_1:13;
reconsider knat = knat as Element of NAT by ORDINAL1:def 12;
dom (C * (Special_Function4 (k,n2))) = NAT by FUNCT_2:def 1;
then A80: (C * (Special_Function4 (k,n2))) . knat = C . ((Special_Function4 (k,n2)) . knat) by FUNCT_1:12;
( (Special_Function4 (k,n2)) . knat = IFGT (knat,(k + 1),(knat + n2),knat) & IFGT (knat,(k + 1),(knat + n2),knat) = knat ) by Def5, A79, XXREAL_0:def 11;
then (Complement F) . knat = (C . knat) ` by A69, A80, PROB_1:def 2;
hence ( x in (Complement C) . knat iff x in (Complement F) . knat ) by PROB_1:def 2; :: thesis:

end;

A81: for x being set holds
( ( for knat being Nat st knat <= k holds
x in (Complement C) . knat ) iff for knat being Nat st knat <= k holds
x in (Complement F) . knat )

proof

let x be set ; :: thesis:

hereby :: thesis:

assume A82: for knat being Nat st knat <= k holds
x in (Complement C) . knat ; :: thesis:
thus for knat being Nat st knat <= k holds
x in (Complement F) . knat :: thesis:

proof

let knat be Nat; :: thesis:
assume A83: knat <= k ; :: thesis:
then ( x in (Complement C) . knat iff x in (Complement F) . knat ) by A78;
hence x in (Complement F) . knat by A83, A82; :: thesis:

end;

assume A84: for knat being Nat st knat <= k holds
x in (Complement F) . knat ; :: thesis:
thus for knat being Nat st knat <= k holds
x in (Complement C) . knat :: thesis:

proof

let knat be Nat; :: thesis:
assume A85: knat <= k ; :: thesis:
then ( x in (Complement C) . knat iff x in (Complement F) . knat ) by A78;
hence x in (Complement C) . knat by A85, A84; :: thesis:

end;

for x being set holds
( x in (Partial_Intersection (Complement C)) . k iff x in (Partial_Intersection (Complement F)) . k )

proof

let x be set ; :: thesis:
( x in (Partial_Intersection (Complement C)) . k iff for knat being Nat st knat <= k holds
x in (Complement C) . knat ) by PROB_3:25;
then ( x in (Partial_Intersection (Complement C)) . k iff for knat being Nat st knat <= k holds
x in (Complement F) . knat ) by A81;
hence ( x in (Partial_Intersection (Complement C)) . k iff x in (Partial_Intersection (Complement F)) . k ) by PROB_3:25; :: thesis:

end;

hence (Partial_Intersection (Complement C)) . k = (Partial_Intersection (Complement F)) . k by TARSKI:1; :: thesis:

end;

A86: (Partial_Intersection (F ^\ (k + 1))) . (q + 1) = (C . (k + 1)) /\ ((Partial_Intersection (C ^\ (((k + 1) + n2) + 1))) . q)

proof

A87: for x being set
for knat being Nat st knat <= q holds
( x in (F ^\ ((k + 1) + 1)) . knat iff x in (C ^\ (((k + 1) + n2) + 1)) . knat )

proof

let x be set ; :: thesis:
let knat be Nat; :: thesis:
assume knat <= q ; :: thesis:
reconsider knat = knat as Element of NAT by ORDINAL1:def 12;
A88: dom (C * (Special_Function4 (k,n2))) = NAT by FUNCT_2:def 1;
set j = ((knat + k) + 1) + 1;
((knat + k) + 1) + 1 > k + 1

proof

( k + 1 < (k + 1) + 1 & k + 2 <= (k + 2) + knat ) by NAT_1:12, NAT_1:13;
hence ((knat + k) + 1) + 1 > k + 1 by XXREAL_0:2; :: thesis:

end;

then ( (Special_Function4 (k,n2)) . (((knat + k) + 1) + 1) = IFGT ((((knat + k) + 1) + 1),(k + 1),((((knat + k) + 1) + 1) + n2),(((knat + k) + 1) + 1)) & IFGT ((((knat + k) + 1) + 1),(k + 1),((((knat + k) + 1) + 1) + n2),(((knat + k) + 1) + 1)) = (((knat + k) + 1) + 1) + n2 ) by Def5, XXREAL_0:def 11;
then F . (knat + ((k + 1) + 1)) = C . (knat + (((k + 1) + n2) + 1)) by A69, A88, FUNCT_1:12;
then (F ^\ ((k + 1) + 1)) . knat = C . (knat + (((k + 1) + n2) + 1)) by NAT_1:def 3;
hence ( x in (F ^\ ((k + 1) + 1)) . knat iff x in (C ^\ (((k + 1) + n2) + 1)) . knat ) by NAT_1:def 3; :: thesis:

end;

A89: for x being set holds
( ( for knat being Nat st knat <= q holds
x in (C ^\ (((k + 1) + n2) + 1)) . knat ) iff for knat being Nat st knat <= q holds
x in (F ^\ ((k + 1) + 1)) . knat )

proof

let x be set ; :: thesis:

hereby :: thesis:

assume A90: for knat being Nat st knat <= q holds
x in (C ^\ (((k + 1) + n2) + 1)) . knat ; :: thesis:
thus for knat being Nat st knat <= q holds
x in (F ^\ ((k + 1) + 1)) . knat :: thesis:

proof

let knat be Nat; :: thesis:
assume A91: knat <= q ; :: thesis:
then ( x in (C ^\ (((k + 1) + n2) + 1)) . knat iff x in (F ^\ ((k + 1) + 1)) . knat ) by A87;
hence x in (F ^\ ((k + 1) + 1)) . knat by A91, A90; :: thesis:

end;

assume A92: for knat being Nat st knat <= q holds
x in (F ^\ ((k + 1) + 1)) . knat ; :: thesis:
thus for knat being Nat st knat <= q holds
x in (C ^\ (((k + 1) + n2) + 1)) . knat :: thesis:

proof

let knat be Nat; :: thesis:
assume A93: knat <= q ; :: thesis:
then ( x in (C ^\ (((k + 1) + n2) + 1)) . knat iff x in (F ^\ ((k + 1) + 1)) . knat ) by A87;
hence x in (C ^\ (((k + 1) + n2) + 1)) . knat by A93, A92; :: thesis:

end;

A94: for x being set holds
( x in (Partial_Intersection (C ^\ (((k + 1) + n2) + 1))) . q iff x in (Partial_Intersection (F ^\ ((k + 1) + 1))) . q )

proof

let x be set ; :: thesis:
( x in (Partial_Intersection (C ^\ (((k + 1) + n2) + 1))) . q iff for knat being Nat st knat <= q holds
x in (C ^\ (((k + 1) + n2) + 1)) . knat ) by PROB_3:25;
then ( x in (Partial_Intersection (C ^\ (((k + 1) + n2) + 1))) . q iff for knat being Nat st knat <= q holds
x in (F ^\ ((k + 1) + 1)) . knat ) by A89;
hence ( x in (Partial_Intersection (C ^\ (((k + 1) + n2) + 1))) . q iff x in (Partial_Intersection (F ^\ ((k + 1) + 1))) . q ) by PROB_3:25; :: thesis:

end;

((Partial_Intersection (F ^\ ((k + 1) + 1))) . q) /\ (C . (k + 1)) = (Partial_Intersection (F ^\ (k + 1))) . (q + 1)

proof

defpred S₂[ Element of NAT ] means ((Partial_Intersection (F ^\ ((k + 1) + 1))) . $1) /\ (C . (k + 1)) = (Partial_Intersection (F ^\ (k + 1))) . ($1 + 1);
A95: S₂[ 0 ]

proof

((Partial_Intersection (F ^\ ((k + 1) + 1))) . 0) /\ (C . (k + 1)) = ((F ^\ ((k + 1) + 1)) . 0) /\ (C . (k + 1)) by PROB_3:21;
then ((Partial_Intersection (F ^\ ((k + 1) + 1))) . 0) /\ (C . (k + 1)) = (F . (0 + ((k + 1) + 1))) /\ (C . (k + 1)) by NAT_1:def 3;
then A96: ((Partial_Intersection (F ^\ ((k + 1) + 1))) . 0) /\ (C . (k + 1)) = ((F ^\ (k + 1)) . (0 + 1)) /\ (C . (k + 1)) by NAT_1:def 3;
A97: dom (C * (Special_Function4 (k,n2))) = NAT by FUNCT_2:def 1;
( (Special_Function4 (k,n2)) . (k + 1) = IFGT ((k + 1),(k + 1),((k + 1) + n2),(k + 1)) & IFGT ((k + 1),(k + 1),((k + 1) + n2),(k + 1)) = k + 1 ) by Def5, XXREAL_0:def 11;
then ((Partial_Intersection (F ^\ ((k + 1) + 1))) . 0) /\ (C . (k + 1)) = ((F ^\ (k + 1)) . (0 + 1)) /\ (F . (0 + (k + 1))) by A69, A97, A96, FUNCT_1:12;
then ((Partial_Intersection (F ^\ ((k + 1) + 1))) . 0) /\ (C . (k + 1)) = ((F ^\ (k + 1)) . (0 + 1)) /\ ((F ^\ (k + 1)) . 0) by NAT_1:def 3;
then ((Partial_Intersection (F ^\ ((k + 1) + 1))) . 0) /\ (C . (k + 1)) = ((Partial_Intersection (F ^\ (k + 1))) . 0) /\ ((F ^\ (k + 1)) . (0 + 1)) by PROB_3:21;
hence S₂[ 0 ] by PROB_3:21; :: thesis:

end;

A98: for q being Element of NAT st S₂[q] holds
S₂[q + 1]

proof

let q be Element of NAT ; :: thesis:
assume A99: S₂[q] ; :: thesis:
((Partial_Intersection (F ^\ ((k + 1) + 1))) . (q + 1)) /\ (C . (k + 1)) = (((Partial_Intersection (F ^\ ((k + 1) + 1))) . q) /\ ((F ^\ ((k + 1) + 1)) . (q + 1))) /\ (C . (k + 1)) by PROB_3:21;
then A100: ((Partial_Intersection (F ^\ ((k + 1) + 1))) . (q + 1)) /\ (C . (k + 1)) = ((Partial_Intersection (F ^\ (k + 1))) . (q + 1)) /\ ((F ^\ ((k + 1) + 1)) . (q + 1)) by A99, XBOOLE_1:16;
(F ^\ ((k + 1) + 1)) . (q + 1) = (F ^\ (k + 1)) . ((q + 1) + 1)

proof

(F ^\ ((k + 1) + 1)) . (q + 1) = F . ((q + 1) + ((k + 1) + 1)) by NAT_1:def 3;
then (F ^\ ((k + 1) + 1)) . (q + 1) = F . (((q + 1) + 1) + (k + 1)) ;
hence (F ^\ ((k + 1) + 1)) . (q + 1) = (F ^\ (k + 1)) . ((q + 1) + 1) by NAT_1:def 3; :: thesis:

end;

hence S₂[q + 1] by A100, PROB_3:21; :: thesis:

end;

for k being Element of NAT holds S₂[k] from NAT_1:sch 1(A95, A98);
hence ((Partial_Intersection (F ^\ ((k + 1) + 1))) . q) /\ (C . (k + 1)) = (Partial_Intersection (F ^\ (k + 1))) . (q + 1) ; :: thesis:

end;

hence (Partial_Intersection (F ^\ (k + 1))) . (q + 1) = (C . (k + 1)) /\ ((Partial_Intersection (C ^\ (((k + 1) + n2) + 1))) . q) by A94, TARSKI:1; :: thesis:

end;

A101: (Partial_Product (Prob * (F ^\ (k + 1)))) . (q + 1) = ((Prob * C) . (k + 1)) * ((Partial_Product (Prob * (C ^\ (((k + 1) + n2) + 1)))) . q)

proof

defpred S₂[ Element of NAT ] means (Partial_Product (Prob * (F ^\ (k + 1)))) . ($1 + 1) = ((Prob * C) . (k + 1)) * ((Partial_Product (Prob * (C ^\ (((k + 1) + n2) + 1)))) . $1);
A102: S₂[ 0 ]

proof

A103: (F ^\ (k + 1)) . (0 + 1) = (C * (Special_Function4 (k,n2))) . ((k + 1) + 1) by A69, NAT_1:def 3;
A104: dom (C * (Special_Function4 (k,n2))) = NAT by FUNCT_2:def 1;
set j = (k + 1) + 1;
(k + 1) + 1 > k + 1 by NAT_1:13;
then ( (Special_Function4 (k,n2)) . ((k + 1) + 1) = IFGT (((k + 1) + 1),(k + 1),(((k + 1) + 1) + n2),((k + 1) + 1)) & IFGT (((k + 1) + 1),(k + 1),(((k + 1) + 1) + n2),((k + 1) + 1)) = ((k + 1) + 1) + n2 ) by Def5, XXREAL_0:def 11;
then (F ^\ (k + 1)) . (0 + 1) = C . (0 + (((k + 1) + n2) + 1)) by A104, A103, FUNCT_1:12;
then A105: Prob . ((F ^\ (k + 1)) . (0 + 1)) = Prob . ((C ^\ (((k + 1) + n2) + 1)) . 0) by NAT_1:def 3;
( dom (Prob * (F ^\ (k + 1))) = NAT & dom (Prob * (C ^\ (((k + 1) + n2) + 1))) = NAT ) by FUNCT_2:def 1;
then ( (Prob * (F ^\ (k + 1))) . (0 + 1) = Prob . ((C ^\ (((k + 1) + n2) + 1)) . 0) & Prob . ((F ^\ (k + 1)) . (0 + 1)) = (Prob * (C ^\ (((k + 1) + n2) + 1))) . 0 & Prob . ((F ^\ (k + 1)) . (0 + 1)) = Prob . ((C ^\ (((k + 1) + n2) + 1)) . 0) ) by A105, FUNCT_1:12;
then A106: ((Partial_Product (Prob * (F ^\ (k + 1)))) . 0) * ((Prob * (F ^\ (k + 1))) . (0 + 1)) = ((Prob * (F ^\ (k + 1))) . 0) * ((Prob * (C ^\ (((k + 1) + n2) + 1))) . 0) by SERIES_3:def 1;
(Prob * (F ^\ (k + 1))) . 0 = (Prob * C) . (k + 1)

proof

A107: (F ^\ (k + 1)) . 0 = F . (0 + (k + 1)) by NAT_1:def 3;
A108: dom (C * (Special_Function4 (k,n2))) = NAT by FUNCT_2:def 1;
A109: F . (k + 1) = C . ((Special_Function4 (k,n2)) . (k + 1)) by A69, A108, FUNCT_1:12;
A110: ( (Special_Function4 (k,n2)) . (k + 1) = IFGT ((k + 1),(k + 1),((k + 1) + n2),(k + 1)) & IFGT ((k + 1),(k + 1),((k + 1) + n2),(k + 1)) = k + 1 ) by Def5, XXREAL_0:def 11;
dom (Prob * C) = NAT by FUNCT_2:def 1;
then A111: Prob . ((F ^\ (k + 1)) . 0) = (Prob * C) . (k + 1) by A110, A109, A107, FUNCT_1:12;
dom (Prob * (F ^\ (k + 1))) = NAT by FUNCT_2:def 1;
hence (Prob * (F ^\ (k + 1))) . 0 = (Prob * C) . (k + 1) by A111, FUNCT_1:12; :: thesis:

end;

then (Partial_Product (Prob * (F ^\ (k + 1)))) . (0 + 1) = ((Prob * C) . (k + 1)) * ((Prob * (C ^\ (((k + 1) + n2) + 1))) . 0) by A106, SERIES_3:def 1;
hence S₂[ 0 ] by SERIES_3:def 1; :: thesis:

end;

A112: for q being Element of NAT st S₂[q] holds
S₂[q + 1]

proof

let q be Element of NAT ; :: thesis:
assume A113: S₂[q] ; :: thesis:
A114: (Prob * (F ^\ (k + 1))) . ((q + 1) + 1) = (Prob * (C ^\ (((k + 1) + n2) + 1))) . (q + 1)

proof

A115: (F ^\ (k + 1)) . ((q + 1) + 1) = (C * (Special_Function4 (k,n2))) . (((q + 1) + 1) + (k + 1)) by A69, NAT_1:def 3;
A116: dom (C * (Special_Function4 (k,n2))) = NAT by FUNCT_2:def 1;
set j = ((q + 1) + 1) + (k + 1);
((q + 1) + 1) + (k + 1) > k + 1

proof

( k + 1 < (k + 1) + 1 & (k + 1) + 1 <= ((k + 1) + 1) + (q + 1) ) by NAT_1:13, XREAL_1:31;
hence ((q + 1) + 1) + (k + 1) > k + 1 by XXREAL_0:2; :: thesis:

end;

then ( (Special_Function4 (k,n2)) . (((q + 1) + 1) + (k + 1)) = IFGT ((((q + 1) + 1) + (k + 1)),(k + 1),((((q + 1) + 1) + (k + 1)) + n2),(((q + 1) + 1) + (k + 1))) & IFGT ((((q + 1) + 1) + (k + 1)),(k + 1),((((q + 1) + 1) + (k + 1)) + n2),(((q + 1) + 1) + (k + 1))) = (((q + 1) + 1) + (k + 1)) + n2 ) by Def5, XXREAL_0:def 11;
then (F ^\ (k + 1)) . ((q + 1) + 1) = C . ((q + 1) + (((k + 1) + n2) + 1)) by A116, A115, FUNCT_1:12;
then A117: Prob . ((F ^\ (k + 1)) . ((q + 1) + 1)) = Prob . ((C ^\ (((k + 1) + n2) + 1)) . (q + 1)) by NAT_1:def 3;
( dom (Prob * (F ^\ (k + 1))) = NAT & dom (Prob * (C ^\ (((k + 1) + n2) + 1))) = NAT ) by FUNCT_2:def 1;
then ( (Prob * (F ^\ (k + 1))) . ((q + 1) + 1) = Prob . ((C ^\ (((k + 1) + n2) + 1)) . (q + 1)) & Prob . ((F ^\ (k + 1)) . ((q + 1) + 1)) = (Prob * (C ^\ (((k + 1) + n2) + 1))) . (q + 1) & Prob . ((F ^\ (k + 1)) . ((q + 1) + 1)) = Prob . ((C ^\ (((k + 1) + n2) + 1)) . (q + 1)) ) by A117, FUNCT_1:12;
hence (Prob * (F ^\ (k + 1))) . ((q + 1) + 1) = (Prob * (C ^\ (((k + 1) + n2) + 1))) . (q + 1) ; :: thesis:

end;

(Partial_Product (Prob * (F ^\ (k + 1)))) . ((q + 1) + 1) = (((Prob * C) . (k + 1)) * ((Partial_Product (Prob * (C ^\ (((k + 1) + n2) + 1)))) . q)) * ((Prob * (C ^\ (((k + 1) + n2) + 1))) . (q + 1)) by A113, A114, SERIES_3:def 1;
then (Partial_Product (Prob * (F ^\ (k + 1)))) . ((q + 1) + 1) = ((Prob * C) . (k + 1)) * (((Partial_Product (Prob * (C ^\ (((k + 1) + n2) + 1)))) . q) * ((Prob * (C ^\ (((k + 1) + n2) + 1))) . (q + 1))) ;
hence S₂[q + 1] by SERIES_3:def 1; :: thesis:

end;

for k being Element of NAT holds S₂[k] from NAT_1:sch 1(A102, A112);
hence (Partial_Product (Prob * (F ^\ (k + 1)))) . (q + 1) = ((Prob * C) . (k + 1)) * ((Partial_Product (Prob * (C ^\ (((k + 1) + n2) + 1)))) . q) ; :: thesis:

end;

defpred S₂[ Element of NAT ] means ( ( for k being Element of NAT st k <= $1 holds
C . k = F . k ) implies (Partial_Product (Prob * (Complement F))) . $1 = (Partial_Product (Prob * (Complement C))) . $1 );
dom (C * (Special_Function4 (k,n2))) = NAT by FUNCT_2:def 1;
then A118: (C * (Special_Function4 (k,n2))) . 0 = C . ((Special_Function4 (k,n2)) . 0) by FUNCT_1:12;
A119: IFGT (0,(k + 1),(0 + n2),0) = 0 by XXREAL_0:def 11;
then (F . 0) ` = (C . 0) ` by Def5, A118, A69;
then (Complement F) . 0 = (C . 0) ` by PROB_1:def 2;
then ( Prob . ((Complement F) . 0) = Prob . ((Complement C) . 0) & dom (Prob * (Complement F)) = NAT & dom (Prob * (Complement C)) = NAT ) by FUNCT_2:def 1, PROB_1:def 2;
then ( Prob . ((Complement F) . 0) = Prob . ((Complement C) . 0) & (Prob * (Complement F)) . 0 = Prob . ((Complement F) . 0) & (Prob * (Complement C)) . 0 = Prob . ((Complement C) . 0) ) by FUNCT_1:12;
then A120: ( (Partial_Product (Prob * (Complement F))) . 0 = (Prob * (Complement C)) . 0 & F . 0 = C . 0 ) by A119, Def5, A118, A69, SERIES_3:def 1;
A121: S₂[ 0 ] by A120, SERIES_3:def 1;
A122: for q being Element of NAT st S₂[q] holds
S₂[q + 1]

proof

let q be Element of NAT ; :: thesis:
assume A123: S₂[q] ; :: thesis:
A124: ( ( for k being Element of NAT st k <= q + 1 holds
C . k = F . k ) implies for k being Element of NAT st k <= q holds
C . k = F . k )

proof

assume A125: for k being Element of NAT st k <= q + 1 holds
C . k = F . k ; :: thesis:
let k be Element of NAT ; :: thesis:
assume k <= q ; :: thesis:
then k <= q + 1 by NAT_1:13;
hence C . k = F . k by A125; :: thesis:

end;

( ( for k being Element of NAT st k <= q + 1 holds
C . k = F . k ) implies (Partial_Product (Prob * (Complement F))) . (q + 1) = (Partial_Product (Prob * (Complement C))) . (q + 1) )

proof

assume A126: for k being Element of NAT st k <= q + 1 holds
C . k = F . k ; :: thesis:
then ( q + 1 <= q + 1 implies (C . (q + 1)) ` = (F . (q + 1)) ` ) ;
then ( q + 1 <= q + 1 implies (Complement C) . (q + 1) = (F . (q + 1)) ` ) by PROB_1:def 2;
then A127: ((Partial_Product (Prob * (Complement F))) . q) * (Prob . ((Complement F) . (q + 1))) = ((Partial_Product (Prob * (Complement C))) . q) * (Prob . ((Complement C) . (q + 1))) by A126, A124, A123, PROB_1:def 2;
( dom (Prob * (Complement C)) = NAT & dom (Prob * (Complement F)) = NAT ) by FUNCT_2:def 1;
then ( (Prob * (Complement C)) . (q + 1) = Prob . ((Complement C) . (q + 1)) & (Prob * (Complement F)) . (q + 1) = Prob . ((Complement F) . (q + 1)) ) by FUNCT_1:12;
then (Partial_Product (Prob * (Complement F))) . (q + 1) = ((Partial_Product (Prob * (Complement C))) . q) * ((Prob * (Complement C)) . (q + 1)) by A127, SERIES_3:def 1;
hence (Partial_Product (Prob * (Complement F))) . (q + 1) = (Partial_Product (Prob * (Complement C))) . (q + 1) by SERIES_3:def 1; :: thesis:

end;

hence S₂[q + 1] ; :: thesis:

end;

A128: for k being Element of NAT holds S₂[k] from NAT_1:sch 1(A121, A122);
for q being Element of NAT st q <= k holds
C . q = F . q

proof

let q be Element of NAT ; :: thesis:
assume q <= k ; :: thesis:
then A129: q <= k + 1 by NAT_1:13;
A130: dom (C * (Special_Function4 (k,n2))) = NAT by FUNCT_2:def 1;
( (Special_Function4 (k,n2)) . q = IFGT (q,(k + 1),(q + n2),q) & IFGT (q,(k + 1),(q + n2),q) = q ) by Def5, A129, XXREAL_0:def 11;
hence C . q = F . q by A130, A69, FUNCT_1:12; :: thesis:

end;

then Prob . (((Partial_Intersection (Complement C)) . k) /\ ((C . (k + 1)) /\ ((Partial_Intersection (C ^\ (((k + 1) + n2) + 1))) . q))) = ((Partial_Product (Prob * (Complement C))) . k) * (((Prob * C) . (k + 1)) * ((Partial_Product (Prob * (C ^\ (((k + 1) + n2) + 1)))) . q)) by A128, A101, A86, A77, A76;
hence (((Prob * C) . (k + 1)) * ((Partial_Product (Prob * (Complement C))) . k)) * ((Partial_Product (Prob * (C ^\ (((k + 1) + n2) + 1)))) . q) = Prob . ((C . (k + 1)) /\ (((Partial_Intersection (Complement C)) . k) /\ ((Partial_Intersection (C ^\ (((k + 1) + n2) + 1))) . q))) by XBOOLE_1:16; :: thesis:

end;

hence Prob . (((Partial_Intersection (Complement C)) . (k + 1)) /\ ((Partial_Intersection (C ^\ (((k + 1) + n2) + 1))) . q)) = (((Partial_Product (Prob * (Complement C))) . k) * ((Partial_Product (Prob * (C ^\ (((k + 1) + n2) + 1)))) . q)) - ((((Prob * C) . (k + 1)) * ((Partial_Product (Prob * (Complement C))) . k)) * ((Partial_Product (Prob * (C ^\ (((k + 1) + n2) + 1)))) . q)) by A67, A66, PROB_1:33, XBOOLE_1:17; :: thesis:

end;

(Prob * C) . (k + 1) = 1 - ((Prob * (Complement C)) . (k + 1))

proof

( C . (k + 1) = ((C . (k + 1)) `) ` & ((C . (k + 1)) `) ` = Omega \ ((C . (k + 1)) `) ) by SUBSET_1:def 4;
then ( Prob . (C . (k + 1)) = Prob . (([#] Sigma) \ ((C . (k + 1)) `)) & (C . (k + 1)) ` is Event of Sigma ) by PROB_1:20;
then A131: Prob . (C . (k + 1)) = 1 - (Prob . ((C . (k + 1)) `)) by PROB_1:32;
dom (Prob * C) = NAT by FUNCT_2:def 1;
then A132: (Prob * C) . (k + 1) = 1 - (Prob . ((C . (k + 1)) `)) by A131, FUNCT_1:12;
dom (Prob * (Complement C)) = NAT by FUNCT_2:def 1;
then (Prob * (Complement C)) . (k + 1) = Prob . ((Complement C) . (k + 1)) by FUNCT_1:12;
hence (Prob * C) . (k + 1) = 1 - ((Prob * (Complement C)) . (k + 1)) by A132, PROB_1:def 2; :: thesis:

end;

then Prob . (((Partial_Intersection (Complement C)) . (k + 1)) /\ ((Partial_Intersection (C ^\ (((k + 1) + n2) + 1))) . q)) = (((Prob * (Complement C)) . (k + 1)) * ((Partial_Product (Prob * (Complement C))) . k)) * ((Partial_Product (Prob * (C ^\ (((k + 1) + n2) + 1)))) . q) by A68;
hence Prob . (((Partial_Intersection (Complement C)) . (k + 1)) /\ ((Partial_Intersection (C ^\ (((k + 1) + n2) + 1))) . q)) = ((Partial_Product (Prob * (Complement C))) . (k + 1)) * ((Partial_Product (Prob * (C ^\ (((k + 1) + n2) + 1)))) . q) by SERIES_3:def 1; :: thesis:

end;

A133: for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A36, A61);
ex e being sequence of NAT st
( A * e = A & e is one-to-one & dom e <> {} )

proof

set e = Special_Function2 0;
A134: dom (Special_Function2 0) <> {} ;
( A is sequence of (bool Omega) & A * (Special_Function2 0) is sequence of (bool Omega) & ( for n being set st n in NAT holds
(A * (Special_Function2 0)) . n = A . n ) )

proof

A135: for n being set st n in NAT holds
( (A * (Special_Function2 0)) . n = A . n & A . ((Special_Function2 0) . n) = A . n )

proof

let n be set ; :: thesis:
assume n in NAT ; :: thesis:
then reconsider n = n as Element of NAT ;
A136: (Special_Function2 0) . n = n + 0 by Def3;
dom (A * (Special_Function2 0)) = NAT by FUNCT_2:def 1;
hence ( (A * (Special_Function2 0)) . n = A . n & A . ((Special_Function2 0) . n) = A . n ) by A136, FUNCT_1:12; :: thesis:

end;

thus ( A is sequence of (bool Omega) & A * (Special_Function2 0) is sequence of (bool Omega) & ( for n being set st n in NAT holds
(A * (Special_Function2 0)) . n = A . n ) ) by A135; :: thesis:

end;

hence ex e being sequence of NAT st
( A * e = A & e is one-to-one & dom e <> {} ) by A134, FUNCT_2:12; :: thesis:

end;

hence Prob . (((Partial_Intersection (Complement A)) . n1) /\ ((Partial_Intersection (A ^\ ((n1 + n2) + 1))) . q)) = ((Partial_Product (Prob * (Complement A))) . n1) * ((Partial_Product (Prob * (A ^\ ((n1 + n2) + 1)))) . q) by A133; :: thesis:

end;

(n - n1) - 1 is Element of NAT

proof

n1 + 1 <= n by A1, NAT_1:13;
then (n1 + 1) - 1 <= n - 1 by XREAL_1:9;
then ( n1 <= n - 1 & n - 1 is Element of NAT ) by A1, 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;

hence Prob . (((Partial_Intersection (Complement A)) . n1) /\ ((Partial_Intersection (A ^\ ((n1 + n2) + 1))) . ((n - n1) - 1))) = ((Partial_Product (Prob * (Complement A))) . n1) * ((Partial_Product (Prob * (A ^\ ((n1 + n2) + 1)))) . ((n - n1) - 1)) by A35; :: thesis: