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

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

let n be Element of 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 V71() by PROB_2:7; :: thesis: verum