let X be set ; for Y being non empty set
for E being SetSequence of [:X,Y:]
for x being set st E is non-ascending holds
ex G being SetSequence of Y st
( G is non-ascending & ( for n being Nat holds G . n = X-section ((E . n),x) ) )
let Y be non empty set ; for E being SetSequence of [:X,Y:]
for x being set st E is non-ascending holds
ex G being SetSequence of Y st
( G is non-ascending & ( for n being Nat holds G . n = X-section ((E . n),x) ) )
let E be SetSequence of [:X,Y:]; for x being set st E is non-ascending holds
ex G being SetSequence of Y st
( G is non-ascending & ( for n being Nat holds G . n = X-section ((E . n),x) ) )
let x be set ; ( E is non-ascending implies ex G being SetSequence of Y st
( G is non-ascending & ( for n being Nat holds G . n = X-section ((E . n),x) ) ) )
assume A1:
E is non-ascending
; ex G being SetSequence of Y st
( G is non-ascending & ( for n being Nat holds G . n = X-section ((E . n),x) ) )
deffunc H1( Nat) -> Subset of Y = X-section ((E . $1),x);
consider G being Function of NAT,(bool Y) such that
A2:
for n being Element of NAT holds G . n = H1(n)
from FUNCT_2:sch 4();
reconsider G = G as SetSequence of Y ;
A3:
for n being Nat holds G . n = X-section ((E . n),x)
take
G
; ( G is non-ascending & ( for n being Nat holds G . n = X-section ((E . n),x) ) )
thus
G is non-ascending
by A1, A3, Th35; for n being Nat holds G . n = X-section ((E . n),x)
thus
for n being Nat holds G . n = X-section ((E . n),x)
by A3; verum