let D be non empty set ; :: thesis: for f, g being FinSequence of D holds ovlcon f,g = (ovlldiff f,g) ^ g
let f, g be FinSequence of D; :: thesis: ovlcon f,g = (ovlldiff f,g) ^ g
ovlcon f,g = (ovlldiff f,g) ^ ((ovlpart f,g) ^ (ovlrdiff f,g)) by FINSEQ_8:12;
hence ovlcon f,g = (ovlldiff f,g) ^ g by Th32; :: thesis: verum