let Omega be non empty set ; :: thesis: for Sigma being SigmaField of Omega

for Prob being Probability of Sigma

for A being SetSequence of Sigma

for n, n1, n2 being Nat st n > n1 & A is_all_independent_wrt Prob holds

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))

let Sigma be SigmaField of Omega; :: thesis: for Prob being Probability of Sigma

for A being SetSequence of Sigma

for n, n1, n2 being Nat st n > n1 & A is_all_independent_wrt Prob holds

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))

let Prob be Probability of Sigma; :: thesis: for A being SetSequence of Sigma

for n, n1, n2 being Nat st n > n1 & A is_all_independent_wrt Prob holds

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))

let A be SetSequence of Sigma; :: thesis: for n, n1, n2 being Nat st n > n1 & A is_all_independent_wrt Prob holds

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))

let n, n1, n2 be Nat; :: thesis: ( n > n1 & A is_all_independent_wrt Prob implies 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)) )

assume that

A1: n > n1 and

A2: A is_all_independent_wrt Prob ; :: thesis: 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))

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

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))

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

for Prob being Probability of Sigma

for A being SetSequence of Sigma

for n, n1, n2 being Nat st n > n1 & A is_all_independent_wrt Prob holds

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))

let Sigma be SigmaField of Omega; :: thesis: for Prob being Probability of Sigma

for A being SetSequence of Sigma

for n, n1, n2 being Nat st n > n1 & A is_all_independent_wrt Prob holds

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))

let Prob be Probability of Sigma; :: thesis: for A being SetSequence of Sigma

for n, n1, n2 being Nat st n > n1 & A is_all_independent_wrt Prob holds

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))

let A be SetSequence of Sigma; :: thesis: for n, n1, n2 being Nat st n > n1 & A is_all_independent_wrt Prob holds

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))

let n, n1, n2 be Nat; :: thesis: ( n > n1 & A is_all_independent_wrt Prob implies 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)) )

assume that

A1: n > n1 and

A2: A is_all_independent_wrt Prob ; :: thesis: 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))

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

proof

A17:
for m, m1, m2 being Element of NAT
let A, B be SetSequence of Sigma; :: thesis: 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 k, n be Element of NAT ; :: thesis: ( B = A * (Special_Function2 k) implies (Partial_Product (Prob * (A ^\ k))) . n = (Partial_Product (Prob * B)) . n )

assume A4: B = A * (Special_Function2 k) ; :: thesis: (Partial_Product (Prob * (A ^\ k))) . n = (Partial_Product (Prob * B)) . n

defpred S_{1}[ 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_{1}[ 0 ]
by A9, A7, A6, FUNCT_1:12;

A11: for q being Nat st S_{1}[q] holds

S_{1}[q + 1]
_{1}[k]
from NAT_1:sch 2(A10, A11);

hence (Partial_Product (Prob * (A ^\ k))) . n = (Partial_Product (Prob * B)) . n ; :: thesis: verum

end;(Partial_Product (Prob * (A ^\ k))) . n = (Partial_Product (Prob * B)) . n

let k, n be Element of NAT ; :: thesis: ( B = A * (Special_Function2 k) implies (Partial_Product (Prob * (A ^\ k))) . n = (Partial_Product (Prob * B)) . n )

assume A4: B = A * (Special_Function2 k) ; :: thesis: (Partial_Product (Prob * (A ^\ k))) . n = (Partial_Product (Prob * B)) . n

defpred S

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

A11: for q being Nat st S

S

proof

for k being Nat holds S
let q be Nat; :: thesis: ( S_{1}[q] implies S_{1}[q + 1] )

assume A12: S_{1}[q]
; :: thesis: S_{1}[q + 1]

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)_{1}[q + 1]
by A13, SERIES_3:def 1; :: thesis: verum

end;assume A12: S

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

hence
S
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: verum

end;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: verum

hence (Partial_Product (Prob * (A ^\ k))) . n = (Partial_Product (Prob * B)) . n ; :: thesis: verum

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

A25:
for m, m1 being Element of NAT
let m, m1, m2 be Element of NAT ; :: thesis: 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))

let e be sequence of NAT; :: thesis: 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))

let C, B be SetSequence of Sigma; :: thesis: ( m1 < m & e is one-to-one & C = A * e & B = C * (Special_Function (m1,m2)) implies Prob . ((Partial_Intersection B) . m) = ((Partial_Product (Prob * C)) . m1) * ((Partial_Product (Prob * (C ^\ ((m1 + m2) + 1)))) . ((m - m1) - 1)) )

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: Prob . ((Partial_Intersection B) . m) = ((Partial_Product (Prob * C)) . m1) * ((Partial_Product (Prob * (C ^\ ((m1 + m2) + 1)))) . ((m - m1) - 1))

( 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 ) )

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: verum

end;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))

let e be sequence of NAT; :: thesis: 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))

let C, B be SetSequence of Sigma; :: thesis: ( m1 < m & e is one-to-one & C = A * e & B = C * (Special_Function (m1,m2)) implies Prob . ((Partial_Intersection B) . m) = ((Partial_Product (Prob * C)) . m1) * ((Partial_Product (Prob * (C ^\ ((m1 + m2) + 1)))) . ((m - m1) - 1)) )

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: Prob . ((Partial_Intersection B) . m) = ((Partial_Product (Prob * C)) . m1) * ((Partial_Product (Prob * (C ^\ ((m1 + m2) + 1)))) . ((m - m1) - 1))

( 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

then
Prob . ((Partial_Intersection B) . m) = (Partial_Product (Prob * B)) . m
by A2;
for n being Nat holds A . ((e * (Special_Function (m1,m2))) . n) = B . n

end;proof

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: verum
let n be Nat; :: thesis: A . ((e * (Special_Function (m1,m2))) . n) = B . n

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: verum

end;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: verum

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: verum

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

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)
let m, m1 be Element of NAT ; :: thesis: 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

let e be sequence of NAT; :: thesis: 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

let C, B be SetSequence of Sigma; :: thesis: ( C = A * e & e is one-to-one & B = C * (Special_Function2 m1) implies Prob . ((Partial_Intersection B) . m) = (Partial_Product (Prob * (C ^\ m1))) . m )

assume that

A26: C = A * e and

A27: e is one-to-one and

A28: B = C * (Special_Function2 m1) ; :: thesis: Prob . ((Partial_Intersection B) . m) = (Partial_Product (Prob * (C ^\ m1))) . m

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 ) )

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

end;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

let e be sequence of NAT; :: thesis: 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

let C, B be SetSequence of Sigma; :: thesis: ( C = A * e & e is one-to-one & B = C * (Special_Function2 m1) implies Prob . ((Partial_Intersection B) . m) = (Partial_Product (Prob * (C ^\ m1))) . m )

assume that

A26: C = A * e and

A27: e is one-to-one and

A28: B = C * (Special_Function2 m1) ; :: thesis: Prob . ((Partial_Intersection B) . m) = (Partial_Product (Prob * (C ^\ m1))) . m

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

Prob . ((Partial_Intersection B) . m) = (Partial_Product (Prob * B)) . m
by A2, A29;
A30:
for n being Nat holds A . ((e * (Special_Function2 m1)) . n) = B . n

end;proof

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

reconsider n = n as Element of NAT by ORDINAL1:def 12;

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: verum

end;reconsider n = n as Element of NAT by ORDINAL1:def 12;

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: verum

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

proof

(n - n1) - 1 is Element of NAT
let q be Nat; :: thesis: 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)

defpred S_{1}[ 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_{1}[ 0 ]
_{1}[k] holds

S_{1}[k + 1]
_{1}[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 <> {} )

end;defpred S

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

proof

A59:
for k being Nat st S
let e be sequence of NAT; :: thesis: 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)) . 0) /\ ((Partial_Intersection (C ^\ ((0 + n2) + 1))) . q)) = ((Partial_Product (Prob * (Complement C))) . 0) * ((Partial_Product (Prob * (C ^\ ((0 + n2) + 1)))) . q)

let q, n2 be Nat; :: thesis: for C being SetSequence of Sigma st e is one-to-one & C = A * e holds

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)

let C be SetSequence of Sigma; :: thesis: ( e is one-to-one & C = A * e implies 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) )

assume A37: e is one-to-one ; :: thesis: ( not C = A * e or 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) )

assume A38: C = A * e ; :: thesis: 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)

Prob . (((Partial_Intersection (Complement C)) . 0) /\ ((Partial_Intersection (C ^\ ((0 + n2) + 1))) . q)) = Prob . (((Complement C) . 0) /\ ((Partial_Intersection (C ^\ ((0 + n2) + 1))) . q)) by PROB_3:21;

then Prob . (((Partial_Intersection (Complement C)) . 0) /\ ((Partial_Intersection (C ^\ ((0 + n2) + 1))) . q)) = Prob . (((C . 0) `) /\ ((Partial_Intersection (C ^\ ((0 + n2) + 1))) . q)) by PROB_1:def 2;

then Prob . (((Partial_Intersection (Complement C)) . 0) /\ ((Partial_Intersection (C ^\ ((0 + n2) + 1))) . q)) = Prob . ((Omega \ (C . 0)) /\ ((Partial_Intersection (C ^\ ((0 + n2) + 1))) . q)) by SUBSET_1:def 4;

then A39: Prob . (((Partial_Intersection (Complement C)) . 0) /\ ((Partial_Intersection (C ^\ ((0 + n2) + 1))) . q)) = Prob . ((Omega /\ ((Partial_Intersection (C ^\ ((0 + n2) + 1))) . q)) \ ((C . 0) /\ ((Partial_Intersection (C ^\ ((0 + n2) + 1))) . q))) by XBOOLE_1:111;

A40: Prob . (((Partial_Intersection (Complement C)) . 0) /\ ((Partial_Intersection (C ^\ ((0 + n2) + 1))) . q)) = Prob . (((Partial_Intersection (C ^\ ((0 + n2) + 1))) . q) \ ((C . 0) /\ ((Partial_Intersection (C ^\ ((0 + n2) + 1))) . q))) by A39, XBOOLE_1:28;

A41: Prob . (((Partial_Intersection (Complement C)) . 0) /\ ((Partial_Intersection (C ^\ ((0 + n2) + 1))) . q)) = (Prob . ((Partial_Intersection (C ^\ ((0 + n2) + 1))) . q)) - (Prob . ((C . 0) /\ ((Partial_Intersection (C ^\ ((0 + n2) + 1))) . q))) by A40, PROB_1:33, XBOOLE_1:17;

consider m1 being Element of NAT such that

A42: m1 = 0 ;

reconsider m = (m1 + 1) + q as Element of NAT by ORDINAL1:def 12;

reconsider m2 = n2 as Element of NAT by ORDINAL1:def 12;

consider B being SetSequence of Omega such that

A43: B = C * (Special_Function (m1,m2)) ;

reconsider B = B as SetSequence of Sigma by A43;

A44: ( m1 < m & C = A * e & B = C * (Special_Function (m1,m2)) )

then ((Partial_Product (Prob * C)) . 0) * ((Partial_Product (Prob * (C ^\ ((0 + n2) + 1)))) . q) = Prob . (((Partial_Intersection C) . 0) /\ ((Partial_Intersection (C ^\ ((0 + n2) + 1))) . q)) by A44, A37, A17, A42;

then (Prob . ((Partial_Intersection (C ^\ ((0 + n2) + 1))) . q)) - (((Partial_Product (Prob * C)) . 0) * ((Partial_Product (Prob * (C ^\ ((0 + n2) + 1)))) . q)) = (Prob . ((Partial_Intersection (C ^\ ((0 + n2) + 1))) . q)) - (Prob . ((C . 0) /\ ((Partial_Intersection (C ^\ ((0 + n2) + 1))) . q))) by PROB_3:21;

then A45: Prob . (((Partial_Intersection (Complement C)) . 0) /\ ((Partial_Intersection (C ^\ ((0 + n2) + 1))) . q)) = (Prob . ((Partial_Intersection (C ^\ ((0 + n2) + 1))) . q)) - (((Prob * C) . 0) * ((Partial_Product (Prob * (C ^\ ((0 + n2) + 1)))) . q)) by A41, SERIES_3:def 1;

(Prob * C) . 0 = 1 - ((Prob * (Complement C)) . 0)

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 C = A * e & B = C * (Special_Function2 k) holds

(Partial_Intersection (C ^\ k)) . n = (Partial_Intersection B) . n

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 A38, 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: verum

end;for C being SetSequence of Sigma st e is one-to-one & C = A * e holds

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)

let q, n2 be Nat; :: thesis: for C being SetSequence of Sigma st e is one-to-one & C = A * e holds

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)

let C be SetSequence of Sigma; :: thesis: ( e is one-to-one & C = A * e implies 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) )

assume A37: e is one-to-one ; :: thesis: ( not C = A * e or 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) )

assume A38: C = A * e ; :: thesis: 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)

Prob . (((Partial_Intersection (Complement C)) . 0) /\ ((Partial_Intersection (C ^\ ((0 + n2) + 1))) . q)) = Prob . (((Complement C) . 0) /\ ((Partial_Intersection (C ^\ ((0 + n2) + 1))) . q)) by PROB_3:21;

then Prob . (((Partial_Intersection (Complement C)) . 0) /\ ((Partial_Intersection (C ^\ ((0 + n2) + 1))) . q)) = Prob . (((C . 0) `) /\ ((Partial_Intersection (C ^\ ((0 + n2) + 1))) . q)) by PROB_1:def 2;

then Prob . (((Partial_Intersection (Complement C)) . 0) /\ ((Partial_Intersection (C ^\ ((0 + n2) + 1))) . q)) = Prob . ((Omega \ (C . 0)) /\ ((Partial_Intersection (C ^\ ((0 + n2) + 1))) . q)) by SUBSET_1:def 4;

then A39: Prob . (((Partial_Intersection (Complement C)) . 0) /\ ((Partial_Intersection (C ^\ ((0 + n2) + 1))) . q)) = Prob . ((Omega /\ ((Partial_Intersection (C ^\ ((0 + n2) + 1))) . q)) \ ((C . 0) /\ ((Partial_Intersection (C ^\ ((0 + n2) + 1))) . q))) by XBOOLE_1:111;

A40: Prob . (((Partial_Intersection (Complement C)) . 0) /\ ((Partial_Intersection (C ^\ ((0 + n2) + 1))) . q)) = Prob . (((Partial_Intersection (C ^\ ((0 + n2) + 1))) . q) \ ((C . 0) /\ ((Partial_Intersection (C ^\ ((0 + n2) + 1))) . q))) by A39, XBOOLE_1:28;

A41: Prob . (((Partial_Intersection (Complement C)) . 0) /\ ((Partial_Intersection (C ^\ ((0 + n2) + 1))) . q)) = (Prob . ((Partial_Intersection (C ^\ ((0 + n2) + 1))) . q)) - (Prob . ((C . 0) /\ ((Partial_Intersection (C ^\ ((0 + n2) + 1))) . q))) by A40, PROB_1:33, XBOOLE_1:17;

consider m1 being Element of NAT such that

A42: m1 = 0 ;

reconsider m = (m1 + 1) + q as Element of NAT by ORDINAL1:def 12;

reconsider m2 = n2 as Element of NAT by ORDINAL1:def 12;

consider B being SetSequence of Omega such that

A43: B = C * (Special_Function (m1,m2)) ;

reconsider B = B as SetSequence of Sigma by A43;

A44: ( m1 < m & C = A * e & B = C * (Special_Function (m1,m2)) )

proof

then
Prob . ((Partial_Intersection B) . m) = Prob . (((Partial_Intersection C) . m1) /\ ((Partial_Intersection (C ^\ ((m1 + m2) + 1))) . ((m - m1) - 1)))
by Th5;
( 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: verum

end;hence ( m1 < m & C = A * e & B = C * (Special_Function (m1,m2)) ) by A38, A43, XXREAL_0:2; :: thesis: verum

then ((Partial_Product (Prob * C)) . 0) * ((Partial_Product (Prob * (C ^\ ((0 + n2) + 1)))) . q) = Prob . (((Partial_Intersection C) . 0) /\ ((Partial_Intersection (C ^\ ((0 + n2) + 1))) . q)) by A44, A37, A17, A42;

then (Prob . ((Partial_Intersection (C ^\ ((0 + n2) + 1))) . q)) - (((Partial_Product (Prob * C)) . 0) * ((Partial_Product (Prob * (C ^\ ((0 + n2) + 1)))) . q)) = (Prob . ((Partial_Intersection (C ^\ ((0 + n2) + 1))) . q)) - (Prob . ((C . 0) /\ ((Partial_Intersection (C ^\ ((0 + n2) + 1))) . q))) by PROB_3:21;

then A45: Prob . (((Partial_Intersection (Complement C)) . 0) /\ ((Partial_Intersection (C ^\ ((0 + n2) + 1))) . q)) = (Prob . ((Partial_Intersection (C ^\ ((0 + n2) + 1))) . q)) - (((Prob * C) . 0) * ((Partial_Product (Prob * (C ^\ ((0 + n2) + 1)))) . q)) by A41, SERIES_3:def 1;

(Prob * C) . 0 = 1 - ((Prob * (Complement C)) . 0)

proof

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;
( 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: verum

end;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: verum

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 C = A * e & B = C * (Special_Function2 k) holds

(Partial_Intersection (C ^\ k)) . n = (Partial_Intersection B) . n

proof

q in NAT
by ORDINAL1:def 12;
let A, B, C be SetSequence of Sigma; :: thesis: 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

let k, n be Element of NAT ; :: thesis: 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

let e be sequence of NAT; :: thesis: ( C = A * e & B = C * (Special_Function2 k) implies (Partial_Intersection (C ^\ k)) . n = (Partial_Intersection B) . n )

assume C = A * e ; :: thesis: ( not B = C * (Special_Function2 k) or (Partial_Intersection (C ^\ k)) . n = (Partial_Intersection B) . n )

assume A50: B = C * (Special_Function2 k) ; :: thesis: (Partial_Intersection (C ^\ k)) . n = (Partial_Intersection B) . n

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 )

( x in (Partial_Intersection (C ^\ k)) . n iff x in (Partial_Intersection B) . n )

end;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

let k, n be Element of NAT ; :: thesis: 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

let e be sequence of NAT; :: thesis: ( C = A * e & B = C * (Special_Function2 k) implies (Partial_Intersection (C ^\ k)) . n = (Partial_Intersection B) . n )

assume C = A * e ; :: thesis: ( not B = C * (Special_Function2 k) or (Partial_Intersection (C ^\ k)) . n = (Partial_Intersection B) . n )

assume A50: B = C * (Special_Function2 k) ; :: thesis: (Partial_Intersection (C ^\ k)) . n = (Partial_Intersection B) . n

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

for x being object holds
let x be set ; :: thesis: ( ( 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 )

x in B . knat ; :: thesis: for knat being Nat st knat <= n holds

x in (C ^\ k) . knat

thus for knat being Nat st knat <= n holds

x in (C ^\ k) . knat :: thesis: verum

end;x in (C ^\ k) . knat ) iff for knat being Nat st knat <= n holds

x in B . knat )

hereby :: thesis: ( ( for knat being Nat st knat <= n holds

x in B . knat ) implies for knat being Nat st knat <= n holds

x in (C ^\ k) . knat )

assume A55:
for knat being Nat st knat <= n holds x in B . knat ) implies for knat being Nat st knat <= n holds

x in (C ^\ k) . knat )

assume A52:
for knat being Nat st knat <= n holds

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

x in B . knat

thus for knat being Nat st knat <= n holds

x in B . knat :: thesis: verum

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

x in B . knat

thus for knat being Nat st knat <= n holds

x in B . knat :: thesis: verum

proof

let knat be Nat; :: thesis: ( knat <= n implies x in B . knat )

assume A53: knat <= n ; :: thesis: x in B . knat

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: verum

end;assume A53: knat <= n ; :: thesis: x in B . knat

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: verum

x in B . knat ; :: thesis: for knat being Nat st knat <= n holds

x in (C ^\ k) . knat

thus for knat being Nat st knat <= n holds

x in (C ^\ k) . knat :: thesis: verum

proof

let knat be Nat; :: thesis: ( knat <= n implies x in (C ^\ k) . knat )

assume A56: knat <= n ; :: thesis: x in (C ^\ k) . knat

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: verum

end;assume A56: knat <= n ; :: thesis: x in (C ^\ k) . knat

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: verum

( x in (Partial_Intersection (C ^\ k)) . n iff x in (Partial_Intersection B) . n )

proof

hence
(Partial_Intersection (C ^\ k)) . n = (Partial_Intersection B) . n
by TARSKI:2; :: thesis: verum
let x be object ; :: thesis: ( x in (Partial_Intersection (C ^\ k)) . n iff x in (Partial_Intersection B) . n )

( ( 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: verum

end;( ( 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: verum

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 A38, 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: verum

S

proof

A132:
for k being Nat holds S
let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume A60: S_{1}[k]
; :: thesis: S_{1}[k + 1]

let e be sequence of NAT; :: thesis: 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)) . (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)

let q, n2 be Nat; :: thesis: for C being SetSequence of Sigma st e is one-to-one & C = A * e holds

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)

let C be SetSequence of Sigma; :: thesis: ( e is one-to-one & C = A * e implies 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) )

assume A61: e is one-to-one ; :: thesis: ( not C = A * e or 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) )

assume A62: C = A * e ; :: thesis: 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)

Prob . (((Partial_Intersection (Complement C)) . (k + 1)) /\ ((Partial_Intersection (C ^\ (((k + 1) + n2) + 1))) . q)) = Prob . ((((Partial_Intersection (Complement C)) . k) /\ ((Complement C) . (k + 1))) /\ ((Partial_Intersection (C ^\ (((k + 1) + n2) + 1))) . q)) by PROB_3:21;

then Prob . (((Partial_Intersection (Complement C)) . (k + 1)) /\ ((Partial_Intersection (C ^\ (((k + 1) + n2) + 1))) . q)) = Prob . ((((C . (k + 1)) `) /\ ((Partial_Intersection (Complement C)) . k)) /\ ((Partial_Intersection (C ^\ (((k + 1) + n2) + 1))) . q)) by PROB_1:def 2;

then Prob . (((Partial_Intersection (Complement C)) . (k + 1)) /\ ((Partial_Intersection (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;

then Prob . (((Partial_Intersection (Complement C)) . (k + 1)) /\ ((Partial_Intersection (C ^\ (((k + 1) + n2) + 1))) . q)) = Prob . ((Omega \ (C . (k + 1))) /\ (((Partial_Intersection (Complement C)) . k) /\ ((Partial_Intersection (C ^\ (((k + 1) + n2) + 1))) . q))) by SUBSET_1:def 4;

then A63: Prob . (((Partial_Intersection (Complement C)) . (k + 1)) /\ ((Partial_Intersection (C ^\ (((k + 1) + n2) + 1))) . q)) = Prob . ((Omega /\ (((Partial_Intersection (Complement C)) . k) /\ ((Partial_Intersection (C ^\ (((k + 1) + n2) + 1))) . q))) \ ((C . (k + 1)) /\ (((Partial_Intersection (Complement C)) . k) /\ ((Partial_Intersection (C ^\ (((k + 1) + n2) + 1))) . q)))) by XBOOLE_1:50;

A64: Prob . (((Partial_Intersection (Complement C)) . (k + 1)) /\ ((Partial_Intersection (C ^\ (((k + 1) + n2) + 1))) . q)) = Prob . ((((Partial_Intersection (Complement C)) . k) /\ ((Partial_Intersection (C ^\ (((k + 1) + n2) + 1))) . q)) \ ((C . (k + 1)) /\ (((Partial_Intersection (Complement C)) . k) /\ ((Partial_Intersection (C ^\ (((k + 1) + n2) + 1))) . q)))) by A63, XBOOLE_1:28;

A65: 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)

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: verum

end;assume A60: S

let e be sequence of NAT; :: thesis: 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)) . (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)

let q, n2 be Nat; :: thesis: for C being SetSequence of Sigma st e is one-to-one & C = A * e holds

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)

let C be SetSequence of Sigma; :: thesis: ( e is one-to-one & C = A * e implies 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) )

assume A61: e is one-to-one ; :: thesis: ( not C = A * e or 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) )

assume A62: C = A * e ; :: thesis: 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)

Prob . (((Partial_Intersection (Complement C)) . (k + 1)) /\ ((Partial_Intersection (C ^\ (((k + 1) + n2) + 1))) . q)) = Prob . ((((Partial_Intersection (Complement C)) . k) /\ ((Complement C) . (k + 1))) /\ ((Partial_Intersection (C ^\ (((k + 1) + n2) + 1))) . q)) by PROB_3:21;

then Prob . (((Partial_Intersection (Complement C)) . (k + 1)) /\ ((Partial_Intersection (C ^\ (((k + 1) + n2) + 1))) . q)) = Prob . ((((C . (k + 1)) `) /\ ((Partial_Intersection (Complement C)) . k)) /\ ((Partial_Intersection (C ^\ (((k + 1) + n2) + 1))) . q)) by PROB_1:def 2;

then Prob . (((Partial_Intersection (Complement C)) . (k + 1)) /\ ((Partial_Intersection (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;

then Prob . (((Partial_Intersection (Complement C)) . (k + 1)) /\ ((Partial_Intersection (C ^\ (((k + 1) + n2) + 1))) . q)) = Prob . ((Omega \ (C . (k + 1))) /\ (((Partial_Intersection (Complement C)) . k) /\ ((Partial_Intersection (C ^\ (((k + 1) + n2) + 1))) . q))) by SUBSET_1:def 4;

then A63: Prob . (((Partial_Intersection (Complement C)) . (k + 1)) /\ ((Partial_Intersection (C ^\ (((k + 1) + n2) + 1))) . q)) = Prob . ((Omega /\ (((Partial_Intersection (Complement C)) . k) /\ ((Partial_Intersection (C ^\ (((k + 1) + n2) + 1))) . q))) \ ((C . (k + 1)) /\ (((Partial_Intersection (Complement C)) . k) /\ ((Partial_Intersection (C ^\ (((k + 1) + n2) + 1))) . q)))) by XBOOLE_1:50;

A64: Prob . (((Partial_Intersection (Complement C)) . (k + 1)) /\ ((Partial_Intersection (C ^\ (((k + 1) + n2) + 1))) . q)) = Prob . ((((Partial_Intersection (Complement C)) . k) /\ ((Partial_Intersection (C ^\ (((k + 1) + n2) + 1))) . q)) \ ((C . (k + 1)) /\ (((Partial_Intersection (Complement C)) . k) /\ ((Partial_Intersection (C ^\ (((k + 1) + n2) + 1))) . q)))) by A63, XBOOLE_1:28;

A65: 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)

proof

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))
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: verum

end;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: verum

proof

(Prob * C) . (k + 1) = 1 - ((Prob * (Complement C)) . (k + 1))
(((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)))

end;proof

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: verum
consider F being SetSequence of Omega such that

A67: F = C * (Special_Function4 (k,n2)) ;

F is 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

A76: (Partial_Intersection (Complement C)) . k = (Partial_Intersection (Complement F)) . k_{2}[ 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_{2}[ 0 ]
by A119, SERIES_3:def 1;

A121: for q being Nat st S_{2}[q] holds

S_{2}[q + 1]
_{2}[k]
from NAT_1:sch 2(A120, A121);

for q being Element of NAT st q <= k holds

C . q = F . q

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: verum

end;A67: F = C * (Special_Function4 (k,n2)) ;

F is SetSequence of Sigma

proof

then reconsider F = F as SetSequence of Sigma ;
for n being Nat holds F . n is Event of Sigma

end;proof

hence
F is SetSequence of Sigma
by PROB_1:25; :: thesis: verum
let n be Nat; :: thesis: F . n is Event of Sigma

A68: n in NAT by ORDINAL1:def 12;

A69: dom (C * (Special_Function4 (k,n2))) = NAT by FUNCT_2:def 1;

F . n = C . ((Special_Function4 (k,n2)) . n) by A67, A69, FUNCT_1:12, A68;

hence F . n is Event of Sigma ; :: thesis: verum

end;A68: n in NAT by ORDINAL1:def 12;

A69: dom (C * (Special_Function4 (k,n2))) = NAT by FUNCT_2:def 1;

F . n = C . ((Special_Function4 (k,n2)) . n) by A67, A69, FUNCT_1:12, A68;

hence F . n is Event of Sigma ; :: thesis: verum

( 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

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;
let q be object ; :: thesis: ( q in NAT implies F . q = (A * f) . q )

assume q in NAT ; :: thesis: F . q = (A * f) . q

then reconsider q = q as Element of NAT ;

dom (A * e) = NAT by FUNCT_2:def 1;

then A72: (A * e) . ((Special_Function4 (k,n2)) . q) = A . (e . ((Special_Function4 (k,n2)) . q)) by FUNCT_1:12;

dom ((A * e) * (Special_Function4 (k,n2))) = NAT by FUNCT_2:def 1;

then A73: ((A * e) * (Special_Function4 (k,n2))) . q = A . (e . ((Special_Function4 (k,n2)) . q)) by A72, FUNCT_1:12;

dom (e * (Special_Function4 (k,n2))) = NAT by FUNCT_2:def 1;

then A74: ((A * e) * (Special_Function4 (k,n2))) . q = A . ((e * (Special_Function4 (k,n2))) . q) by A73, FUNCT_1:12;

dom (A * f) = NAT by FUNCT_2:def 1;

hence F . q = (A * f) . q by A70, A74, A62, A67, FUNCT_1:12; :: thesis: verum

end;assume q in NAT ; :: thesis: F . q = (A * f) . q

then reconsider q = q as Element of NAT ;

dom (A * e) = NAT by FUNCT_2:def 1;

then A72: (A * e) . ((Special_Function4 (k,n2)) . q) = A . (e . ((Special_Function4 (k,n2)) . q)) by FUNCT_1:12;

dom ((A * e) * (Special_Function4 (k,n2))) = NAT by FUNCT_2:def 1;

then A73: ((A * e) * (Special_Function4 (k,n2))) . q = A . (e . ((Special_Function4 (k,n2)) . q)) by A72, FUNCT_1:12;

dom (e * (Special_Function4 (k,n2))) = NAT by FUNCT_2:def 1;

then A74: ((A * e) * (Special_Function4 (k,n2))) . q = A . ((e * (Special_Function4 (k,n2))) . q) by A73, FUNCT_1:12;

dom (A * f) = NAT by FUNCT_2:def 1;

hence F . q = (A * f) . q by A70, A74, A62, A67, FUNCT_1:12; :: thesis: verum

A76: (Partial_Intersection (Complement C)) . k = (Partial_Intersection (Complement F)) . k

proof

A85:
(Partial_Intersection (F ^\ (k + 1))) . (q + 1) = (C . (k + 1)) /\ ((Partial_Intersection (C ^\ (((k + 1) + n2) + 1))) . q)
A77:
for x being set

for knat being Nat st knat <= k holds

( x in (Complement C) . knat iff x in (Complement F) . knat )

( ( 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 )

( x in (Partial_Intersection (Complement C)) . k iff x in (Partial_Intersection (Complement F)) . k )

end;for knat being Nat st knat <= k holds

( x in (Complement C) . knat iff x in (Complement F) . knat )

proof

A80:
for x being object holds
let x be set ; :: thesis: for knat being Nat st knat <= k holds

( x in (Complement C) . knat iff x in (Complement F) . knat )

let knat be Nat; :: thesis: ( knat <= k implies ( x in (Complement C) . knat iff x in (Complement F) . knat ) )

assume knat <= k ; :: thesis: ( x in (Complement C) . knat iff x in (Complement F) . knat )

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: verum

end;( x in (Complement C) . knat iff x in (Complement F) . knat )

let knat be Nat; :: thesis: ( knat <= k implies ( x in (Complement C) . knat iff x in (Complement F) . knat ) )

assume knat <= k ; :: thesis: ( x in (Complement C) . knat iff x in (Complement F) . knat )

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: verum

( ( 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

for x being object holds
let x be object ; :: thesis: ( ( 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 )

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

x in (Complement C) . knat

thus for knat being Nat st knat <= k holds

x in (Complement C) . knat :: thesis: verum

end;x in (Complement C) . knat ) iff for knat being Nat st knat <= k holds

x in (Complement F) . knat )

hereby :: thesis: ( ( for knat being Nat st knat <= k holds

x in (Complement F) . knat ) implies for knat being Nat st knat <= k holds

x in (Complement C) . knat )

assume A83:
for knat being Nat st knat <= k holds x in (Complement F) . knat ) implies for knat being Nat st knat <= k holds

x in (Complement C) . knat )

assume A81:
for knat being Nat st knat <= k holds

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

x in (Complement F) . knat

thus for knat being Nat st knat <= k holds

x in (Complement F) . knat :: thesis: verum

end;x in (Complement C) . knat ; :: thesis: for knat being Nat st knat <= k holds

x in (Complement F) . knat

thus for knat being Nat st knat <= k holds

x in (Complement F) . knat :: thesis: verum

proof

let knat be Nat; :: thesis: ( knat <= k implies x in (Complement F) . knat )

assume A82: knat <= k ; :: thesis: x in (Complement F) . knat

then ( x in (Complement C) . knat iff x in (Complement F) . knat ) by A77;

hence x in (Complement F) . knat by A82, A81; :: thesis: verum

end;assume A82: knat <= k ; :: thesis: x in (Complement F) . knat

then ( x in (Complement C) . knat iff x in (Complement F) . knat ) by A77;

hence x in (Complement F) . knat by A82, A81; :: thesis: verum

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

x in (Complement C) . knat

thus for knat being Nat st knat <= k holds

x in (Complement C) . knat :: thesis: verum

proof

let knat be Nat; :: thesis: ( knat <= k implies x in (Complement C) . knat )

assume A84: knat <= k ; :: thesis: x in (Complement C) . knat

then ( x in (Complement C) . knat iff x in (Complement F) . knat ) by A77;

hence x in (Complement C) . knat by A84, A83; :: thesis: verum

end;assume A84: knat <= k ; :: thesis: x in (Complement C) . knat

then ( x in (Complement C) . knat iff x in (Complement F) . knat ) by A77;

hence x in (Complement C) . knat by A84, A83; :: thesis: verum

( x in (Partial_Intersection (Complement C)) . k iff x in (Partial_Intersection (Complement F)) . k )

proof

hence
(Partial_Intersection (Complement C)) . k = (Partial_Intersection (Complement F)) . k
by TARSKI:2; :: thesis: verum
let x be object ; :: thesis: ( x in (Partial_Intersection (Complement C)) . k iff x in (Partial_Intersection (Complement F)) . k )

( 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: verum

end;( 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: verum

proof

A100:
(Partial_Product (Prob * (F ^\ (k + 1)))) . (q + 1) = ((Prob * C) . (k + 1)) * ((Partial_Product (Prob * (C ^\ (((k + 1) + n2) + 1)))) . q)
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 )

( ( 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 )

( x in (Partial_Intersection (C ^\ (((k + 1) + n2) + 1))) . q iff x in (Partial_Intersection (F ^\ ((k + 1) + 1))) . q )

end;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

A88:
for x being object holds
let x be set ; :: thesis: for knat being Nat st knat <= q holds

( x in (F ^\ ((k + 1) + 1)) . knat iff x in (C ^\ (((k + 1) + n2) + 1)) . knat )

let knat be Nat; :: thesis: ( knat <= q implies ( x in (F ^\ ((k + 1) + 1)) . knat iff x in (C ^\ (((k + 1) + n2) + 1)) . knat ) )

assume knat <= q ; :: thesis: ( x in (F ^\ ((k + 1) + 1)) . knat iff x in (C ^\ (((k + 1) + n2) + 1)) . knat )

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

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: verum

end;( x in (F ^\ ((k + 1) + 1)) . knat iff x in (C ^\ (((k + 1) + n2) + 1)) . knat )

let knat be Nat; :: thesis: ( knat <= q implies ( x in (F ^\ ((k + 1) + 1)) . knat iff x in (C ^\ (((k + 1) + n2) + 1)) . knat ) )

assume knat <= q ; :: thesis: ( x in (F ^\ ((k + 1) + 1)) . knat iff x in (C ^\ (((k + 1) + n2) + 1)) . knat )

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

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;
( 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: verum

end;hence ((knat + k) + 1) + 1 > k + 1 by XXREAL_0:2; :: thesis: verum

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: verum

( ( 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

A93:
for x being object holds
let x be object ; :: thesis: ( ( 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 )

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

x in (C ^\ (((k + 1) + n2) + 1)) . knat

thus for knat being Nat st knat <= q holds

x in (C ^\ (((k + 1) + n2) + 1)) . knat :: thesis: verum

end;x in (C ^\ (((k + 1) + n2) + 1)) . knat ) iff for knat being Nat st knat <= q holds

x in (F ^\ ((k + 1) + 1)) . knat )

hereby :: thesis: ( ( for knat being Nat st knat <= q holds

x in (F ^\ ((k + 1) + 1)) . knat ) implies for knat being Nat st knat <= q holds

x in (C ^\ (((k + 1) + n2) + 1)) . knat )

assume A91:
for knat being Nat st knat <= q holds x in (F ^\ ((k + 1) + 1)) . knat ) implies for knat being Nat st knat <= q holds

x in (C ^\ (((k + 1) + n2) + 1)) . knat )

assume A89:
for knat being Nat st knat <= q holds

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

x in (F ^\ ((k + 1) + 1)) . knat

thus for knat being Nat st knat <= q holds

x in (F ^\ ((k + 1) + 1)) . knat :: thesis: verum

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

x in (F ^\ ((k + 1) + 1)) . knat

thus for knat being Nat st knat <= q holds

x in (F ^\ ((k + 1) + 1)) . knat :: thesis: verum

proof

let knat be Nat; :: thesis: ( knat <= q implies x in (F ^\ ((k + 1) + 1)) . knat )

assume A90: knat <= q ; :: thesis: x in (F ^\ ((k + 1) + 1)) . knat

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: verum

end;assume A90: knat <= q ; :: thesis: x in (F ^\ ((k + 1) + 1)) . knat

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: verum

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

x in (C ^\ (((k + 1) + n2) + 1)) . knat

thus for knat being Nat st knat <= q holds

x in (C ^\ (((k + 1) + n2) + 1)) . knat :: thesis: verum

proof

let knat be Nat; :: thesis: ( knat <= q implies x in (C ^\ (((k + 1) + n2) + 1)) . knat )

assume A92: knat <= q ; :: thesis: x in (C ^\ (((k + 1) + n2) + 1)) . knat

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: verum

end;assume A92: knat <= q ; :: thesis: x in (C ^\ (((k + 1) + n2) + 1)) . knat

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: verum

( x in (Partial_Intersection (C ^\ (((k + 1) + n2) + 1))) . q iff x in (Partial_Intersection (F ^\ ((k + 1) + 1))) . q )

proof

((Partial_Intersection (F ^\ ((k + 1) + 1))) . q) /\ (C . (k + 1)) = (Partial_Intersection (F ^\ (k + 1))) . (q + 1)
let x be object ; :: thesis: ( x in (Partial_Intersection (C ^\ (((k + 1) + n2) + 1))) . q iff x in (Partial_Intersection (F ^\ ((k + 1) + 1))) . q )

( 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: verum

end;( 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: verum

proof

hence
(Partial_Intersection (F ^\ (k + 1))) . (q + 1) = (C . (k + 1)) /\ ((Partial_Intersection (C ^\ (((k + 1) + n2) + 1))) . q)
by A93, TARSKI:2; :: thesis: verum
defpred S_{2}[ Nat] means ((Partial_Intersection (F ^\ ((k + 1) + 1))) . $1) /\ (C . (k + 1)) = (Partial_Intersection (F ^\ (k + 1))) . ($1 + 1);

A94: S_{2}[ 0 ]
_{2}[q] holds

S_{2}[q + 1]
_{2}[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: verum

end;A94: S

proof

A97:
for q being Nat st S
((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_{2}[ 0 ]
by PROB_3:21; :: thesis: verum

end;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

S

proof

for k being Nat holds S
let q be Nat; :: thesis: ( S_{2}[q] implies S_{2}[q + 1] )

assume A98: S_{2}[q]
; :: thesis: S_{2}[q + 1]

((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)_{2}[q + 1]
by A99, PROB_3:21; :: thesis: verum

end;assume A98: S

((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

hence
S
(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: verum

end;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: verum

hence ((Partial_Intersection (F ^\ ((k + 1) + 1))) . q) /\ (C . (k + 1)) = (Partial_Intersection (F ^\ (k + 1))) . (q + 1) ; :: thesis: verum

proof

defpred S
defpred S_{2}[ 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_{2}[ 0 ]
_{2}[q] holds

S_{2}[q + 1]
_{2}[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: verum

end;A101: S

proof

A111:
for q being Nat st S
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)

hence S_{2}[ 0 ]
by SERIES_3:def 1; :: thesis: verum

end;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

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;
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: verum

end;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: verum

hence S

S

proof

for k being Nat holds S
let q be Nat; :: thesis: ( S_{2}[q] implies S_{2}[q + 1] )

assume A112: S_{2}[q]
; :: thesis: S_{2}[q + 1]

A113: (Prob * (F ^\ (k + 1))) . ((q + 1) + 1) = (Prob * (C ^\ (((k + 1) + n2) + 1))) . (q + 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_{2}[q + 1]
by SERIES_3:def 1; :: thesis: verum

end;assume A112: S

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

proof

(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;
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

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: verum

end;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

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;
( 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: verum

end;hence ((q + 1) + 1) + (k + 1) > k + 1 by XXREAL_0:2; :: thesis: verum

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: verum

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

hence (Partial_Product (Prob * (F ^\ (k + 1)))) . (q + 1) = ((Prob * C) . (k + 1)) * ((Partial_Product (Prob * (C ^\ (((k + 1) + n2) + 1)))) . q) ; :: thesis: verum

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

A121: for q being Nat st S

S

proof

A127:
for k being Nat holds S
let q be Nat; :: thesis: ( S_{2}[q] implies S_{2}[q + 1] )

assume A122: S_{2}[q]
; :: thesis: S_{2}[q + 1]

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 )

C . k = F . k ) implies (Partial_Product (Prob * (Complement F))) . (q + 1) = (Partial_Product (Prob * (Complement C))) . (q + 1) )_{2}[q + 1]
; :: thesis: verum

end;assume A122: S

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

( ( for k being Element of NAT st k <= q + 1 holds
assume A124:
for k being Element of NAT st k <= q + 1 holds

C . k = F . k ; :: thesis: for k being Element of NAT st k <= q holds

C . k = F . k

let k be Element of NAT ; :: thesis: ( k <= q implies C . k = F . k )

assume k <= q ; :: thesis: C . k = F . k

then k <= q + 1 by NAT_1:13;

hence C . k = F . k by A124; :: thesis: verum

end;C . k = F . k ; :: thesis: for k being Element of NAT st k <= q holds

C . k = F . k

let k be Element of NAT ; :: thesis: ( k <= q implies C . k = F . k )

assume k <= q ; :: thesis: C . k = F . k

then k <= q + 1 by NAT_1:13;

hence C . k = F . k by A124; :: thesis: verum

C . k = F . k ) implies (Partial_Product (Prob * (Complement F))) . (q + 1) = (Partial_Product (Prob * (Complement C))) . (q + 1) )

proof

hence
S
assume A125:
for k being Element of NAT st k <= q + 1 holds

C . k = F . k ; :: thesis: (Partial_Product (Prob * (Complement F))) . (q + 1) = (Partial_Product (Prob * (Complement C))) . (q + 1)

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: verum

end;C . k = F . k ; :: thesis: (Partial_Product (Prob * (Complement F))) . (q + 1) = (Partial_Product (Prob * (Complement C))) . (q + 1)

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: verum

for q being Element of NAT st q <= k holds

C . q = F . q

proof

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;
let q be Element of NAT ; :: thesis: ( q <= k implies C . q = F . q )

assume q <= k ; :: thesis: C . q = F . q

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: verum

end;assume q <= k ; :: thesis: C . q = F . q

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: verum

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: verum

proof

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;
( 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: verum

end;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: verum

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: verum

ex e being sequence of NAT st

( A * e = A & e is one-to-one & dom e <> {} )

proof

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: verum
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 ) )

( A * e = A & e is one-to-one & dom e <> {} ) by A133, FUNCT_2:12; :: thesis: verum

end;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

hence
ex e being sequence of NAT st
A134:
for n being object st n in NAT holds

( (A * (Special_Function2 0)) . n = A . n & A . ((Special_Function2 0) . n) = A . n )

(A * (Special_Function2 0)) . n = A . n ) ) by A134; :: thesis: verum

end;( (A * (Special_Function2 0)) . n = A . n & A . ((Special_Function2 0) . n) = A . n )

proof

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

assume n in NAT ; :: thesis: ( (A * (Special_Function2 0)) . n = A . n & A . ((Special_Function2 0) . n) = A . n )

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: verum

end;assume n in NAT ; :: thesis: ( (A * (Special_Function2 0)) . n = A . n & A . ((Special_Function2 0) . n) = A . n )

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: verum

(A * (Special_Function2 0)) . n = A . n ) ) by A134; :: thesis: verum

( A * e = A & e is one-to-one & dom e <> {} ) by A133, FUNCT_2:12; :: thesis: verum

proof

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: verum
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: verum

end;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: verum