let n be Nat; :: thesis: for x being object
for X being set
for A1 being SetSequence of X holds
( x in (Partial_Union A1) . n iff ex k being Nat st
( k <= n & x in A1 . k ) )
let x be object ; :: thesis: for X being set
for A1 being SetSequence of X holds
( x in (Partial_Union A1) . n iff ex k being Nat st
( k <= n & x in A1 . k ) )
let X be set ; :: thesis: for A1 being SetSequence of X holds
( x in (Partial_Union A1) . n iff ex k being Nat st
( k <= n & x in A1 . k ) )
let A1 be SetSequence of X; :: thesis: ( x in (Partial_Union A1) . n iff ex k being Nat st
( k <= n & x in A1 . k ) )
defpred S₁[ Nat] means ( x in (Partial_Union A1) . $1 implies ex k being Nat st
( k <= $1 & x in A1 . k ) );
A1: for i being Nat st S₁[i] holds
S₁[i + 1]

proof

let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume A2: ( x in (Partial_Union A1) . i implies ex k being Nat st
( k <= i & x in A1 . k ) ) ; :: thesis: S₁[i + 1]
assume A3: x in (Partial_Union A1) . (i + 1) ; :: thesis: ex k being Nat st
( k <= i + 1 & x in A1 . k )
A4: (Partial_Union A1) . (i + 1) = ((Partial_Union A1) . i) \/ (A1 . (i + 1)) by Def2;

now :: thesis: ( ( x in (Partial_Union A1) . i & ex k, k being Nat st
( k <= i + 1 & x in A1 . k ) ) or ( x in A1 . (i + 1) & ex k being Nat st
( k <= i + 1 & x in A1 . k ) ) )

per cases ( x in (Partial_Union A1) . i or x in A1 . (i + 1) ) by A3, A4, XBOOLE_0:def 3;

case x in (Partial_Union A1) . i ; :: thesis: ex k, k being Nat st
( k <= i + 1 & x in A1 . k )

then consider k being Nat such that
A5: ( k <= i & x in A1 . k ) by A2;
take k = k; :: thesis: ex k being Nat st
( k <= i + 1 & x in A1 . k )
thus ex k being Nat st
( k <= i + 1 & x in A1 . k ) by A5, NAT_1:12; :: thesis: verum

end;

case x in A1 . (i + 1) ; :: thesis: ex k being Nat st
( k <= i + 1 & x in A1 . k )

hence ex k being Nat st
( k <= i + 1 & x in A1 . k ) ; :: thesis: verum

end;

end;

end;

hence ex k being Nat st
( k <= i + 1 & x in A1 . k ) ; :: thesis: verum

end;

A6: S₁[ 0 ]

proof

assume A7: x in (Partial_Union A1) . 0 ; :: thesis: ex k being Nat st
( k <= 0 & x in A1 . k )
take 0 ; :: thesis: ( 0 <= 0 & x in A1 . 0 )
thus ( 0 <= 0 & x in A1 . 0 ) by A7, Def2; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A6, A1);
hence ( x in (Partial_Union A1) . n implies ex k being Nat st
( k <= n & x in A1 . k ) ) ; :: thesis: ( ex k being Nat st
( k <= n & x in A1 . k ) implies x in (Partial_Union A1) . n )
given i being Nat such that A8: i <= n and
A9: x in A1 . i ; :: thesis: x in (Partial_Union A1) . n
A1 . i c= (Partial_Union A1) . i by Th9;
then A10: x in (Partial_Union A1) . i by A9;
A11: Partial_Union A1 is non-descending by Th11;
(Partial_Union A1) . i c= (Partial_Union A1) . n by A8, A11, PROB_1:def 5;
hence x in (Partial_Union A1) . n by A10; :: thesis: verum