let p, q be XFinSequence; :: thesis: (p ^ q) /^ (len p) = q
thus (p ^ q) /^ (len p) = (p ^ q) /^ ((len p) + 0)
.= q /^ 0 by Th11
.= q by Th10 ; :: thesis: verum