let E be non empty finite set ; :: thesis: for ASeq being SetSequence of E st ASeq is non-descending holds
ex N being Nat st
for m being Nat st N <= m holds
Union ASeq = ASeq . m
let ASeq be SetSequence of E; :: thesis: ( ASeq is non-descending implies ex N being Nat st
for m being Nat st N <= m holds
Union ASeq = ASeq . m )
assume A1: ASeq is non-descending ; :: thesis: ex N being Nat st
for m being Nat st N <= m holds
Union ASeq = ASeq . m
then consider N0 being Nat such that
A2: for m being Nat st N0 <= m holds
ASeq . N0 = ASeq . m by Th16;
reconsider N = N0 as Nat ;
take N ; :: thesis: for m being Nat st N <= m holds
Union ASeq = ASeq . m
let m be Nat; :: thesis: ( N <= m implies Union ASeq = ASeq . m )
reconsider M = m as Element of NAT by ORDINAL1:def 12;
assume A3: N <= m ; :: thesis: Union ASeq = ASeq . m

now :: thesis: for x being object st x in Union ASeq holds
x in ASeq . m

let x be object ; :: thesis: ( x in Union ASeq implies b₁ in ASeq . m )
assume x in Union ASeq ; :: thesis: b₁ in ASeq . m
then consider n being Nat such that
A4: x in ASeq . n by PROB_1:12;

per cases ( n < N or N <= n ) ;

suppose A5: n < N ; :: thesis: b₁ in ASeq . m

A6: ASeq . N c= ASeq . M by A2, A3;
ASeq . n c= ASeq . N by A1, A5, PROB_1:def 5;
then ASeq . n c= ASeq . m by A6;
hence x in ASeq . m by A4; :: thesis: verum

end;

suppose N <= n ; :: thesis: b₁ in ASeq . m

then ASeq . N = ASeq . n by A2;
then ASeq . n c= ASeq . M by A2, A3;
hence x in ASeq . m by A4; :: thesis: verum

end;

end;

end;

then A7: Union ASeq c= ASeq . m ;
ASeq . m c= Union ASeq by ABCMIZ_1:1;
hence ASeq . m = Union ASeq by A7; :: thesis: verum