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 that
A1: len v1 = 0 and
A2: len v2 = 0 and
rng v1 = rng v2 and
v1 is increasing and
v2 is increasing ; :: thesis: v1 = v2
v1 = {} by A1;
hence v1 = v2 by A2; :: thesis: verum