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 )

proof

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

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

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

case n = 0 ; :: thesis: ( x in A1 . n & ( for k being Nat st k < n holds
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;

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

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

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: verum

end;

end;

end;

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

end;

assume that
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 ) )

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

case n = 0 ; :: thesis: x in (Partial_Diff_Union A1) . n

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

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

proof

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;

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: verum

end;

end;

end;

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