let n be Nat; :: thesis: for p being XFinSequence st len p <= n holds
p | n = p
let p be XFinSequence; :: thesis: ( len p <= n implies p | n = p )
assume len p <= n ; :: thesis: p | n = p
then (len p) /\ n = len p by NAT_1:47;
hence p | n = p by RELAT_1:97, XBOOLE_1:18; :: thesis: verum