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 Fy being FinSequence of S2
for p being set st dom F = dom Fy & ( for n being Nat st n in dom Fy holds
Fy . n = Measurable-X-section ((F . n),p) ) holds
Measurable-X-section ((Union F),p) = Union Fy
let S1 be SigmaField of X1; :: thesis: for S2 being SigmaField of X2
for F being FinSequence of sigma (measurable_rectangles (S1,S2))
for Fy being FinSequence of S2
for p being set st dom F = dom Fy & ( for n being Nat st n in dom Fy holds
Fy . n = Measurable-X-section ((F . n),p) ) holds
Measurable-X-section ((Union F),p) = Union Fy
let S2 be SigmaField of X2; :: thesis: for F being FinSequence of sigma (measurable_rectangles (S1,S2))
for Fy being FinSequence of S2
for p being set st dom F = dom Fy & ( for n being Nat st n in dom Fy holds
Fy . n = Measurable-X-section ((F . n),p) ) holds
Measurable-X-section ((Union F),p) = Union Fy
let F be FinSequence of sigma (measurable_rectangles (S1,S2)); :: thesis: for Fy being FinSequence of S2
for p being set st dom F = dom Fy & ( for n being Nat st n in dom Fy holds
Fy . n = Measurable-X-section ((F . n),p) ) holds
Measurable-X-section ((Union F),p) = Union Fy
let Fy be FinSequence of S2; :: thesis: for p being set st dom F = dom Fy & ( for n being Nat st n in dom Fy holds
Fy . n = Measurable-X-section ((F . n),p) ) holds
Measurable-X-section ((Union F),p) = Union Fy
let p be set ; :: thesis: ( dom F = dom Fy & ( for n being Nat st n in dom Fy holds
Fy . n = Measurable-X-section ((F . n),p) ) implies Measurable-X-section ((Union F),p) = Union Fy )
assume that
A1: dom F = dom Fy and
A2: for n being Nat st n in dom Fy holds
Fy . n = Measurable-X-section ((F . n),p) ; :: thesis: Measurable-X-section ((Union F),p) = Union Fy
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 F1y = Fy as FinSequence of bool X2 by FINSEQ_2:24;
for n being Nat st n in dom F1y holds
F1y . n = X-section ((F1 . n),p)

proof

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

end;

then X-section ((union (rng F1)),p) = union (rng F1y) by A1, Th22;
hence Measurable-X-section ((Union F),p) = Union Fy by A3, CARD_3:def 4; :: thesis: verum