let X be non empty set ; :: thesis: for Y, x being set
for E being SetSequence of [:X,Y:]
for G being SetSequence of X st E is non-descending & ( for n being Nat holds G . n = Y-section ((E . n),x) ) holds
G is non-descending
let Y, x be set ; :: thesis: for E being SetSequence of [:X,Y:]
for G being SetSequence of X st E is non-descending & ( for n being Nat holds G . n = Y-section ((E . n),x) ) holds
G is non-descending
let E be SetSequence of [:X,Y:]; :: thesis: for G being SetSequence of X st E is non-descending & ( for n being Nat holds G . n = Y-section ((E . n),x) ) holds
G is non-descending
let G be SetSequence of X; :: thesis: ( E is non-descending & ( for n being Nat holds G . n = Y-section ((E . n),x) ) implies G is non-descending )
assume that
A1: E is non-descending and
A2: for n being Nat holds G . n = Y-section ((E . n),x) ; :: thesis: G is non-descending
for n being Nat holds G . n c= G . (n + 1)

proof

let n be Nat; :: thesis: G . n c= G . (n + 1)
Y-section ((E . n),x) c= Y-section ((E . (n + 1)),x) by Th15, A1, KURATO_0:def 4;
then G . n c= Y-section ((E . (n + 1)),x) by A2;
hence G . n c= G . (n + 1) by A2; :: thesis: verum

end;

hence G is non-descending by KURATO_0:def 4; :: thesis: verum