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

for Prob being Probability of Sigma

for n, n1, n2 being Nat holds

( ( for A, B being SetSequence of Sigma st n > n1 & B = A * (Special_Function (n1,n2)) holds

(Partial_Product (Prob * B)) . n = ((Partial_Product (Prob * A)) . n1) * ((Partial_Product (Prob * (A ^\ ((n1 + n2) + 1)))) . ((n - n1) - 1)) ) & ( for A, B, C being SetSequence of Sigma

for e being sequence of NAT st n > n1 & C = A * e & B = C * (Special_Function (n1,n2)) holds

(Partial_Intersection B) . n = ((Partial_Intersection C) . n1) /\ ((Partial_Intersection (C ^\ ((n1 + n2) + 1))) . ((n - n1) - 1)) ) )

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

for n, n1, n2 being Nat holds

( ( for A, B being SetSequence of Sigma st n > n1 & B = A * (Special_Function (n1,n2)) holds

(Partial_Product (Prob * B)) . n = ((Partial_Product (Prob * A)) . n1) * ((Partial_Product (Prob * (A ^\ ((n1 + n2) + 1)))) . ((n - n1) - 1)) ) & ( for A, B, C being SetSequence of Sigma

for e being sequence of NAT st n > n1 & C = A * e & B = C * (Special_Function (n1,n2)) holds

(Partial_Intersection B) . n = ((Partial_Intersection C) . n1) /\ ((Partial_Intersection (C ^\ ((n1 + n2) + 1))) . ((n - n1) - 1)) ) )

let Prob be Probability of Sigma; :: thesis: for n, n1, n2 being Nat holds

( ( for A, B being SetSequence of Sigma st n > n1 & B = A * (Special_Function (n1,n2)) holds

(Partial_Product (Prob * B)) . n = ((Partial_Product (Prob * A)) . n1) * ((Partial_Product (Prob * (A ^\ ((n1 + n2) + 1)))) . ((n - n1) - 1)) ) & ( for A, B, C being SetSequence of Sigma

for e being sequence of NAT st n > n1 & C = A * e & B = C * (Special_Function (n1,n2)) holds

(Partial_Intersection B) . n = ((Partial_Intersection C) . n1) /\ ((Partial_Intersection (C ^\ ((n1 + n2) + 1))) . ((n - n1) - 1)) ) )

let n, n1, n2 be Nat; :: thesis: ( ( for A, B being SetSequence of Sigma st n > n1 & B = A * (Special_Function (n1,n2)) holds

(Partial_Product (Prob * B)) . n = ((Partial_Product (Prob * A)) . n1) * ((Partial_Product (Prob * (A ^\ ((n1 + n2) + 1)))) . ((n - n1) - 1)) ) & ( for A, B, C being SetSequence of Sigma

for e being sequence of NAT st n > n1 & C = A * e & B = C * (Special_Function (n1,n2)) holds

(Partial_Intersection B) . n = ((Partial_Intersection C) . n1) /\ ((Partial_Intersection (C ^\ ((n1 + n2) + 1))) . ((n - n1) - 1)) ) )

A1: for A, B being SetSequence of Sigma st n > n1 & B = A * (Special_Function (n1,n2)) holds

(Partial_Product (Prob * B)) . n = ((Partial_Product (Prob * A)) . n1) * ((Partial_Product (Prob * (A ^\ ((n1 + n2) + 1)))) . ((n - n1) - 1))

for n1, n2, n being Nat

for e being sequence of NAT st n > n1 & C = A * e & B = C * (Special_Function (n1,n2)) holds

(Partial_Intersection B) . n = ((Partial_Intersection C) . n1) /\ ((Partial_Intersection (C ^\ ((n1 + n2) + 1))) . ((n - n1) - 1))

(Partial_Product (Prob * B)) . n = ((Partial_Product (Prob * A)) . n1) * ((Partial_Product (Prob * (A ^\ ((n1 + n2) + 1)))) . ((n - n1) - 1)) ) & ( for A, B, C being SetSequence of Sigma

for e being sequence of NAT st n > n1 & C = A * e & B = C * (Special_Function (n1,n2)) holds

(Partial_Intersection B) . n = ((Partial_Intersection C) . n1) /\ ((Partial_Intersection (C ^\ ((n1 + n2) + 1))) . ((n - n1) - 1)) ) ) by A1; :: thesis: verum

for Prob being Probability of Sigma

for n, n1, n2 being Nat holds

( ( for A, B being SetSequence of Sigma st n > n1 & B = A * (Special_Function (n1,n2)) holds

(Partial_Product (Prob * B)) . n = ((Partial_Product (Prob * A)) . n1) * ((Partial_Product (Prob * (A ^\ ((n1 + n2) + 1)))) . ((n - n1) - 1)) ) & ( for A, B, C being SetSequence of Sigma

for e being sequence of NAT st n > n1 & C = A * e & B = C * (Special_Function (n1,n2)) holds

(Partial_Intersection B) . n = ((Partial_Intersection C) . n1) /\ ((Partial_Intersection (C ^\ ((n1 + n2) + 1))) . ((n - n1) - 1)) ) )

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

for n, n1, n2 being Nat holds

( ( for A, B being SetSequence of Sigma st n > n1 & B = A * (Special_Function (n1,n2)) holds

(Partial_Product (Prob * B)) . n = ((Partial_Product (Prob * A)) . n1) * ((Partial_Product (Prob * (A ^\ ((n1 + n2) + 1)))) . ((n - n1) - 1)) ) & ( for A, B, C being SetSequence of Sigma

for e being sequence of NAT st n > n1 & C = A * e & B = C * (Special_Function (n1,n2)) holds

(Partial_Intersection B) . n = ((Partial_Intersection C) . n1) /\ ((Partial_Intersection (C ^\ ((n1 + n2) + 1))) . ((n - n1) - 1)) ) )

let Prob be Probability of Sigma; :: thesis: for n, n1, n2 being Nat holds

( ( for A, B being SetSequence of Sigma st n > n1 & B = A * (Special_Function (n1,n2)) holds

(Partial_Product (Prob * B)) . n = ((Partial_Product (Prob * A)) . n1) * ((Partial_Product (Prob * (A ^\ ((n1 + n2) + 1)))) . ((n - n1) - 1)) ) & ( for A, B, C being SetSequence of Sigma

for e being sequence of NAT st n > n1 & C = A * e & B = C * (Special_Function (n1,n2)) holds

(Partial_Intersection B) . n = ((Partial_Intersection C) . n1) /\ ((Partial_Intersection (C ^\ ((n1 + n2) + 1))) . ((n - n1) - 1)) ) )

let n, n1, n2 be Nat; :: thesis: ( ( for A, B being SetSequence of Sigma st n > n1 & B = A * (Special_Function (n1,n2)) holds

(Partial_Product (Prob * B)) . n = ((Partial_Product (Prob * A)) . n1) * ((Partial_Product (Prob * (A ^\ ((n1 + n2) + 1)))) . ((n - n1) - 1)) ) & ( for A, B, C being SetSequence of Sigma

for e being sequence of NAT st n > n1 & C = A * e & B = C * (Special_Function (n1,n2)) holds

(Partial_Intersection B) . n = ((Partial_Intersection C) . n1) /\ ((Partial_Intersection (C ^\ ((n1 + n2) + 1))) . ((n - n1) - 1)) ) )

A1: for A, B being SetSequence of Sigma st n > n1 & B = A * (Special_Function (n1,n2)) holds

(Partial_Product (Prob * B)) . n = ((Partial_Product (Prob * A)) . n1) * ((Partial_Product (Prob * (A ^\ ((n1 + n2) + 1)))) . ((n - n1) - 1))

proof

for A, B, C being SetSequence of Sigma
let A, B be SetSequence of Sigma; :: thesis: ( n > n1 & B = A * (Special_Function (n1,n2)) implies (Partial_Product (Prob * B)) . n = ((Partial_Product (Prob * A)) . n1) * ((Partial_Product (Prob * (A ^\ ((n1 + n2) + 1)))) . ((n - n1) - 1)) )

assume that

A2: n > n1 and

A3: B = A * (Special_Function (n1,n2)) ; :: thesis: (Partial_Product (Prob * B)) . n = ((Partial_Product (Prob * A)) . n1) * ((Partial_Product (Prob * (A ^\ ((n1 + n2) + 1)))) . ((n - n1) - 1))

A4: for q being Element of NAT st q <= n1 holds

(Partial_Product (Prob * B)) . q = (Partial_Product (Prob * A)) . q_{1}[ Nat] means (Partial_Product (Prob * B)) . (($1 + n1) + 1) = ((Partial_Product (Prob * A)) . n1) * ((Partial_Product (Prob * (A ^\ ((n1 + n2) + 1)))) . (((($1 + n1) + 1) - n1) - 1));

A28: n1 in NAT by ORDINAL1:def 12;

( (Partial_Product (Prob * B)) . ((0 + n1) + 1) = ((Partial_Product (Prob * B)) . n1) * ((Prob * B) . (n1 + 1)) & n1 <= n1 ) by SERIES_3:def 1;

then A29: (Partial_Product (Prob * B)) . ((0 + n1) + 1) = ((Partial_Product (Prob * A)) . n1) * ((Prob * B) . (n1 + 1)) by A4, A28;

A30: dom (A * (Special_Function (n1,n2))) = NAT by FUNCT_2:def 1;

A31: n1 < n1 + 1 by NAT_1:13;

( (Special_Function (n1,n2)) . (n1 + 1) = IFGT ((n1 + 1),n1,((n1 + 1) + n2),(n1 + 1)) & IFGT ((n1 + 1),n1,((n1 + 1) + n2),(n1 + 1)) = (n1 + 1) + n2 ) by Def2, A31, XXREAL_0:def 11;

then A32: Prob . (B . (n1 + 1)) = Prob . (A . ((n1 + 1) + n2)) by A30, A3, FUNCT_1:12;

A33: A . (((n1 + n2) + 1) + 0) = (A ^\ ((n1 + n2) + 1)) . 0 by NAT_1:def 3;

dom (Prob * (A ^\ ((n1 + n2) + 1))) = NAT by FUNCT_2:def 1;

then A34: Prob . (B . (n1 + 1)) = (Prob * (A ^\ ((n1 + n2) + 1))) . 0 by A33, A32, FUNCT_1:12;

dom (Prob * B) = NAT by FUNCT_2:def 1;

then (Prob * B) . (n1 + 1) = (Prob * (A ^\ ((n1 + n2) + 1))) . 0 by A34, FUNCT_1:12;

then A35: S_{1}[ 0 ]
by A29, SERIES_3:def 1;

A36: for k being Nat st S_{1}[k] holds

S_{1}[k + 1]
_{1}[k]
from NAT_1:sch 2(A35, A36);

(n - n1) - 1 is Element of NAT

A44: k = (n - n1) - 1 ;

(Partial_Product (Prob * B)) . n = ((Partial_Product (Prob * A)) . n1) * ((Partial_Product (Prob * (A ^\ ((n1 + n2) + 1)))) . ((((((n - n1) - 1) + n1) + 1) - n1) - 1)) by A43, A44;

hence (Partial_Product (Prob * B)) . n = ((Partial_Product (Prob * A)) . n1) * ((Partial_Product (Prob * (A ^\ ((n1 + n2) + 1)))) . ((n - n1) - 1)) ; :: thesis: verum

end;assume that

A2: n > n1 and

A3: B = A * (Special_Function (n1,n2)) ; :: thesis: (Partial_Product (Prob * B)) . n = ((Partial_Product (Prob * A)) . n1) * ((Partial_Product (Prob * (A ^\ ((n1 + n2) + 1)))) . ((n - n1) - 1))

A4: for q being Element of NAT st q <= n1 holds

(Partial_Product (Prob * B)) . q = (Partial_Product (Prob * A)) . q

proof

defpred S
let q be Element of NAT ; :: thesis: ( q <= n1 implies (Partial_Product (Prob * B)) . q = (Partial_Product (Prob * A)) . q )

assume A5: q <= n1 ; :: thesis: (Partial_Product (Prob * B)) . q = (Partial_Product (Prob * A)) . q

defpred S_{1}[ Nat] means (Partial_Product (Prob * B)) . ($1 * ((Special_Function3 n1) . $1)) = (Partial_Product (Prob * A)) . ($1 * ((Special_Function3 n1) . $1));

A6: S_{1}[ 0 ]
_{1}[k] holds

S_{1}[k + 1]
_{1}[k]
from NAT_1:sch 2(A6, A12);

(Partial_Product (Prob * B)) . q = (Partial_Product (Prob * A)) . q

end;assume A5: q <= n1 ; :: thesis: (Partial_Product (Prob * B)) . q = (Partial_Product (Prob * A)) . q

defpred S

A6: S

proof

A12:
for k being Nat st S
A7:
(Partial_Product (Prob * B)) . 0 = (Prob * B) . 0
by SERIES_3:def 1;

A8: (Partial_Product (Prob * A)) . 0 = (Prob * A) . 0 by SERIES_3:def 1;

dom (Prob * B) = NAT by FUNCT_2:def 1;

then A9: (Prob * B) . 0 = Prob . (B . 0) by FUNCT_1:12;

A10: dom (A * (Special_Function (n1,n2))) = NAT by FUNCT_2:def 1;

( (Special_Function (n1,n2)) . 0 = IFGT (0,n1,(0 + n2),0) & IFGT (0,n1,(0 + n2),0) = 0 ) by Def2, XXREAL_0:def 11;

then A11: (Prob * B) . 0 = Prob . (A . 0) by A10, A3, A9, FUNCT_1:12;

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

hence S_{1}[ 0 ]
by A11, A7, A8, FUNCT_1:12; :: thesis: verum

end;A8: (Partial_Product (Prob * A)) . 0 = (Prob * A) . 0 by SERIES_3:def 1;

dom (Prob * B) = NAT by FUNCT_2:def 1;

then A9: (Prob * B) . 0 = Prob . (B . 0) by FUNCT_1:12;

A10: dom (A * (Special_Function (n1,n2))) = NAT by FUNCT_2:def 1;

( (Special_Function (n1,n2)) . 0 = IFGT (0,n1,(0 + n2),0) & IFGT (0,n1,(0 + n2),0) = 0 ) by Def2, XXREAL_0:def 11;

then A11: (Prob * B) . 0 = Prob . (A . 0) by A10, A3, A9, FUNCT_1:12;

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

hence S

S

proof

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

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

end;assume A13: S

per cases
( k < n1 or not k < n1 )
;

end;

suppose A14:
k < n1
; :: thesis: S_{1}[k + 1]

then A15:
( (Special_Function3 n1) . k = IFGT (k,n1,0,1) & IFGT (k,n1,0,1) = 1 )
by Def4, XXREAL_0:def 11;

k + 1 <= n1 by A14, NAT_1:13;

then A16: ( (Special_Function3 n1) . (k + 1) = IFGT ((k + 1),n1,0,1) & IFGT ((k + 1),n1,0,1) = 1 ) by Def4, XXREAL_0:def 11;

A17: (Prob * B) . (k + 1) = (Prob * A) . (k + 1)

hence S_{1}[k + 1]
by A16, SERIES_3:def 1; :: thesis: verum

end;k + 1 <= n1 by A14, NAT_1:13;

then A16: ( (Special_Function3 n1) . (k + 1) = IFGT ((k + 1),n1,0,1) & IFGT ((k + 1),n1,0,1) = 1 ) by Def4, XXREAL_0:def 11;

A17: (Prob * B) . (k + 1) = (Prob * A) . (k + 1)

proof

(Partial_Product (Prob * B)) . (k + 1) = ((Partial_Product (Prob * A)) . k) * ((Prob * A) . (k + 1))
by A15, A13, A17, SERIES_3:def 1;
dom (Prob * B) = NAT
by FUNCT_2:def 1;

then A18: (Prob * B) . (k + 1) = Prob . (B . (k + 1)) by FUNCT_1:12;

A19: dom (A * (Special_Function (n1,n2))) = NAT by FUNCT_2:def 1;

k + 1 <= n1 by A14, NAT_1:13;

then ( (Special_Function (n1,n2)) . (k + 1) = IFGT ((k + 1),n1,((k + 1) + n2),(k + 1)) & IFGT ((k + 1),n1,((k + 1) + n2),(k + 1)) = k + 1 ) by Def2, XXREAL_0:def 11;

then A20: (Prob * B) . (k + 1) = Prob . (A . (k + 1)) by A19, A3, A18, FUNCT_1:12;

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

hence (Prob * B) . (k + 1) = (Prob * A) . (k + 1) by A20, FUNCT_1:12; :: thesis: verum

end;then A18: (Prob * B) . (k + 1) = Prob . (B . (k + 1)) by FUNCT_1:12;

A19: dom (A * (Special_Function (n1,n2))) = NAT by FUNCT_2:def 1;

k + 1 <= n1 by A14, NAT_1:13;

then ( (Special_Function (n1,n2)) . (k + 1) = IFGT ((k + 1),n1,((k + 1) + n2),(k + 1)) & IFGT ((k + 1),n1,((k + 1) + n2),(k + 1)) = k + 1 ) by Def2, XXREAL_0:def 11;

then A20: (Prob * B) . (k + 1) = Prob . (A . (k + 1)) by A19, A3, A18, FUNCT_1:12;

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

hence (Prob * B) . (k + 1) = (Prob * A) . (k + 1) by A20, FUNCT_1:12; :: thesis: verum

hence S

suppose A21:
not k < n1
; :: thesis: S_{1}[k + 1]

n1 < k + 1
by A21, XREAL_1:145;

then A22: ( (Special_Function3 n1) . (k + 1) = IFGT ((k + 1),n1,0,1) & IFGT ((k + 1),n1,0,1) = 0 ) by Def4, XXREAL_0:def 11;

A23: (Prob * B) . 0 = (Prob * A) . 0

hence S_{1}[k + 1]
by A23; :: thesis: verum

end;then A22: ( (Special_Function3 n1) . (k + 1) = IFGT ((k + 1),n1,0,1) & IFGT ((k + 1),n1,0,1) = 0 ) by Def4, XXREAL_0:def 11;

A23: (Prob * B) . 0 = (Prob * A) . 0

proof

( (Partial_Product (Prob * B)) . ((k + 1) * ((Special_Function3 n1) . (k + 1))) = (Prob * B) . 0 & (Partial_Product (Prob * A)) . ((k + 1) * ((Special_Function3 n1) . (k + 1))) = (Prob * A) . 0 )
by A22, SERIES_3:def 1;
dom (Prob * B) = NAT
by FUNCT_2:def 1;

then A24: (Prob * B) . 0 = Prob . (B . 0) by FUNCT_1:12;

A25: dom (A * (Special_Function (n1,n2))) = NAT by FUNCT_2:def 1;

( (Special_Function (n1,n2)) . 0 = IFGT (0,n1,(0 + n2),0) & IFGT (0,n1,(0 + n2),0) = 0 ) by Def2, XXREAL_0:def 11;

then A26: (Prob * B) . 0 = Prob . (A . 0) by A25, A3, A24, FUNCT_1:12;

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

hence (Prob * B) . 0 = (Prob * A) . 0 by A26, FUNCT_1:12; :: thesis: verum

end;then A24: (Prob * B) . 0 = Prob . (B . 0) by FUNCT_1:12;

A25: dom (A * (Special_Function (n1,n2))) = NAT by FUNCT_2:def 1;

( (Special_Function (n1,n2)) . 0 = IFGT (0,n1,(0 + n2),0) & IFGT (0,n1,(0 + n2),0) = 0 ) by Def2, XXREAL_0:def 11;

then A26: (Prob * B) . 0 = Prob . (A . 0) by A25, A3, A24, FUNCT_1:12;

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

hence (Prob * B) . 0 = (Prob * A) . 0 by A26, FUNCT_1:12; :: thesis: verum

hence S

(Partial_Product (Prob * B)) . q = (Partial_Product (Prob * A)) . q

proof

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

then q * ((Special_Function3 n1) . q) = q ;

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

end;then q * ((Special_Function3 n1) . q) = q ;

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

A28: n1 in NAT by ORDINAL1:def 12;

( (Partial_Product (Prob * B)) . ((0 + n1) + 1) = ((Partial_Product (Prob * B)) . n1) * ((Prob * B) . (n1 + 1)) & n1 <= n1 ) by SERIES_3:def 1;

then A29: (Partial_Product (Prob * B)) . ((0 + n1) + 1) = ((Partial_Product (Prob * A)) . n1) * ((Prob * B) . (n1 + 1)) by A4, A28;

A30: dom (A * (Special_Function (n1,n2))) = NAT by FUNCT_2:def 1;

A31: n1 < n1 + 1 by NAT_1:13;

( (Special_Function (n1,n2)) . (n1 + 1) = IFGT ((n1 + 1),n1,((n1 + 1) + n2),(n1 + 1)) & IFGT ((n1 + 1),n1,((n1 + 1) + n2),(n1 + 1)) = (n1 + 1) + n2 ) by Def2, A31, XXREAL_0:def 11;

then A32: Prob . (B . (n1 + 1)) = Prob . (A . ((n1 + 1) + n2)) by A30, A3, FUNCT_1:12;

A33: A . (((n1 + n2) + 1) + 0) = (A ^\ ((n1 + n2) + 1)) . 0 by NAT_1:def 3;

dom (Prob * (A ^\ ((n1 + n2) + 1))) = NAT by FUNCT_2:def 1;

then A34: Prob . (B . (n1 + 1)) = (Prob * (A ^\ ((n1 + n2) + 1))) . 0 by A33, A32, FUNCT_1:12;

dom (Prob * B) = NAT by FUNCT_2:def 1;

then (Prob * B) . (n1 + 1) = (Prob * (A ^\ ((n1 + n2) + 1))) . 0 by A34, FUNCT_1:12;

then A35: S

A36: for k being Nat st S

S

proof

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

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

A38: (Partial_Product (Prob * B)) . (((k + 1) + n1) + 1) = (((Partial_Product (Prob * A)) . n1) * ((Partial_Product (Prob * (A ^\ ((n1 + n2) + 1)))) . k)) * ((Prob * B) . (((k + 1) + n1) + 1)) by A37, SERIES_3:def 1;

A39: (Prob * B) . (((k + 1) + n1) + 1) = (Prob * (A ^\ ((n1 + n2) + 1))) . (k + 1)

hence S_{1}[k + 1]
by A39, A38; :: thesis: verum

end;assume A37: S

A38: (Partial_Product (Prob * B)) . (((k + 1) + n1) + 1) = (((Partial_Product (Prob * A)) . n1) * ((Partial_Product (Prob * (A ^\ ((n1 + n2) + 1)))) . k)) * ((Prob * B) . (((k + 1) + n1) + 1)) by A37, SERIES_3:def 1;

A39: (Prob * B) . (((k + 1) + n1) + 1) = (Prob * (A ^\ ((n1 + n2) + 1))) . (k + 1)

proof

((Partial_Product (Prob * (A ^\ ((n1 + n2) + 1)))) . k) * ((Prob * (A ^\ ((n1 + n2) + 1))) . (k + 1)) = (Partial_Product (Prob * (A ^\ ((n1 + n2) + 1)))) . (k + 1)
by SERIES_3:def 1;
set j = ((k + 1) + n1) + 1;

A40: dom (A * (Special_Function (n1,n2))) = NAT by FUNCT_2:def 1;

1 <= (k + 1) + 1 by XREAL_1:31;

then n1 < n1 + ((k + 1) + 1) by NAT_1:19;

then ( (Special_Function (n1,n2)) . (((k + 1) + n1) + 1) = IFGT ((((k + 1) + n1) + 1),n1,((((k + 1) + n1) + 1) + n2),(((k + 1) + n1) + 1)) & IFGT ((((k + 1) + n1) + 1),n1,((((k + 1) + n1) + 1) + n2),(((k + 1) + n1) + 1)) = (((k + 1) + n1) + 1) + n2 ) by Def2, XXREAL_0:def 11;

then B . (((k + 1) + n1) + 1) = A . (((n1 + n2) + 1) + (k + 1)) by A40, A3, FUNCT_1:12;

then A41: Prob . (B . (((k + 1) + n1) + 1)) = Prob . ((A ^\ ((n1 + n2) + 1)) . (k + 1)) by NAT_1:def 3;

dom (Prob * B) = NAT by FUNCT_2:def 1;

then A42: (Prob * B) . (((k + 1) + n1) + 1) = Prob . ((A ^\ ((n1 + n2) + 1)) . (k + 1)) by A41, FUNCT_1:12;

dom (Prob * (A ^\ ((n1 + n2) + 1))) = NAT by FUNCT_2:def 1;

hence (Prob * B) . (((k + 1) + n1) + 1) = (Prob * (A ^\ ((n1 + n2) + 1))) . (k + 1) by A42, FUNCT_1:12; :: thesis: verum

end;A40: dom (A * (Special_Function (n1,n2))) = NAT by FUNCT_2:def 1;

1 <= (k + 1) + 1 by XREAL_1:31;

then n1 < n1 + ((k + 1) + 1) by NAT_1:19;

then ( (Special_Function (n1,n2)) . (((k + 1) + n1) + 1) = IFGT ((((k + 1) + n1) + 1),n1,((((k + 1) + n1) + 1) + n2),(((k + 1) + n1) + 1)) & IFGT ((((k + 1) + n1) + 1),n1,((((k + 1) + n1) + 1) + n2),(((k + 1) + n1) + 1)) = (((k + 1) + n1) + 1) + n2 ) by Def2, XXREAL_0:def 11;

then B . (((k + 1) + n1) + 1) = A . (((n1 + n2) + 1) + (k + 1)) by A40, A3, FUNCT_1:12;

then A41: Prob . (B . (((k + 1) + n1) + 1)) = Prob . ((A ^\ ((n1 + n2) + 1)) . (k + 1)) by NAT_1:def 3;

dom (Prob * B) = NAT by FUNCT_2:def 1;

then A42: (Prob * B) . (((k + 1) + n1) + 1) = Prob . ((A ^\ ((n1 + n2) + 1)) . (k + 1)) by A41, FUNCT_1:12;

dom (Prob * (A ^\ ((n1 + n2) + 1))) = NAT by FUNCT_2:def 1;

hence (Prob * B) . (((k + 1) + n1) + 1) = (Prob * (A ^\ ((n1 + n2) + 1))) . (k + 1) by A42, FUNCT_1:12; :: thesis: verum

hence S

(n - n1) - 1 is Element of NAT

proof

then consider k being Element of NAT such that
n1 + 1 <= n
by A2, NAT_1:13;

then (n1 + 1) - 1 <= n - 1 by XREAL_1:9;

then ( n1 <= n - 1 & n - 1 is Element of NAT ) by A2, NAT_1:20;

then (n - 1) - n1 is Element of NAT by NAT_1:21;

hence (n - n1) - 1 is Element of NAT ; :: thesis: verum

end;then (n1 + 1) - 1 <= n - 1 by XREAL_1:9;

then ( n1 <= n - 1 & n - 1 is Element of NAT ) by A2, NAT_1:20;

then (n - 1) - n1 is Element of NAT by NAT_1:21;

hence (n - n1) - 1 is Element of NAT ; :: thesis: verum

A44: k = (n - n1) - 1 ;

(Partial_Product (Prob * B)) . n = ((Partial_Product (Prob * A)) . n1) * ((Partial_Product (Prob * (A ^\ ((n1 + n2) + 1)))) . ((((((n - n1) - 1) + n1) + 1) - n1) - 1)) by A43, A44;

hence (Partial_Product (Prob * B)) . n = ((Partial_Product (Prob * A)) . n1) * ((Partial_Product (Prob * (A ^\ ((n1 + n2) + 1)))) . ((n - n1) - 1)) ; :: thesis: verum

for n1, n2, n being Nat

for e being sequence of NAT st n > n1 & C = A * e & B = C * (Special_Function (n1,n2)) holds

(Partial_Intersection B) . n = ((Partial_Intersection C) . n1) /\ ((Partial_Intersection (C ^\ ((n1 + n2) + 1))) . ((n - n1) - 1))

proof

hence
( ( for A, B being SetSequence of Sigma st n > n1 & B = A * (Special_Function (n1,n2)) holds
let A, B, C be SetSequence of Sigma; :: thesis: for n1, n2, n being Nat

for e being sequence of NAT st n > n1 & C = A * e & B = C * (Special_Function (n1,n2)) holds

(Partial_Intersection B) . n = ((Partial_Intersection C) . n1) /\ ((Partial_Intersection (C ^\ ((n1 + n2) + 1))) . ((n - n1) - 1))

let n1, n2, n be Nat; :: thesis: for e being sequence of NAT st n > n1 & C = A * e & B = C * (Special_Function (n1,n2)) holds

(Partial_Intersection B) . n = ((Partial_Intersection C) . n1) /\ ((Partial_Intersection (C ^\ ((n1 + n2) + 1))) . ((n - n1) - 1))

let e be sequence of NAT; :: thesis: ( n > n1 & C = A * e & B = C * (Special_Function (n1,n2)) implies (Partial_Intersection B) . n = ((Partial_Intersection C) . n1) /\ ((Partial_Intersection (C ^\ ((n1 + n2) + 1))) . ((n - n1) - 1)) )

assume A45: n > n1 ; :: thesis: ( not C = A * e or not B = C * (Special_Function (n1,n2)) or (Partial_Intersection B) . n = ((Partial_Intersection C) . n1) /\ ((Partial_Intersection (C ^\ ((n1 + n2) + 1))) . ((n - n1) - 1)) )

assume C = A * e ; :: thesis: ( not B = C * (Special_Function (n1,n2)) or (Partial_Intersection B) . n = ((Partial_Intersection C) . n1) /\ ((Partial_Intersection (C ^\ ((n1 + n2) + 1))) . ((n - n1) - 1)) )

assume A46: B = C * (Special_Function (n1,n2)) ; :: thesis: (Partial_Intersection B) . n = ((Partial_Intersection C) . n1) /\ ((Partial_Intersection (C ^\ ((n1 + n2) + 1))) . ((n - n1) - 1))

reconsider B = B as SetSequence of Sigma ;

A47: (Partial_Intersection B) . n1 = (Partial_Intersection C) . n1

x in B . knat ) holds

( ( for knat being Nat st knat <= n1 holds

x in B . knat ) & ( for knat being Nat st n1 < knat & knat <= n holds

x in B . knat ) ) by A45, XXREAL_0:2;

A58: for x being object st x in (Partial_Intersection (C ^\ ((n1 + n2) + 1))) . ((n - n1) - 1) holds

for qnat being Nat st n1 < qnat & qnat <= n holds

x in B . qnat

x in B . qnat ) holds

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

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

x in B . knat ) & ( for knat being Nat st n1 < knat & knat <= n holds

x in B . knat ) ) )

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

x in B . knat ) ) )

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

end;for e being sequence of NAT st n > n1 & C = A * e & B = C * (Special_Function (n1,n2)) holds

(Partial_Intersection B) . n = ((Partial_Intersection C) . n1) /\ ((Partial_Intersection (C ^\ ((n1 + n2) + 1))) . ((n - n1) - 1))

let n1, n2, n be Nat; :: thesis: for e being sequence of NAT st n > n1 & C = A * e & B = C * (Special_Function (n1,n2)) holds

(Partial_Intersection B) . n = ((Partial_Intersection C) . n1) /\ ((Partial_Intersection (C ^\ ((n1 + n2) + 1))) . ((n - n1) - 1))

let e be sequence of NAT; :: thesis: ( n > n1 & C = A * e & B = C * (Special_Function (n1,n2)) implies (Partial_Intersection B) . n = ((Partial_Intersection C) . n1) /\ ((Partial_Intersection (C ^\ ((n1 + n2) + 1))) . ((n - n1) - 1)) )

assume A45: n > n1 ; :: thesis: ( not C = A * e or not B = C * (Special_Function (n1,n2)) or (Partial_Intersection B) . n = ((Partial_Intersection C) . n1) /\ ((Partial_Intersection (C ^\ ((n1 + n2) + 1))) . ((n - n1) - 1)) )

assume C = A * e ; :: thesis: ( not B = C * (Special_Function (n1,n2)) or (Partial_Intersection B) . n = ((Partial_Intersection C) . n1) /\ ((Partial_Intersection (C ^\ ((n1 + n2) + 1))) . ((n - n1) - 1)) )

assume A46: B = C * (Special_Function (n1,n2)) ; :: thesis: (Partial_Intersection B) . n = ((Partial_Intersection C) . n1) /\ ((Partial_Intersection (C ^\ ((n1 + n2) + 1))) . ((n - n1) - 1))

reconsider B = B as SetSequence of Sigma ;

A47: (Partial_Intersection B) . n1 = (Partial_Intersection C) . n1

proof

A57:
for x being set st ( for knat being Nat st knat <= n holds
for x being object holds

( x in (Partial_Intersection B) . n1 iff x in (Partial_Intersection C) . n1 )

end;( x in (Partial_Intersection B) . n1 iff x in (Partial_Intersection C) . n1 )

proof

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

x in (Partial_Intersection B) . n1

end;hereby :: thesis: ( x in (Partial_Intersection C) . n1 implies x in (Partial_Intersection B) . n1 )

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

x in (Partial_Intersection C) . n1

end;x in (Partial_Intersection C) . n1

proof

hence
x in (Partial_Intersection C) . n1
; :: thesis: verum
A49:
for knat being Nat st knat <= n1 holds

x in C . knat

thus x in (Partial_Intersection C) . n1 by A49, PROB_3:25; :: thesis: verum

end;x in C . knat

proof

reconsider n1 = n1 as Nat ;
let knat be Nat; :: thesis: ( knat <= n1 implies x in C . knat )

assume A50: knat <= n1 ; :: thesis: x in C . knat

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

A51: x in B . knat by A50, A48, PROB_3:25;

A52: dom (C * (Special_Function (n1,n2))) = NAT by FUNCT_2:def 1;

( (Special_Function (n1,n2)) . knat = IFGT (knat,n1,(knat + n2),knat) & IFGT (knat,n1,(knat + n2),knat) = knat ) by Def2, A50, XXREAL_0:def 11;

hence x in C . knat by A52, A46, A51, FUNCT_1:12; :: thesis: verum

end;assume A50: knat <= n1 ; :: thesis: x in C . knat

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

A51: x in B . knat by A50, A48, PROB_3:25;

A52: dom (C * (Special_Function (n1,n2))) = NAT by FUNCT_2:def 1;

( (Special_Function (n1,n2)) . knat = IFGT (knat,n1,(knat + n2),knat) & IFGT (knat,n1,(knat + n2),knat) = knat ) by Def2, A50, XXREAL_0:def 11;

hence x in C . knat by A52, A46, A51, FUNCT_1:12; :: thesis: verum

thus x in (Partial_Intersection C) . n1 by A49, PROB_3:25; :: thesis: verum

x in (Partial_Intersection B) . n1

proof

hence
x in (Partial_Intersection B) . n1
; :: thesis: verum
for knat being Nat st knat <= n1 holds

x in B . knat

end;x in B . knat

proof

hence
x in (Partial_Intersection B) . n1
by PROB_3:25; :: thesis: verum
let knat be Nat; :: thesis: ( knat <= n1 implies x in B . knat )

assume A54: knat <= n1 ; :: thesis: x in B . knat

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

A55: x in C . knat by A54, A53, PROB_3:25;

A56: dom (C * (Special_Function (n1,n2))) = NAT by FUNCT_2:def 1;

( (Special_Function (n1,n2)) . knat = IFGT (knat,n1,(knat + n2),knat) & IFGT (knat,n1,(knat + n2),knat) = knat ) by Def2, A54, XXREAL_0:def 11;

hence x in B . knat by A56, A46, A55, FUNCT_1:12; :: thesis: verum

end;assume A54: knat <= n1 ; :: thesis: x in B . knat

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

A55: x in C . knat by A54, A53, PROB_3:25;

A56: dom (C * (Special_Function (n1,n2))) = NAT by FUNCT_2:def 1;

( (Special_Function (n1,n2)) . knat = IFGT (knat,n1,(knat + n2),knat) & IFGT (knat,n1,(knat + n2),knat) = knat ) by Def2, A54, XXREAL_0:def 11;

hence x in B . knat by A56, A46, A55, FUNCT_1:12; :: thesis: verum

x in B . knat ) holds

( ( for knat being Nat st knat <= n1 holds

x in B . knat ) & ( for knat being Nat st n1 < knat & knat <= n holds

x in B . knat ) ) by A45, XXREAL_0:2;

A58: for x being object st x in (Partial_Intersection (C ^\ ((n1 + n2) + 1))) . ((n - n1) - 1) holds

for qnat being Nat st n1 < qnat & qnat <= n holds

x in B . qnat

proof

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

x in B . qnat )

assume A59: x in (Partial_Intersection (C ^\ ((n1 + n2) + 1))) . ((n - n1) - 1) ; :: thesis: for qnat being Nat st n1 < qnat & qnat <= n holds

x in B . qnat

A60: ( (n - n1) - 1 >= 0 & (n - n1) - 1 is Element of NAT )

x in C . (knat + ((n1 + n2) + 1))

x in B . qnat

x in B . qnat ; :: thesis: verum

end;x in B . qnat )

assume A59: x in (Partial_Intersection (C ^\ ((n1 + n2) + 1))) . ((n - n1) - 1) ; :: thesis: for qnat being Nat st n1 < qnat & qnat <= n holds

x in B . qnat

A60: ( (n - n1) - 1 >= 0 & (n - n1) - 1 is Element of NAT )

proof

A61:
for knat being Nat st knat <= (n - n1) - 1 holds
n - n1 is Element of NAT
by A45, NAT_1:21;

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

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

x in C . (knat + ((n1 + n2) + 1))

proof

for qnat being Nat st n1 < qnat & qnat <= n holds
let knat be Nat; :: thesis: ( knat <= (n - n1) - 1 implies x in C . (knat + ((n1 + n2) + 1)) )

assume knat <= (n - n1) - 1 ; :: thesis: x in C . (knat + ((n1 + n2) + 1))

then x in (C ^\ ((n1 + n2) + 1)) . knat by A60, A59, PROB_3:25;

hence x in C . (knat + ((n1 + n2) + 1)) by NAT_1:def 3; :: thesis: verum

end;assume knat <= (n - n1) - 1 ; :: thesis: x in C . (knat + ((n1 + n2) + 1))

then x in (C ^\ ((n1 + n2) + 1)) . knat by A60, A59, PROB_3:25;

hence x in C . (knat + ((n1 + n2) + 1)) by NAT_1:def 3; :: thesis: verum

x in B . qnat

proof

hence
for qnat being Nat st n1 < qnat & qnat <= n holds
let qnat be Nat; :: thesis: ( n1 < qnat & qnat <= n implies x in B . qnat )

assume that

A62: n1 < qnat and

A63: qnat <= n ; :: thesis: x in B . qnat

A64: ( n1 + 1 <= qnat & qnat <= n ) by A62, A63, NAT_1:13;

A65: qnat - (n1 + 1) is Element of NAT by A64, NAT_1:21;

consider knat being Nat such that

A66: knat = (qnat - n1) - 1 by A65;

A67: (qnat - n1) - 1 <= (n - n1) - 1

x in B . qnat

end;assume that

A62: n1 < qnat and

A63: qnat <= n ; :: thesis: x in B . qnat

A64: ( n1 + 1 <= qnat & qnat <= n ) by A62, A63, NAT_1:13;

A65: qnat - (n1 + 1) is Element of NAT by A64, NAT_1:21;

consider knat being Nat such that

A66: knat = (qnat - n1) - 1 by A65;

A67: (qnat - n1) - 1 <= (n - n1) - 1

proof

A68:
x in C . (knat + ((n1 + n2) + 1))
by A66, A67, A61;
qnat - (n1 + 1) <= n - (n1 + 1)
by A63, XREAL_1:9;

hence (qnat - n1) - 1 <= (n - n1) - 1 ; :: thesis: verum

end;hence (qnat - n1) - 1 <= (n - n1) - 1 ; :: thesis: verum

x in B . qnat

proof

hence
x in B . qnat
; :: thesis: verum
reconsider qnat = qnat as Element of NAT by ORDINAL1:def 12;

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

( (Special_Function (n1,n2)) . qnat = IFGT (qnat,n1,(qnat + n2),qnat) & IFGT (qnat,n1,(qnat + n2),qnat) = qnat + n2 ) by Def2, A62, XXREAL_0:def 11;

hence x in B . qnat by A69, A46, A66, A68, FUNCT_1:12; :: thesis: verum

end;A69: dom (C * (Special_Function (n1,n2))) = NAT by FUNCT_2:def 1;

( (Special_Function (n1,n2)) . qnat = IFGT (qnat,n1,(qnat + n2),qnat) & IFGT (qnat,n1,(qnat + n2),qnat) = qnat + n2 ) by Def2, A62, XXREAL_0:def 11;

hence x in B . qnat by A69, A46, A66, A68, FUNCT_1:12; :: thesis: verum

x in B . qnat ; :: thesis: verum

x in B . qnat ) holds

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

proof

A82:
for x being set holds
let x be object ; :: thesis: ( ( for qnat being Nat st n1 < qnat & qnat <= n holds

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

assume A71: for qnat being Nat st n1 < qnat & qnat <= n holds

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

A72: ( (n - n1) - 1 >= 0 & (n - n1) - 1 is Element of NAT )

end;x in B . qnat ) implies x in (Partial_Intersection (C ^\ ((n1 + n2) + 1))) . ((n - n1) - 1) )

assume A71: for qnat being Nat st n1 < qnat & qnat <= n holds

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

A72: ( (n - n1) - 1 >= 0 & (n - n1) - 1 is Element of NAT )

proof

x in (Partial_Intersection (C ^\ ((n1 + n2) + 1))) . ((n - n1) - 1)
n - n1 is Element of NAT
by A45, NAT_1:21;

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

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

proof

hence
x in (Partial_Intersection (C ^\ ((n1 + n2) + 1))) . ((n - n1) - 1)
; :: thesis: verum
A73:
for qnat being Nat st 0 <= (qnat - n1) - 1 & (qnat - n1) - 1 <= (n - n1) - 1 holds

x in B . qnat

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

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

hence x in (Partial_Intersection (C ^\ ((n1 + n2) + 1))) . ((n - n1) - 1) by A72, PROB_3:25; :: thesis: verum

end;x in B . qnat

proof

for knat being Nat st 0 <= knat & knat <= (n - n1) - 1 holds
let qnat be Nat; :: thesis: ( 0 <= (qnat - n1) - 1 & (qnat - n1) - 1 <= (n - n1) - 1 implies x in B . qnat )

assume that

A74: 0 <= (qnat - n1) - 1 and

A75: (qnat - n1) - 1 <= (n - n1) - 1 ; :: thesis: x in B . qnat

0 + (n1 + 1) <= (qnat - (n1 + 1)) + (n1 + 1) by A74, XREAL_1:6;

then (n1 + 1) - 1 <= qnat - 1 by XREAL_1:9;

then ( n1 <= qnat - 1 & qnat < qnat + 1 ) by NAT_1:13;

then ( n1 <= qnat - 1 & qnat - 1 < (qnat + 1) - 1 ) by XREAL_1:9;

then A76: n1 < qnat by XXREAL_0:2;

(qnat - (n1 + 1)) + (n1 + 1) <= (n - (n1 + 1)) + (n1 + 1) by A75, XREAL_1:6;

hence x in B . qnat by A76, A71; :: thesis: verum

end;assume that

A74: 0 <= (qnat - n1) - 1 and

A75: (qnat - n1) - 1 <= (n - n1) - 1 ; :: thesis: x in B . qnat

0 + (n1 + 1) <= (qnat - (n1 + 1)) + (n1 + 1) by A74, XREAL_1:6;

then (n1 + 1) - 1 <= qnat - 1 by XREAL_1:9;

then ( n1 <= qnat - 1 & qnat < qnat + 1 ) by NAT_1:13;

then ( n1 <= qnat - 1 & qnat - 1 < (qnat + 1) - 1 ) by XREAL_1:9;

then A76: n1 < qnat by XXREAL_0:2;

(qnat - (n1 + 1)) + (n1 + 1) <= (n - (n1 + 1)) + (n1 + 1) by A75, XREAL_1:6;

hence x in B . qnat by A76, A71; :: thesis: verum

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

proof

then
for knat being Nat st knat <= (n - n1) - 1 holds
let knat be Nat; :: thesis: ( 0 <= knat & knat <= (n - n1) - 1 implies x in (C ^\ ((n1 + n2) + 1)) . knat )

assume that

0 <= knat and

A77: knat <= (n - n1) - 1 ; :: thesis: x in (C ^\ ((n1 + n2) + 1)) . knat

set qnat = (knat + n1) + 1;

A78: (((knat + n1) + 1) - n1) - 1 <= (n - n1) - 1 by A77;

A79: x in B . ((knat + n1) + 1) by A78, A73;

A80: dom (C * (Special_Function (n1,n2))) = NAT by FUNCT_2:def 1;

A81: n1 < (knat + n1) + 1 by NAT_1:13, XREAL_1:31;

( (Special_Function (n1,n2)) . ((knat + n1) + 1) = IFGT (((knat + n1) + 1),n1,(((knat + n1) + 1) + n2),((knat + n1) + 1)) & IFGT (((knat + n1) + 1),n1,(((knat + n1) + 1) + n2),((knat + n1) + 1)) = ((knat + n1) + 1) + n2 ) by Def2, A81, XXREAL_0:def 11;

then B . ((knat + n1) + 1) = C . (((n1 + n2) + 1) + knat) by A46, A80, FUNCT_1:12;

hence x in (C ^\ ((n1 + n2) + 1)) . knat by A79, NAT_1:def 3; :: thesis: verum

end;assume that

0 <= knat and

A77: knat <= (n - n1) - 1 ; :: thesis: x in (C ^\ ((n1 + n2) + 1)) . knat

set qnat = (knat + n1) + 1;

A78: (((knat + n1) + 1) - n1) - 1 <= (n - n1) - 1 by A77;

A79: x in B . ((knat + n1) + 1) by A78, A73;

A80: dom (C * (Special_Function (n1,n2))) = NAT by FUNCT_2:def 1;

A81: n1 < (knat + n1) + 1 by NAT_1:13, XREAL_1:31;

( (Special_Function (n1,n2)) . ((knat + n1) + 1) = IFGT (((knat + n1) + 1),n1,(((knat + n1) + 1) + n2),((knat + n1) + 1)) & IFGT (((knat + n1) + 1),n1,(((knat + n1) + 1) + n2),((knat + n1) + 1)) = ((knat + n1) + 1) + n2 ) by Def2, A81, XXREAL_0:def 11;

then B . ((knat + n1) + 1) = C . (((n1 + n2) + 1) + knat) by A46, A80, FUNCT_1:12;

hence x in (C ^\ ((n1 + n2) + 1)) . knat by A79, NAT_1:def 3; :: thesis: verum

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

hence x in (Partial_Intersection (C ^\ ((n1 + n2) + 1))) . ((n - n1) - 1) by A72, PROB_3:25; :: thesis: verum

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

x in B . knat ) & ( for knat being Nat st n1 < knat & knat <= n holds

x in B . knat ) ) )

proof

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

x in B . knat ) & ( for knat being Nat st n1 < knat & knat <= n holds

x in B . knat ) ) )

( x in (Partial_Intersection B) . n iff for knat being Nat st knat <= n holds

x in B . knat ) by PROB_3:25;

hence ( x in (Partial_Intersection B) . n iff ( ( for knat being Nat st knat <= n1 holds

x in B . knat ) & ( for knat being Nat st n1 < knat & knat <= n holds

x in B . knat ) ) ) by A57; :: thesis: verum

end;x in B . knat ) & ( for knat being Nat st n1 < knat & knat <= n holds

x in B . knat ) ) )

( x in (Partial_Intersection B) . n iff for knat being Nat st knat <= n holds

x in B . knat ) by PROB_3:25;

hence ( x in (Partial_Intersection B) . n iff ( ( for knat being Nat st knat <= n1 holds

x in B . knat ) & ( for knat being Nat st n1 < knat & knat <= n holds

x in B . knat ) ) ) by A57; :: thesis: verum

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

x in B . knat ) ) )

proof

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

x in B . knat ) ) )

( x in (Partial_Intersection B) . n1 iff for knat being Nat st knat <= n1 holds

x in B . knat ) by PROB_3:25;

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

x in B . knat ) ) ) by A82; :: thesis: verum

end;x in B . knat ) ) )

( x in (Partial_Intersection B) . n1 iff for knat being Nat st knat <= n1 holds

x in B . knat ) by PROB_3:25;

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

x in B . knat ) ) ) by A82; :: thesis: verum

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

proof

hence
(Partial_Intersection B) . n = ((Partial_Intersection C) . n1) /\ ((Partial_Intersection (C ^\ ((n1 + n2) + 1))) . ((n - n1) - 1))
by A47, XBOOLE_0:def 4; :: thesis: verum
let x be object ; :: thesis: ( x in (Partial_Intersection B) . n iff ( x in (Partial_Intersection B) . n1 & x in (Partial_Intersection (C ^\ ((n1 + n2) + 1))) . ((n - n1) - 1) ) )

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

x in B . knat ) by A58, A70;

hence ( x in (Partial_Intersection B) . n iff ( x in (Partial_Intersection B) . n1 & x in (Partial_Intersection (C ^\ ((n1 + n2) + 1))) . ((n - n1) - 1) ) ) by A83; :: thesis: verum

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

x in B . knat ) by A58, A70;

hence ( x in (Partial_Intersection B) . n iff ( x in (Partial_Intersection B) . n1 & x in (Partial_Intersection (C ^\ ((n1 + n2) + 1))) . ((n - n1) - 1) ) ) by A83; :: thesis: verum

(Partial_Product (Prob * B)) . n = ((Partial_Product (Prob * A)) . n1) * ((Partial_Product (Prob * (A ^\ ((n1 + n2) + 1)))) . ((n - n1) - 1)) ) & ( for A, B, C being SetSequence of Sigma

for e being sequence of NAT st n > n1 & C = A * e & B = C * (Special_Function (n1,n2)) holds

(Partial_Intersection B) . n = ((Partial_Intersection C) . n1) /\ ((Partial_Intersection (C ^\ ((n1 + n2) + 1))) . ((n - n1) - 1)) ) ) by A1; :: thesis: verum