let f1, f2 be FinSequence of LTLB_WFF ; :: thesis: ( ( len f > 0 & len f1 = len f & f1 . 1 = (f /. 1) => A & ( for i being Element of NAT st 1 <= i & i < len f holds
f1 . (i + 1) = (f /. (i + 1)) => (f1 /. i) ) & len f2 = len f & f2 . 1 = (f /. 1) => A & ( for i being Element of NAT st 1 <= i & i < len f holds
f2 . (i + 1) = (f /. (i + 1)) => (f2 /. i) ) implies f1 = f2 ) & ( not len f > 0 & f1 = <*> LTLB_WFF & f2 = <*> LTLB_WFF implies f1 = f2 ) )
thus ( len f > 0 & len f1 = len f & f1 . 1 = (f /. 1) => A & ( for i being Element of NAT st 1 <= i & i < len f holds
f1 . (i + 1) = (f /. (i + 1)) => (f1 /. i) ) & len f2 = len f & f2 . 1 = (f /. 1) => A & ( for i being Element of NAT st 1 <= i & i < len f holds
f2 . (i + 1) = (f /. (i + 1)) => (f2 /. i) ) implies f1 = f2 ) :: thesis: ( not len f > 0 & f1 = <*> LTLB_WFF & f2 = <*> LTLB_WFF implies f1 = f2 )

proof

assume that
A5: len f > 0 and
A6: len f1 = len f and
A7: f1 . 1 = (f /. 1) => A and
A8: for i being Element of NAT st 1 <= i & i < len f holds
f1 . (i + 1) = (f /. (i + 1)) => (f1 /. i) and
A9: len f2 = len f and
A10: f2 . 1 = (f /. 1) => A and
A11: for i being Element of NAT st 1 <= i & i < len f holds
f2 . (i + 1) = (f /. (i + 1)) => (f2 /. i) ; :: thesis: f1 = f2
A12: 1 <= len f2 by A9, NAT_1:25, A5;
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 S₁[ 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 n in dom f1 ; :: thesis: f1 . n = f2 . n
then A15: n in Seg (len f1) by FINSEQ_1:def 3;
then 1 <= n by FINSEQ_1:1;
then 1 + (- 1) <= n + (- 1) by XREAL_1:6;
then A16: n -' 1 = n - 1 by XREAL_0:def 2;
then A17: (n -' 1) + 1 <= len f by A6, A15, FINSEQ_1:1;
A18: for i being Nat st S₁[i] holds
S₁[i + 1]

proof

let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume A19: S₁[i] ; :: thesis: S₁[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 i = 0 ; :: thesis: f1 . ((i + 1) + 1) = f2 . ((i + 1) + 1)

hence f1 . ((i + 1) + 1) = (f /. ((i + 1) + 1)) => (f2 /. (i + 1)) by A13, A20, A8
.= f2 . ((i + 1) + 1) by A20, A21, A11 ;
:: thesis: verum

end;

suppose i >= 1 ; :: thesis: f1 . ((i + 1) + 1) = f2 . ((i + 1) + 1)

A22: f1 /. (i + 1) = f1 . (i + 1) by FINSEQ_4:15, A6, A20, A21
.= f2 /. (i + 1) by FINSEQ_4:15, A9, A20, A19, NAT_1:12 ;
thus f1 . ((i + 1) + 1) = (f /. ((i + 1) + 1)) => (f1 /. (i + 1)) by A20, A21, A8
.= f2 . ((i + 1) + 1) by A20, A21, A11, A22 ; :: thesis: verum

end;

end;

end;

A23: S₁[ 0 ] by A7, A10;
A24: for i being Nat holds S₁[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 FINSEQ_3:29, A6, A9;
hence f1 = f2 by A14, PARTFUN1:5; :: thesis: verum

end;

thus ( not len f > 0 & f1 = <*> LTLB_WFF & f2 = <*> LTLB_WFF implies f1 = f2 ) ; :: thesis: verum