let X be set ; :: thesis: for Y being non empty set
for x being set
for E being SetSequence of [:X,Y:]
for G being SetSequence of Y st E is non-descending & ( for n being Nat holds G . n = X-section ((E . n),x) ) holds
G is non-descending
let Y be non empty set ; :: thesis: for x being set
for E being SetSequence of [:X,Y:]
for G being SetSequence of Y st E is non-descending & ( for n being Nat holds G . n = X-section ((E . n),x) ) holds
G is non-descending
let x be set ; :: thesis: for E being SetSequence of [:X,Y:]
for G being SetSequence of Y st E is non-descending & ( for n being Nat holds G . n = X-section ((E . n),x) ) holds
G is non-descending
let E be SetSequence of [:X,Y:]; :: thesis: for G being SetSequence of Y st E is non-descending & ( for n being Nat holds G . n = X-section ((E . n),x) ) holds
G is non-descending
let G be SetSequence of Y; :: thesis: ( E is non-descending & ( for n being Nat holds G . n = X-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 = X-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)
X-section ((E . n),x) c= X-section ((E . (n + 1)),x) by Th14, A1, KURATO_0:def 4;
then G . n c= X-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