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 ;
1 <= len f1 by ;
then A13: f1 /. 1 = f1 . 1 by FINSEQ_4:15
.= f2 /. 1 by ;
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 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 ;
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 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 ;
:: thesis: verum
end;
suppose i >= 1 ; :: thesis: f1 . ((i + 1) + 1) = f2 . ((i + 1) + 1)
A22: f1 /. (i + 1) = f1 . (i + 1) by
.= f2 /. (i + 1) by ;
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: S1[ 0 ] by ;
A24: for i being Nat holds S1[i] from thus f1 . n = f2 . n by ; :: thesis: verum
end;
dom f1 = dom f2 by ;
hence f1 = f2 by ; :: thesis: verum
end;
thus ( not len f > 0 & f1 = <*> LTLB_WFF & f2 = <*> LTLB_WFF implies f1 = f2 ) ; :: thesis: verum