let X be non empty set ; :: thesis: for Y being set
for E being SetSequence of [:X,Y:]
for x being set st E is non-descending holds
ex G being SetSequence of X st
( G is non-descending & ( for n being Nat holds G . n = Y-section ((E . n),x) ) )
let Y be set ; :: thesis: for E being SetSequence of [:X,Y:]
for x being set st E is non-descending holds
ex G being SetSequence of X st
( G is non-descending & ( for n being Nat holds G . n = Y-section ((E . n),x) ) )
let E be SetSequence of [:X,Y:]; :: thesis: for x being set st E is non-descending holds
ex G being SetSequence of X st
( G is non-descending & ( for n being Nat holds G . n = Y-section ((E . n),x) ) )
let x be set ; :: thesis: ( E is non-descending implies ex G being SetSequence of X st
( G is non-descending & ( for n being Nat holds G . n = Y-section ((E . n),x) ) ) )
assume A1: E is non-descending ; :: thesis: ex G being SetSequence of X st
( G is non-descending & ( for n being Nat holds G . n = Y-section ((E . n),x) ) )
deffunc H₁( Nat) -> Subset of X = Y-section ((E . $1),x);
consider G being Function of NAT,(bool X) 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 X ;
A3: for n being Nat holds G . n = Y-section ((E . n),x)

proof

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

end;

take G ; :: thesis: ( G is non-descending & ( for n being Nat holds G . n = Y-section ((E . n),x) ) )
thus G is non-descending by A1, A3, Th34; :: thesis: for n being Nat holds G . n = Y-section ((E . n),x)
thus for n being Nat holds G . n = Y-section ((E . n),x) by A3; :: thesis: verum