let X be non empty set ; for Y, p being set
for F being SetSequence of [:X,Y:]
for Fx being SetSequence of X st ( for n being Nat holds Fx . n = Y-section ((F . n),p) ) holds
Y-section ((union (rng F)),p) = union (rng Fx)
let Y, p be set ; for F being SetSequence of [:X,Y:]
for Fx being SetSequence of X st ( for n being Nat holds Fx . n = Y-section ((F . n),p) ) holds
Y-section ((union (rng F)),p) = union (rng Fx)
let F be SetSequence of [:X,Y:]; for Fx being SetSequence of X st ( for n being Nat holds Fx . n = Y-section ((F . n),p) ) holds
Y-section ((union (rng F)),p) = union (rng Fx)
let Fx be SetSequence of X; ( ( for n being Nat holds Fx . n = Y-section ((F . n),p) ) implies Y-section ((union (rng F)),p) = union (rng Fx) )
assume A2:
for n being Nat holds Fx . n = Y-section ((F . n),p)
; Y-section ((union (rng F)),p) = union (rng Fx)
now for q being set st q in Y-section ((union (rng F)),p) holds
q in union (rng Fx)let q be
set ;
( q in Y-section ((union (rng F)),p) implies q in union (rng Fx) )assume
q in Y-section (
(union (rng F)),
p)
;
q in union (rng Fx)then consider x1 being
Element of
X such that A3:
(
q = x1 &
[x1,p] in union (rng F) )
;
consider T being
set such that A4:
(
[x1,p] in T &
T in rng F )
by A3, TARSKI:def 4;
consider m being
Element of
NAT such that A5:
T = F . m
by A4, FUNCT_2:113;
Fx . m = Y-section (
(F . m),
p)
by A2;
then
(
q in Fx . m &
Fx . m in rng Fx )
by A3, A4, A5, FUNCT_2:112;
hence
q in union (rng Fx)
by TARSKI:def 4;
verum end;
then A7:
Y-section ((union (rng F)),p) c= union (rng Fx)
;
now for q being set st q in union (rng Fx) holds
q in Y-section ((union (rng F)),p)let q be
set ;
( q in union (rng Fx) implies q in Y-section ((union (rng F)),p) )assume
q in union (rng Fx)
;
q in Y-section ((union (rng F)),p)then consider T being
set such that A8:
(
q in T &
T in rng Fx )
by TARSKI:def 4;
consider m being
Element of
NAT such that A9:
T = Fx . m
by A8, FUNCT_2:113;
q in Y-section (
(F . m),
p)
by A2, A8, A9;
then consider x1 being
Element of
X such that A10:
(
q = x1 &
[x1,p] in F . m )
;
F . m in rng F
by FUNCT_2:112;
then
[x1,p] in union (rng F)
by A10, TARSKI:def 4;
hence
q in Y-section (
(union (rng F)),
p)
by A10;
verum end;
then
union (rng Fx) c= Y-section ((union (rng F)),p)
;
hence
Y-section ((union (rng F)),p) = union (rng Fx)
by A7; verum