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

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