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 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₁[ 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 Nat st S₁[q] holds
S₁[q + 1]

let q be Nat; :: thesis:
assume S₁[q] ; :: thesis:
then A13: (Partial_Product (Prob * (A ^\ k))) . (q + 1) = ((Partial_Product (Prob * B)) . q) * ((Prob * (A ^\ k)) . (q + 1)) by 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 Nat holds S₁[k] from NAT_1:sch 2(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 Nat holds A . ((e * (Special_Function (m1,m2))) . n) = B . n ) )

proof

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

proof

let n be Nat; :: thesis:
A22: dom ((A * e) * (Special_Function (m1,m2))) = NAT by FUNCT_2:def 1;
reconsider n = n as Element of NAT by ORDINAL1:def 12;
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 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;
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 Nat holds A . ((e * (Special_Function2 m1)) . n) = B . n ) )

proof

for n being Nat holds A . ((e * (Special_Function2 m1)) . n) = B . n

proof

end;

hence ( 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 Nat holds A . ((e * (Special_Function2 m1)) . n) = B . n ) ) by A27, FUNCT_1:24; :: thesis:

end;

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

end;

A35: for q being 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 Nat; :: thesis:
defpred S₁[ Nat] means for e being sequence of NAT
for q, n2 being 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 A38, A43, 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 A46: Prob . (C . 0) = 1 - (Prob . ((C . 0) `)) by PROB_1:32;
dom (Prob * C) = NAT by FUNCT_2:def 1;
then A47: (Prob * C) . 0 = 1 - (Prob . ((C . 0) `)) by A46, 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 A47, PROB_1:def 2; :: thesis:

end;

then A48: 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 A45;
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 ;
A49: for A, B, C being SetSequence of Sigma
for k, n being Element of NAT
for e being sequence of NAT st 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 A50: B = C * (Special_Function2 k) ; :: thesis:
A51: 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 A52: 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 A53: 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 A54: (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 A50, A54, NAT_1:def 3;
hence x in B . knat by A53, A52; :: thesis:

end;

assume A55: 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 A56: 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 A57: (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 A50, A57, NAT_1:def 3;
hence x in (C ^\ k) . knat by A55, A56; :: thesis:

end;

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

proof

let x be object ; :: 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 A51; :: thesis:

end;

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

end;

q in NAT by ORDINAL1:def 12;
then A58: Prob . ((Partial_Intersection B) . q) = (Partial_Product (Prob * (C ^\ ((0 + n2) + 1)))) . q by A38, A37, A25;
q in NAT by ORDINAL1:def 12;
then Prob . ((Partial_Intersection (C ^\ ((0 + n2) + 1))) . q) = (Partial_Product (Prob * (C ^\ ((0 + n2) + 1)))) . q by A49, A58;
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 A48, SERIES_3:def 1; :: thesis:

end;

A59: for k being 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 A61, A62, A60;
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;

A66: 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
A67: F = C * (Special_Function4 (k,n2)) ;
F is SetSequence of Sigma

proof

for n being Nat holds F . n is Event of Sigma

proof

let n be Nat; :: thesis:
dom (C * (Special_Function4 (k,n2))) = NAT by FUNCT_2:def 1;
then F . n = C . ((Special_Function4 (k,n2)) . n) by A67, FUNCT_1:12, ORDINAL1:def 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 A61, FUNCT_1:24;
then consider f being sequence of NAT such that
A70: ( f = e * (Special_Function4 (k,n2)) & f is one-to-one & dom f <> {} ) ;
A71: for q being object st q in NAT holds
F . q = (A * f) . q

proof

end;

A75: 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 A70, A71, A60, FUNCT_2:12;
A76: (Partial_Intersection (Complement C)) . k = (Partial_Intersection (Complement F)) . k

proof

A77: 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 A78: 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 A79: (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, A78, XXREAL_0:def 11;
then (Complement F) . knat = (C . knat) ` by A67, A79, PROB_1:def 2;
hence ( x in (Complement C) . knat iff x in (Complement F) . knat ) by PROB_1:def 2; :: thesis:

end;

A80: for x being object 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 object ; :: thesis:

hereby :: thesis:

assume A81: 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 A82: knat <= k ; :: thesis:
then ( x in (Complement C) . knat iff x in (Complement F) . knat ) by A77;
hence x in (Complement F) . knat by A82, A81; :: thesis:

end;

assume A83: 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 A84: knat <= k ; :: thesis:
then ( x in (Complement C) . knat iff x in (Complement F) . knat ) by A77;
hence x in (Complement C) . knat by A84, A83; :: thesis:

end;

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

proof

let x be object ; :: 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 A80;
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:2; :: thesis:

end;

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

proof

A86: 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;
A87: 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 A67, A87, 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;

A88: for x being object 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 object ; :: thesis:

hereby :: thesis:

assume A89: 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 A90: knat <= q ; :: thesis:
then ( x in (C ^\ (((k + 1) + n2) + 1)) . knat iff x in (F ^\ ((k + 1) + 1)) . knat ) by A86;
hence x in (F ^\ ((k + 1) + 1)) . knat by A90, A89; :: thesis:

end;

assume A91: 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 A92: knat <= q ; :: thesis:
then ( x in (C ^\ (((k + 1) + n2) + 1)) . knat iff x in (F ^\ ((k + 1) + 1)) . knat ) by A86;
hence x in (C ^\ (((k + 1) + n2) + 1)) . knat by A92, A91; :: thesis:

end;

A93: for x being object 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 object ; :: 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 A88;
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₂[ Nat] means ((Partial_Intersection (F ^\ ((k + 1) + 1))) . $1) /\ (C . (k + 1)) = (Partial_Intersection (F ^\ (k + 1))) . ($1 + 1);
A94: 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 A95: ((Partial_Intersection (F ^\ ((k + 1) + 1))) . 0) /\ (C . (k + 1)) = ((F ^\ (k + 1)) . (0 + 1)) /\ (C . (k + 1)) by NAT_1:def 3;
A96: 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 A67, A96, A95, 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;

A97: for q being Nat st S₂[q] holds
S₂[q + 1]

proof

let q be Nat; :: thesis:
assume A98: 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 A99: ((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 A98, 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 A99, PROB_3:21; :: thesis:

end;

for k being Nat holds S₂[k] from NAT_1:sch 2(A94, A97);
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 A93, TARSKI:2; :: thesis:

end;

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

proof

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

proof

A102: (F ^\ (k + 1)) . (0 + 1) = (C * (Special_Function4 (k,n2))) . ((k + 1) + 1) by A67, NAT_1:def 3;
A103: 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 A103, A102, FUNCT_1:12;
then A104: 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 A104, FUNCT_1:12;
then A105: ((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

A106: (F ^\ (k + 1)) . 0 = F . (0 + (k + 1)) by NAT_1:def 3;
A107: dom (C * (Special_Function4 (k,n2))) = NAT by FUNCT_2:def 1;
A108: F . (k + 1) = C . ((Special_Function4 (k,n2)) . (k + 1)) by A67, A107, FUNCT_1:12;
A109: ( (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 A110: Prob . ((F ^\ (k + 1)) . 0) = (Prob * C) . (k + 1) by A109, A108, A106, 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 A110, 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 A105, SERIES_3:def 1;
hence S₂[ 0 ] by SERIES_3:def 1; :: thesis:

end;

A111: for q being Nat st S₂[q] holds
S₂[q + 1]

proof

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

proof

A114: (F ^\ (k + 1)) . ((q + 1) + 1) = (C * (Special_Function4 (k,n2))) . (((q + 1) + 1) + (k + 1)) by A67, NAT_1:def 3;
A115: 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 A115, A114, FUNCT_1:12;
then A116: 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 A116, 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 A112, A113, 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 Nat holds S₂[k] from NAT_1:sch 2(A101, A111);
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₂[ 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 A117: (C * (Special_Function4 (k,n2))) . 0 = C . ((Special_Function4 (k,n2)) . 0) by FUNCT_1:12;
A118: IFGT (0,(k + 1),(0 + n2),0) = 0 by XXREAL_0:def 11;
then (F . 0) ` = (C . 0) ` by Def5, A117, A67;
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 A119: ( (Partial_Product (Prob * (Complement F))) . 0 = (Prob * (Complement C)) . 0 & F . 0 = C . 0 ) by A118, Def5, A117, A67, SERIES_3:def 1;
A120: S₂[ 0 ] by A119, SERIES_3:def 1;
A121: for q being Nat st S₂[q] holds
S₂[q + 1]

proof

let q be Nat; :: thesis:
assume A122: S₂[q] ; :: thesis:
A123: ( ( 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 A124: 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 A124; :: 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 A125: 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 A126: ((Partial_Product (Prob * (Complement F))) . q) * (Prob . ((Complement F) . (q + 1))) = ((Partial_Product (Prob * (Complement C))) . q) * (Prob . ((Complement C) . (q + 1))) by A125, A123, A122, 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 A126, 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;

A127: for k being Nat holds S₂[k] from NAT_1:sch 2(A120, A121);
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 A128: q <= k + 1 by NAT_1:13;
A129: 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, A128, XXREAL_0:def 11;
hence C . q = F . q by A129, A67, 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 A127, A100, A85, A76, A75;
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 A65, A64, 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 A130: Prob . (C . (k + 1)) = 1 - (Prob . ((C . (k + 1)) `)) by PROB_1:32;
dom (Prob * C) = NAT by FUNCT_2:def 1;
then A131: (Prob * C) . (k + 1) = 1 - (Prob . ((C . (k + 1)) `)) by A130, 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 A131, 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 A66;
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;

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

proof

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

proof

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

proof

let n be object ; :: thesis:
assume n in NAT ; :: thesis:
then reconsider n = n as Element of NAT ;
A135: (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 A135, FUNCT_1:12; :: thesis:

end;

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

end;

hence ex e being sequence of NAT st
( A * e = A & e is one-to-one & dom e <> {} ) by A133, 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 A132; :: 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: