let D be non empty set ; for f, g being FinSequence of D holds ovlcon (f,g) = (ovlldiff (f,g)) ^ g
let f, g be FinSequence of D; 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; verum