let X be set ; :: thesis: 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 ; :: thesis: 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:]; :: thesis: 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 ; :: thesis: ( 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 ; :: thesis: ex G being SetSequence of Y st
( G is non-ascending & ( for n being Nat holds G . n = X-section ((E . n),x) ) )
deffunc H₁( 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 = H₁(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)

proof

let n be Nat; :: thesis: G . n = X-section ((E . n),x)
n is Element of NAT by ORDINAL1:def 12;
hence G . n = X-section ((E . n),x) by A2; :: thesis: verum

end;

take G ; :: thesis: ( 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; :: thesis: 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; :: thesis: verum