let X be set ; :: thesis: for A1 being SetSequence of X holds Partial_Union A1 is V75()

let A1 be SetSequence of X; :: thesis: Partial_Union A1 is V75()

let A1 be SetSequence of X; :: thesis: Partial_Union A1 is V75()

now :: thesis: for n being Nat holds (Partial_Union A1) . n c= (Partial_Union A1) . (n + 1)

hence
Partial_Union A1 is V75()
by PROB_2:7; :: thesis: verumlet n be Nat; :: thesis: (Partial_Union A1) . n c= (Partial_Union A1) . (n + 1)

(Partial_Union A1) . (n + 1) = ((Partial_Union A1) . n) \/ (A1 . (n + 1)) by Def2;

hence (Partial_Union A1) . n c= (Partial_Union A1) . (n + 1) by XBOOLE_1:7; :: thesis: verum

end;(Partial_Union A1) . (n + 1) = ((Partial_Union A1) . n) \/ (A1 . (n + 1)) by Def2;

hence (Partial_Union A1) . n c= (Partial_Union A1) . (n + 1) by XBOOLE_1:7; :: thesis: verum