let D be set ; :: thesis: for p, q being FinSequence of D holds Union (p ^ q) = (Union p) \/ (Union q)
let p, q be FinSequence of D; :: thesis: Union (p ^ q) = (Union p) \/ (Union q)
union (rng (p ^ q)) = union ((rng p) \/ (rng q)) by FINSEQ_1:31
.= (Union p) \/ (Union q) by ZFMISC_1:78 ;
hence Union (p ^ q) = (Union p) \/ (Union q) ; :: thesis: verum