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