let f be non empty XFinSequence; :: thesis: f = <%(f . 0)%> ^ (f /^ 1)
thus f = (f | 1) ^ (f /^ 1)
.= <%(f . 0)%> ^ (f /^ 1) by Th1 ; :: thesis: verum