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 AS: 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 Element of NAT such that
P1: for m being Element of NAT st N0 <= m holds
ASeq . N0 = ASeq . m by LME3;
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 13;
assume AS2: N <= m ; :: thesis: Union ASeq = ASeq . m
thus ASeq . m = Union ASeq :: thesis: verum

proof

now

let x be set ; :: thesis: ( x in Union ASeq implies b₁ in ASeq . m )
assume x in Union ASeq ; :: thesis: b₁ in ASeq . m
then consider n being Element of NAT such that
P2: x in ASeq . n by PROB_1:25;

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

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

then P21: ASeq . n c= ASeq . N by AS, PROB_1:def 7;
ASeq . N c= ASeq . M by AS2, P1;
then ASeq . n c= ASeq . m by P21, XBOOLE_1:1;
hence x in ASeq . m by P2; :: thesis: verum

end;

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

then ASeq . N = ASeq . n by P1;
then ASeq . n c= ASeq . M by P1, AS2;
hence x in ASeq . m by P2; :: thesis: verum

end;

end;

end;

then L1: Union ASeq c= ASeq . m by TARSKI:def 3;
ASeq . m c= Union ASeq by ABCMIZ_1:1;
hence ASeq . m = Union ASeq by L1, XBOOLE_0:def 10; :: thesis: verum

end;