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()
now :: thesis: for n being Nat holds (Partial_Union A1) . n c= (Partial_Union A1) . (n + 1)
let 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;
hence Partial_Union A1 is V75() by PROB_2:7; :: thesis: verum