let f1, f2 be FinSequence of LTLB_WFF ; :: thesis: ( ( len f > 0 & len f1 = len f & f1 . 1 = f . 1 & ( for i being Nat st 1 <= i & i < len f holds
f1 . (i + 1) = (f1 /. i) '&&' (f /. (i + 1)) ) & len f2 = len f & f2 . 1 = f . 1 & ( for i being Nat st 1 <= i & i < len f holds
f2 . (i + 1) = (f2 /. i) '&&' (f /. (i + 1)) ) implies f1 = f2 ) & ( not len f > 0 & f1 = <*TVERUM*> & f2 = <*TVERUM*> implies f1 = f2 ) )
thus ( len f > 0 & len f1 = len f & f1 . 1 = f . 1 & ( for i being Nat st 1 <= i & i < len f holds
f1 . (i + 1) = (f1 /. i) '&&' (f /. (i + 1)) ) & len f2 = len f & f2 . 1 = f . 1 & ( for i being Nat st 1 <= i & i < len f holds
f2 . (i + 1) = (f2 /. i) '&&' (f /. (i + 1)) ) implies f1 = f2 ) :: thesis: ( not len f > 0 & f1 = <*TVERUM*> & f2 = <*TVERUM*> implies f1 = f2 )
proof
assume that
A5: len f > 0 and
A6: len f1 = len f and
A7: f1 . 1 = f . 1 and
A8: for i being Nat st 1 <= i & i < len f holds
f1 . (i + 1) = (f1 /. i) '&&' (f /. (i + 1)) and
A9: len f2 = len f and
A10: f2 . 1 = f . 1 and
A11: for i being Nat st 1 <= i & i < len f holds
f2 . (i + 1) = (f2 /. i) '&&' (f /. (i + 1)) ; :: thesis: f1 = f2
A12: 1 <= len f2 by NAT_1:25, A5, A9;
1 <= len f1 by A6, NAT_1:25, A5;
then A13: f1 /. 1 = f1 . 1 by FINSEQ_4:15
.= f2 /. 1 by FINSEQ_4:15, A12, A10, A7 ;
A14: now :: thesis: for n being Element of NAT st n in dom f1 holds
f1 . n = f2 . n
defpred S1[ Nat] means ( $1 < len f implies f1 . ($1 + 1) = f2 . ($1 + 1) );
let n be Element of NAT ; :: thesis: ( n in dom f1 implies f1 . n = f2 . n )
set m = n -' 1;
assume A15: n in dom f1 ; :: thesis: f1 . n = f2 . n
then 1 + (- 1) <= n + (- 1) by XREAL_1:6, FINSEQ_3:25;
then A16: n -' 1 = n - 1 by XREAL_0:def 2;
then A17: (n -' 1) + 1 <= len f by A6, A15, FINSEQ_3:25;
A18: for i being Nat st S1[i] holds
S1[i + 1]
proof
let i be Nat; :: thesis: ( S1[i] implies S1[i + 1] )
assume A19: S1[i] ; :: thesis: S1[i + 1]
assume A20: i + 1 < len f ; :: thesis: f1 . ((i + 1) + 1) = f2 . ((i + 1) + 1)
A21: 1 <= i + 1 by NAT_1:25;
per cases ( i = 0 or i >= 1 ) by NAT_1:25;
suppose A22: i = 0 ; :: thesis: f1 . ((i + 1) + 1) = f2 . ((i + 1) + 1)
thus f1 . ((i + 1) + 1) = (f1 /. (i + 1)) '&&' (f /. ((i + 1) + 1)) by A20, A21, A8
.= f2 . ((i + 1) + 1) by A20, A11, A22, A13 ; :: thesis: verum
end;
suppose i >= 1 ; :: thesis: f1 . ((i + 1) + 1) = f2 . ((i + 1) + 1)
f1 /. (i + 1) = f2 . (i + 1) by A19, A20, NAT_1:12, FINSEQ_4:15, A6
.= f2 /. (i + 1) by FINSEQ_4:15, A21, A9, A20 ;
hence f1 . ((i + 1) + 1) = (f2 /. (i + 1)) '&&' (f /. ((i + 1) + 1)) by A20, A21, A8
.= f2 . ((i + 1) + 1) by A20, A21, A11 ;
:: thesis: verum
end;
end;
end;
A23: S1[ 0 ] by A7, A10;
A24: for i being Nat holds S1[i] from NAT_1:sch 2(A23, A18);
thus f1 . n = f2 . n by A16, A24, A17, XREAL_1:145; :: thesis: verum
end;
dom f1 = dom f2 by A6, A9, FINSEQ_3:29;
hence f1 = f2 by A14, PARTFUN1:5; :: thesis: verum
end;
thus ( not len f > 0 & f1 = <*TVERUM*> & f2 = <*TVERUM*> implies f1 = f2 ) ; :: thesis: verum