let p, q be FinSequence; :: thesis: ( len p < len q iff dom p c< dom q )
A: ( len p <= len q iff dom p c= dom q ) by Th32;
( len p = len q iff dom p = dom q ) by Th31;
hence ( len p < len q iff dom p c< dom q ) by A, XBOOLE_0:def 8, XXREAL_0:1; :: thesis: verum