let X be set ; :: thesis: for A1 being SetSequence of X st A1 is non-descending holds
( (Partial_Diff_Union A1) . 0 = A1 . 0 & ( for n being Nat holds (Partial_Diff_Union A1) . (n + 1) = (A1 . (n + 1)) \ (A1 . n) ) )
let A1 be SetSequence of X; :: thesis: ( A1 is non-descending implies ( (Partial_Diff_Union A1) . 0 = A1 . 0 & ( for n being Nat holds (Partial_Diff_Union A1) . (n + 1) = (A1 . (n + 1)) \ (A1 . n) ) ) )
assume A1: A1 is non-descending ; :: thesis: ( (Partial_Diff_Union A1) . 0 = A1 . 0 & ( for n being Nat holds (Partial_Diff_Union A1) . (n + 1) = (A1 . (n + 1)) \ (A1 . n) ) )
thus (Partial_Diff_Union A1) . 0 = A1 . 0 by PROB_3:def 3; :: thesis: for n being Nat holds (Partial_Diff_Union A1) . (n + 1) = (A1 . (n + 1)) \ (A1 . n)
let n be Nat; :: thesis: (Partial_Diff_Union A1) . (n + 1) = (A1 . (n + 1)) \ (A1 . n)
thus (Partial_Diff_Union A1) . (n + 1) = (A1 . (n + 1)) \ ((Partial_Union A1) . n) by PROB_3:def 3
.= (A1 . (n + 1)) \ (A1 . n) by A1, Lm2 ; :: thesis: verum