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 S1[ 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 S1[i] holds
S1[i + 1]
proof
let i be Nat; :: thesis: ( S1[i] implies S1[i + 1] )
assume A2: ( x in (Partial_Union A1) . i implies ex k being Nat st
( k <= i & x in A1 . k ) ) ; :: thesis: S1[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: S1[ 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 S1[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