let n be Nat; :: thesis: for X, 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, 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: S₁[ 0 ]

proof

assume A2: 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 A2, Def2; :: thesis: verum

end;

A3: for i being Nat st S₁[i] holds
S₁[i + 1]

proof

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

now

per cases ( x in (Partial_Union A1) . i or x in A1 . (i + 1) ) by A5, A6, 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
A7: ( k <= i & x in A1 . k ) by A4;
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 A7, 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;

for n being Nat holds S₁[n] from NAT_1:sch 2(A1, A3);
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 Th11;
then A10: x in (Partial_Union A1) . i by A9;
A11: ( n in NAT & i in NAT ) by ORDINAL1:def 13;
Partial_Union A1 is non-descending by Th13;
then (Partial_Union A1) . i c= (Partial_Union A1) . n by A8, A11, PROB_1:def 7;
hence x in (Partial_Union A1) . n by A10; :: thesis: verum