let n be Nat; :: thesis:
let x be object ; :: thesis:
let X be set ; :: thesis:
let A1 be SetSequence of X; :: thesis:
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:

proof

assume A1: x in (Partial_Diff_Union A1) . n ; :: thesis:

now :: thesis:

per cases by NAT_1:6;

case n = 0 ; :: thesis:

hence ( x in A1 . n & ( for k being Nat st k < n holds
not x in A1 . k ) ) by A1, Def3; :: thesis:

end;

case ex n1 being Nat st n = n1 + 1 ; :: thesis:

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

proof

let k be Nat; :: thesis:
assume k < n ; :: thesis:
then k <= n1 by A2, NAT_1:13;
hence not x in A1 . k by A4, Th13; :: thesis:

end;

hence ( x in A1 . n & ( for k being Nat st k < n holds
not x in A1 . k ) ) by A2, A3, XBOOLE_0:def 5; :: thesis:

end;

end;

end;

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

end;

assume that
A5: x in A1 . n and
A6: for k being Nat st k < n holds
not x in A1 . k ; :: thesis:

now :: thesis:

per cases by NAT_1:6;

case n = 0 ; :: thesis:

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

end;

case ex n1 being Nat st n = n1 + 1 ; :: thesis:

then consider n1 being Nat such that
A7: n = n1 + 1 ;
for k being Nat st k <= n1 holds
not x in A1 . k

proof

let k be Nat; :: thesis:
assume k <= n1 ; :: thesis:
then k < n1 + 1 by NAT_1:13;
hence not x in A1 . k by A6, A7; :: thesis:

end;

then not x in (Partial_Union A1) . n1 by Th13;
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:

end;

end;

end;

hence x in (Partial_Diff_Union A1) . n ; :: thesis: