let g1, g2 be FinSequence; :: thesis: ( len g1 = (len f) -' 1 & ( for i being Element of NAT st 1 <= i & i < len f holds
g1 . i = [(f . i),(f . (i + 1))] ) & len g2 = (len f) -' 1 & ( for i being Element of NAT st 1 <= i & i < len f holds
g2 . i = [(f . i),(f . (i + 1))] ) implies g1 = g2 )
assume A4: ( len g1 = (len f) -' 1 & ( for i being Element of NAT st 1 <= i & i < len f holds
g1 . i = [(f . i),(f . (i + 1))] ) & len g2 = (len f) -' 1 & ( for i being Element of NAT st 1 <= i & i < len f holds
g2 . i = [(f . i),(f . (i + 1))] ) ) ; :: thesis: g1 = g2

per cases ( len f >= 1 or len f < 1 ) ;

suppose A5: len f >= 1 ; :: thesis: g1 = g2

for j being Nat st 1 <= j & j <= len g1 holds
g1 . j = g2 . j

proof

let j be Nat; :: thesis: ( 1 <= j & j <= len g1 implies g1 . j = g2 . j )
assume A6: ( 1 <= j & j <= len g1 ) ; :: thesis: g1 . j = g2 . j
A7: j in NAT by ORDINAL1:def 13;
len f < (len f) + 1 by NAT_1:13;
then (len f) - 1 < len f by XREAL_1:21;
then len g1 < len f by A4, A5, XREAL_1:235;
then A8: j < len f by A6, XXREAL_0:2;
then g1 . j = [(f . j),(f . (j + 1))] by A4, A6, A7;
hence g1 . j = g2 . j by A4, A6, A7, A8; :: thesis: verum

end;

hence g1 = g2 by A4, FINSEQ_1:18; :: thesis: verum

end;

suppose len f < 1 ; :: thesis: g1 = g2

then (len f) + 1 <= 1 by NAT_1:13;
then ((len f) + 1) - 1 <= 1 - 1 by XREAL_1:11;
then A9: len f = 0 ;
0 - 1 < 0 ;
then ( len g1 = 0 & len g2 = 0 ) by A4, A9, XREAL_0:def 2;
then g1 = {} ;
hence g1 = g2 by A4; :: thesis: verum

end;

end;