let X be set ; :: thesis: for A1 being SetSequence of X st A1 is non-descending holds
for n being Nat holds (Partial_Union A1) . n = A1 . n
let A1 be SetSequence of X; :: thesis: ( A1 is non-descending implies for n being Nat holds (Partial_Union A1) . n = A1 . n )
defpred S₁[ Nat] means (Partial_Union A1) . $1 = A1 . $1;
assume A1: A1 is non-descending ; :: thesis: for n being Nat holds (Partial_Union A1) . n = A1 . n
A2: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A3: S₁[k] ; :: thesis: S₁[k + 1]
A4: A1 . k c= A1 . (k + 1) by A1, PROB_2:7;
thus (Partial_Union A1) . (k + 1) = (A1 . k) \/ (A1 . (k + 1)) by A3, PROB_3:def 2
.= A1 . (k + 1) by A4, XBOOLE_1:12 ; :: thesis: verum

end;

A5: S₁[ 0 ] by PROB_3:def 2;
thus for k being Nat holds S₁[k] from NAT_1:sch 2(A5, A2); :: thesis: verum