let f, g be XFinSequence; :: 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