let X be set ; :: thesis: for A1 being SetSequence of X st A1 is non-descending holds
for n being Element of NAT holds A1 . (n + 1) = ((Partial_Diff_Union A1) . (n + 1)) \/ (A1 . n)
let A1 be SetSequence of X; :: thesis: ( A1 is non-descending implies for n being Element of NAT holds A1 . (n + 1) = ((Partial_Diff_Union A1) . (n + 1)) \/ (A1 . n) )
assume A1: A1 is non-descending ; :: thesis: for n being Element of NAT holds A1 . (n + 1) = ((Partial_Diff_Union A1) . (n + 1)) \/ (A1 . n)
thus for n being Element of NAT holds A1 . (n + 1) = ((Partial_Diff_Union A1) . (n + 1)) \/ (A1 . n) :: thesis: verum

proof

let n be Element of NAT ; :: thesis: A1 . (n + 1) = ((Partial_Diff_Union A1) . (n + 1)) \/ (A1 . n)
A2: A1 . n c= A1 . (n + 1) by A1, PROB_2:7;
thus ((Partial_Diff_Union A1) . (n + 1)) \/ (A1 . n) = ((A1 . (n + 1)) \ ((Partial_Union A1) . n)) \/ (A1 . n) by PROB_3:def 3
.= ((A1 . (n + 1)) \ (A1 . n)) \/ (A1 . n) by A1, Lm2
.= (A1 . (n + 1)) \/ (A1 . n) by XBOOLE_1:39
.= A1 . (n + 1) by A2, XBOOLE_1:12 ; :: thesis: verum

end;