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