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 Th27;
( len p <= len q iff dom p c= dom q ) by Th28;
hence ( len p < len q iff dom p c< dom q ) by A1, XXREAL_0:1; :: thesis: verum