let g1, g2 be FinSequence; :: thesis: ( len g1 = (len f) -' 1 & ( for i being Nat st 1 <= i & i < len f holds
g1 . i = [(f . i),(f . (i + 1))] ) & len g2 = (len f) -' 1 & ( for i being Nat st 1 <= i & i < len f holds
g2 . i = [(f . i),(f . (i + 1))] ) implies g1 = g2 )
assume that
A6: len g1 = (len f) -' 1 and
A7: for i being Nat st 1 <= i & i < len f holds
g1 . i = [(f . i),(f . (i + 1))] and
A8: len g2 = (len f) -' 1 and
A9: for i being 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 A10: 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 that
A11: 1 <= j and
A12: j <= len g1 ; :: thesis: g1 . j = g2 . j
len f < (len f) + 1 by NAT_1:13;
then (len f) - 1 < len f by XREAL_1:19;
then len g1 < len f by A6, A10, XREAL_1:233;
then A13: ( j in NAT & j < len f ) by A12, ORDINAL1:def 12, XXREAL_0:2;
then g1 . j = [(f . j),(f . (j + 1))] by A7, A11;
hence g1 . j = g2 . j by A9, A11, A13; :: thesis: verum
end;
hence g1 = g2 by A6, A8, FINSEQ_1:14; :: 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:9;
then A14: len f = 0 ;
0 - 1 < 0 ;
then g1 = {} by A6, A14, XREAL_0:def 2;
hence g1 = g2 by A6, A8; :: thesis: verum
end;
end;