let v1, v2 be FinSequence of REAL ; :: thesis: ( len v1 = 0 & len v2 = 0 & rng v1 = rng v2 & v1 is increasing & v2 is increasing implies v1 = v2 )
assume ( len v1 = 0 & len v2 = 0 & rng v1 = rng v2 & v1 is increasing & v2 is increasing ) ; :: thesis: v1 = v2
then ( v1 = {} & v2 = {} ) ;
hence v1 = v2 ; :: thesis: verum