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_{1}[ 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_{1}[i] holds

S_{1}[i + 1]
_{1}[ 0 ]
_{1}[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 V75() 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

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

( k <= $1 & x in A1 . k ) );

A1: for i being Nat st S

S

proof

A6:
S
let i be Nat; :: thesis: ( S_{1}[i] implies S_{1}[i + 1] )

assume A2: ( x in (Partial_Union A1) . i implies ex k being Nat st

( k <= i & x in A1 . k ) ) ; :: thesis: S_{1}[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;

( k <= i + 1 & x in A1 . k ) ; :: thesis: verum

end;assume A2: ( x in (Partial_Union A1) . i implies ex k being Nat st

( k <= i & x in A1 . k ) ) ; :: thesis: S

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 ) ) )end;

hence
ex 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;

end;

case
x in (Partial_Union A1) . i
; :: thesis: ex k, k being Nat st

( k <= i + 1 & x in A1 . k )

( 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;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

( k <= i + 1 & x in A1 . k ) ; :: thesis: verum

proof

for n being Nat holds S
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;( 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

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 V75() 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