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