let D be non empty set ; :: thesis: for f, g being FinSequence of D holds (f ^ g) /^ (len f) = g
let f, g be FinSequence of D; :: thesis: (f ^ g) /^ (len f) = g
thus (f ^ g) /^ (len f) = (f ^ g) /^ ((len f) + 0)
.= g /^ 0 by Th39
.= g by Th31 ; :: thesis: verum