let f, g be FinSequence; :: thesis: (f ^ g) /^ (len f) = g
thus (f ^ g) /^ (len f) = (f ^ g) /^ ((len f) + 0)
.= g /^ 0 by Th36
.= g ; :: thesis: verum