let n be Nat; :: thesis: for x being object

for X being set

for A1 being SetSequence of X holds

( x in (Partial_Diff_Union A1) . n iff ( x in A1 . n & ( for k being Nat st k < n holds

not x in A1 . k ) ) )

let x be object ; :: thesis: for X being set

for A1 being SetSequence of X holds

( x in (Partial_Diff_Union A1) . n iff ( x in A1 . n & ( for k being Nat st k < n holds

not x in A1 . k ) ) )

let X be set ; :: thesis: for A1 being SetSequence of X holds

( x in (Partial_Diff_Union A1) . n iff ( x in A1 . n & ( for k being Nat st k < n holds

not x in A1 . k ) ) )

let A1 be SetSequence of X; :: thesis: ( x in (Partial_Diff_Union A1) . n iff ( x in A1 . n & ( for k being Nat st k < n holds

not x in A1 . k ) ) )

thus ( x in (Partial_Diff_Union A1) . n implies ( x in A1 . n & ( for k being Nat st k < n holds

not x in A1 . k ) ) ) :: thesis: ( x in A1 . n & ( for k being Nat st k < n holds

not x in A1 . k ) implies x in (Partial_Diff_Union A1) . n )

A5: x in A1 . n and

A6: for k being Nat st k < n holds

not x in A1 . k ; :: thesis: x in (Partial_Diff_Union A1) . n

for X being set

for A1 being SetSequence of X holds

( x in (Partial_Diff_Union A1) . n iff ( x in A1 . n & ( for k being Nat st k < n holds

not x in A1 . k ) ) )

let x be object ; :: thesis: for X being set

for A1 being SetSequence of X holds

( x in (Partial_Diff_Union A1) . n iff ( x in A1 . n & ( for k being Nat st k < n holds

not x in A1 . k ) ) )

let X be set ; :: thesis: for A1 being SetSequence of X holds

( x in (Partial_Diff_Union A1) . n iff ( x in A1 . n & ( for k being Nat st k < n holds

not x in A1 . k ) ) )

let A1 be SetSequence of X; :: thesis: ( x in (Partial_Diff_Union A1) . n iff ( x in A1 . n & ( for k being Nat st k < n holds

not x in A1 . k ) ) )

thus ( x in (Partial_Diff_Union A1) . n implies ( x in A1 . n & ( for k being Nat st k < n holds

not x in A1 . k ) ) ) :: thesis: ( x in A1 . n & ( for k being Nat st k < n holds

not x in A1 . k ) implies x in (Partial_Diff_Union A1) . n )

proof

assume that
assume A1:
x in (Partial_Diff_Union A1) . n
; :: thesis: ( x in A1 . n & ( for k being Nat st k < n holds

not x in A1 . k ) )

not x in A1 . k ) ) ; :: thesis: verum

end;not x in A1 . k ) )

now :: thesis: ( ( n = 0 & x in A1 . n & ( for k being Nat st k < n holds

not x in A1 . k ) ) or ( ex n1 being Nat st n = n1 + 1 & x in A1 . n & ( for k being Nat st k < n holds

not x in A1 . k ) ) )end;

hence
( x in A1 . n & ( for k being Nat st k < n holds not x in A1 . k ) ) or ( ex n1 being Nat st n = n1 + 1 & x in A1 . n & ( for k being Nat st k < n holds

not x in A1 . k ) ) )

per cases
( n = 0 or ex n1 being Nat st n = n1 + 1 )
by NAT_1:6;

end;

case
n = 0
; :: thesis: ( x in A1 . n & ( for k being Nat st k < n holds

not x in A1 . k ) )

not x in A1 . k ) )

hence
( x in A1 . n & ( for k being Nat st k < n holds

not x in A1 . k ) ) by A1, Def3; :: thesis: verum

end;not x in A1 . k ) ) by A1, Def3; :: thesis: verum

case
ex n1 being Nat st n = n1 + 1
; :: thesis: ( x in A1 . n & ( for k being Nat st k < n holds

not x in A1 . k ) )

not x in A1 . k ) )

then consider n1 being Nat such that

A2: n = n1 + 1 ;

A3: x in (A1 . (n1 + 1)) \ ((Partial_Union A1) . n1) by A1, A2, Def3;

then A4: not x in (Partial_Union A1) . n1 by XBOOLE_0:def 5;

for k being Nat st k < n holds

not x in A1 . k

not x in A1 . k ) ) by A2, A3, XBOOLE_0:def 5; :: thesis: verum

end;A2: n = n1 + 1 ;

A3: x in (A1 . (n1 + 1)) \ ((Partial_Union A1) . n1) by A1, A2, Def3;

then A4: not x in (Partial_Union A1) . n1 by XBOOLE_0:def 5;

for k being Nat st k < n holds

not x in A1 . k

proof

hence
( x in A1 . n & ( for k being Nat st k < n holds
let k be Nat; :: thesis: ( k < n implies not x in A1 . k )

assume k < n ; :: thesis: not x in A1 . k

then k <= n1 by A2, NAT_1:13;

hence not x in A1 . k by A4, Th13; :: thesis: verum

end;assume k < n ; :: thesis: not x in A1 . k

then k <= n1 by A2, NAT_1:13;

hence not x in A1 . k by A4, Th13; :: thesis: verum

not x in A1 . k ) ) by A2, A3, XBOOLE_0:def 5; :: thesis: verum

not x in A1 . k ) ) ; :: thesis: verum

A5: x in A1 . n and

A6: for k being Nat st k < n holds

not x in A1 . k ; :: thesis: x in (Partial_Diff_Union A1) . n

now :: thesis: ( ( n = 0 & x in (Partial_Diff_Union A1) . n ) or ( ex n1 being Nat st n = n1 + 1 & x in (Partial_Diff_Union A1) . n ) )end;

hence
x in (Partial_Diff_Union A1) . n
; :: thesis: verumper cases
( n = 0 or ex n1 being Nat st n = n1 + 1 )
by NAT_1:6;

end;

case
ex n1 being Nat st n = n1 + 1
; :: thesis: x in (Partial_Diff_Union A1) . n

then consider n1 being Nat such that

A7: n = n1 + 1 ;

for k being Nat st k <= n1 holds

not x in A1 . k

then x in (A1 . (n1 + 1)) \ ((Partial_Union A1) . n1) by A5, A7, XBOOLE_0:def 5;

hence x in (Partial_Diff_Union A1) . n by A7, Def3; :: thesis: verum

end;A7: n = n1 + 1 ;

for k being Nat st k <= n1 holds

not x in A1 . k

proof

then
not x in (Partial_Union A1) . n1
by Th13;
let k be Nat; :: thesis: ( k <= n1 implies not x in A1 . k )

assume k <= n1 ; :: thesis: not x in A1 . k

then k < n1 + 1 by NAT_1:13;

hence not x in A1 . k by A6, A7; :: thesis: verum

end;assume k <= n1 ; :: thesis: not x in A1 . k

then k < n1 + 1 by NAT_1:13;

hence not x in A1 . k by A6, A7; :: thesis: verum

then x in (A1 . (n1 + 1)) \ ((Partial_Union A1) . n1) by A5, A7, XBOOLE_0:def 5;

hence x in (Partial_Diff_Union A1) . n by A7, Def3; :: thesis: verum