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