let X1, X2 be non empty set ; :: thesis: 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; :: thesis: 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; :: thesis: 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)); :: thesis: 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; :: thesis: 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 ; :: thesis: ( 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) ; :: thesis: 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)

proof

let n be Nat; :: thesis: ( n in dom F1x implies F1x . n = Y-section ((F1 . n),p) )
assume n in dom F1x ; :: thesis: F1x . n = Y-section ((F1 . n),p)
then Fx . n = Measurable-Y-section ((F . n),p) by A2;
hence F1x . n = Y-section ((F1 . n),p) ; :: thesis: verum

end;

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