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 ((meet (rng F)),p) = meet (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 ((meet (rng F)),p) = meet (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 ((meet (rng F)),p) = meet (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 ((meet (rng F)),p) = meet (rng Fy)
let Fy be SetSequence of Y; ( ( for n being Nat holds Fy . n = X-section ((F . n),p) ) implies X-section ((meet (rng F)),p) = meet (rng Fy) )
assume A2:
for n being Nat holds Fy . n = X-section ((F . n),p)
; X-section ((meet (rng F)),p) = meet (rng Fy)
then A7:
X-section ((meet (rng F)),p) c= meet (rng Fy)
;
then
meet (rng Fy) c= X-section ((meet (rng F)),p)
;
hence
X-section ((meet (rng F)),p) = meet (rng Fy)
by A7; verum