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