let X be set ; :: thesis: for A1 being SetSequence of X holds Partial_Diff_Union A1 is disjoint_valued
let A1 be SetSequence of X; :: thesis: Partial_Diff_Union A1 is disjoint_valued
for m, n being Nat st m <> n holds
(Partial_Diff_Union A1) . n misses (Partial_Diff_Union A1) . m

proof

let m, n be Nat; :: thesis: ( m <> n implies (Partial_Diff_Union A1) . n misses (Partial_Diff_Union A1) . m )
assume A1: m <> n ; :: thesis: (Partial_Diff_Union A1) . n misses (Partial_Diff_Union A1) . m
assume (Partial_Diff_Union A1) . n meets (Partial_Diff_Union A1) . m ; :: thesis: contradiction
then consider x being set such that
A2: x in (Partial_Diff_Union A1) . n and
A3: x in (Partial_Diff_Union A1) . m by XBOOLE_0:3;

per cases ( m < n or n < m ) by A1, XXREAL_0:1;

suppose m < n ; :: thesis: contradiction

then not x in A1 . m by A2, Th19;
hence contradiction by A3, Th19; :: thesis: verum

end;

suppose n < m ; :: thesis: contradiction

then not x in A1 . n by A3, Th19;
hence contradiction by A2, Th19; :: thesis: verum

end;

end;

end;

hence Partial_Diff_Union A1 is disjoint_valued by Def4; :: thesis: verum