let X1, X2 be non empty set ; for S1 being SigmaField of X1
for S2 being SigmaField of X2
for F being FinSequence of sigma (measurable_rectangles (S1,S2))
for Fx being FinSequence of S1
for p being set st dom F = dom Fx & ( for n being Nat st n in dom Fx holds
Fx . n = Measurable-Y-section ((F . n),p) ) holds
Measurable-Y-section ((Union F),p) = Union Fx
let S1 be SigmaField of X1; for S2 being SigmaField of X2
for F being FinSequence of sigma (measurable_rectangles (S1,S2))
for Fx being FinSequence of S1
for p being set st dom F = dom Fx & ( for n being Nat st n in dom Fx holds
Fx . n = Measurable-Y-section ((F . n),p) ) holds
Measurable-Y-section ((Union F),p) = Union Fx
let S2 be SigmaField of X2; for F being FinSequence of sigma (measurable_rectangles (S1,S2))
for Fx being FinSequence of S1
for p being set st dom F = dom Fx & ( for n being Nat st n in dom Fx holds
Fx . n = Measurable-Y-section ((F . n),p) ) holds
Measurable-Y-section ((Union F),p) = Union Fx
let F be FinSequence of sigma (measurable_rectangles (S1,S2)); for Fx being FinSequence of S1
for p being set st dom F = dom Fx & ( for n being Nat st n in dom Fx holds
Fx . n = Measurable-Y-section ((F . n),p) ) holds
Measurable-Y-section ((Union F),p) = Union Fx
let Fx be FinSequence of S1; for p being set st dom F = dom Fx & ( for n being Nat st n in dom Fx holds
Fx . n = Measurable-Y-section ((F . n),p) ) holds
Measurable-Y-section ((Union F),p) = Union Fx
let p be set ; ( dom F = dom Fx & ( for n being Nat st n in dom Fx holds
Fx . n = Measurable-Y-section ((F . n),p) ) implies Measurable-Y-section ((Union F),p) = Union Fx )
assume that
A1:
dom F = dom Fx
and
A2:
for n being Nat st n in dom Fx holds
Fx . n = Measurable-Y-section ((F . n),p)
; Measurable-Y-section ((Union F),p) = Union Fx
A3:
union (rng F) = Union F
by CARD_3:def 4;
reconsider F1 = F as FinSequence of bool [:X1,X2:] by FINSEQ_2:24;
reconsider F1x = Fx as FinSequence of bool X1 by FINSEQ_2:24;
for n being Nat st n in dom F1x holds
F1x . n = Y-section ((F1 . n),p)
then
Y-section ((union (rng F1)),p) = union (rng F1x)
by A1, Th23;
hence
Measurable-Y-section ((Union F),p) = Union Fx
by A3, CARD_3:def 4; verum