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 Th31; :: thesis: verum